Skip to content

Instantly share code, notes, and snippets.

View viercc's full-sized avatar

Koji Miyazato viercc

View GitHub Profile
type A :: Type
type X :: Type
type F :: Type -> Type
instance Functor F

p :: forall x. (F x, x -> A) -> X

newtype H a = H { runH :: (a -> A) -> X }
@viercc
viercc / sequenceA-eq-distribute.md
Last active May 7, 2024 14:46
sequenceA == distribute?

https://twitter.com/lotz84_/status/1787796266484908211

lotz @lotz84_

これを書いていて Vector n a 同士の sequenceA が distribute のように振る舞うのが気になった👀 一般に Traversable の distribute が Distributive の sequenceA に一致することが則を使って言えないだろうか?🤔 QuickCheck で少し探してみたけど反例はなさそう

大枠

-- Overkilling a cute li'l exercise
-- https://www.reddit.com/r/haskell/comments/v0mfkl/cute_lil_exercise/
{-# LANGUAGE UnicodeSyntax, TypeOperators, ScopedTypeVariables, RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
-- (this time without ImpredicativeTypes, but I'm not sure it's better or not)
module Isomorphisms2(goal, to, from) where
import Prelude hiding (id, (.))
import Control.Category
-- https://twitter.com/mi12cp/status/1753203763211571656
-- https://twitter.com/rsk0315_h4x/status/1753233137629646938
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ExistentialQuantification #-}
module Main where
import Data.IORef
-- trait Fn()
{-# LANGUAGE RankNTypes #-}
module PolymorphicState where
{-
-- https://twitter.com/Kory__3/status/1737757423673413635
> forall s, a. Monad (a =>> s -> (s, a)) の値って一意なのでしょうか
-}
{-# LANGUAGE GHC2021 #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PolyKinds, DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE UndecidableInstances #-}
module InfiniteHigherOrderEffect where
import Data.Kind (Type)
import Data.Functor.Contravariant (Contravariant)
@viercc
viercc / monolocalbinds.hs
Last active December 8, 2023 05:18
Effect of MonoLocalBinds
{-# LANGUAGE ExplicitForAll #-}
-- With MonomorphismRestriction (which is ON by default,)
-- any constrained type variable (e.g. `m` in `Monad m`)
-- are not generalized
{-# LANGUAGE NoMonomorphismRestriction #-}
-- MonoLocalBinds prevents generalization of non-top-level binding
{-# LANGUAGE MonoLocalBinds #-}
-- Compare for

(1)

-- m は暗黙に量化されている
{-
action :: forall m. MonadError OutOfRange m => m Int
-}
action :: MonadError OutOfRange m => m Int
action = undefined
@viercc
viercc / Check.hs
Last active January 30, 2023 13:37
Note on Distributive laws for semialign package
-- This exists so that I haven't made a silly mistake,
-- like typo or type mismatch of expressions surrounding equal sign.
{-# LANGUAGE TypeOperators #-}
module Check where
import Prelude hiding (zip)
import Data.These
import Data.Zip
import Data.Bifunctor
-- https://www.reddit.com/r/haskell/comments/z9eyu7/monthly_hask_anything_december_2022/izpv48z/
{-# language
DeriveGeneric,
DerivingVia,
StandaloneDeriving,
TypeOperators,
FlexibleInstances,
ScopedTypeVariables,
TypeFamilies,
TypeApplications,