Data.Exists

使い方

code:purs(hs)

newtype ShowBox' a = SB { value :: a, show :: a -> String }

newtype ShowBox = ShowBox (Exists ShowBox')

普通の書き方でいったんShowBox' aを定義しておいてから、Exists ShowBox'で本命を作る

こういう気持ちで読めばいい

code:purs(hs)

newtype ShowBox = ShowBox (exsits a. a)

あるいは

code:purs(hs)

newtype ShowBox = ∀ a. ShowBox a

これはまさにHaskellの存在型の定義の仕方mrsekut.icon

実装

code:purs(hs)

type role Exists representational

mkExists :: forall f a. f a -> Exists f

mkExists = unsafeCoerce

runExists :: forall f r. (forall a. f a -> r) -> Exists f -> r

runExists = unsafeCoerce

いろいろ見どころがあるmrsekut.icon

type roleを使っている

mkExistsの型

runExistsの型

forallを二重に使っている

ExistsはStack Safety for Freeに出てきたmrsekut.icon

code:purs(hs)

data GosubF f a b = GosubF (Unit -> Free f b) (b -> Free f a)

data Free f a

= Free (Either a (f (Free f a)))

| Gosub (Exists (GosubF f a))