Skip to content

Instantly share code, notes, and snippets.

@ymdryo
Last active January 6, 2024 10:48
Show Gist options
  • Save ymdryo/e8af81d454371c719c289eba1418e573 to your computer and use it in GitHub Desktop.
Save ymdryo/e8af81d454371c719c289eba1418e573 to your computer and use it in GitHub Desktop.
括弧が見づらいので()に加えて[],{}も括弧の代わりに使います
つまり[]はいわゆるHaskellのリストの型ではないので注意してください
まず前提として
Hefty h a = Return a | Op [h (Hefty h) (Hefty h a)]
Coyoneda f a = ∀b. (b -> a, f b)
です
(cf. https://twitter.com/ymdfield/status/1743235218847465546)
ここでCoyonedaの高階版を定義します
HCoyoneda h f a := Coyoneda (h f) a = ∀b. (b -> a, h f b)
そしてHeftyとHCoyonedaを合成して新たに
Heftier h a := Hefty (HCoyoneda h) a
と定義します
展開すると
Heftier h a
= Return a | Op {HCoyoneda h [Hefty (HCoyoneda h)] [Hefty (HCoyoneda h) a]}
= Return a | Op [HCoyoneda h (Heftier h) (Heftier h a)]
= Return a | Op {Coyoneda [h (Heftier h)] (Heftier h a)} -- (1)
次にFreerから定義したバージョンです
まず
Free f a = Pure a | Free [f (Free f a)]
(https://hackage.haskell.org/package/free-5.2/docs/Control-Monad-Free.html#t:Free より)
そして
Freer f a = Free (Coyoneda f) a
です
展開すると
Freer f a
= Pure a | Free {Coyoneda f [Free (Coyoneda f) a]}
= Pure a | Free {Coyoneda f (Freer f a)}
最後に、Freerに基づき再帰型的に定義したバージョンのHeftier'を
Heftier' h a := Freer [h (Heftier' h)] a
で定義します
( cf. https://twitter.com/Kory__3/status/1733437962787189064
Heftier' h a = (fix α. Freer (h α)) a
)
展開すると
Heftier' h a
= Pure a | Free {Coyoneda [h (Heftier' h)] {Freer [h (Heftier' h)] a}}
Heftier'の定義より
= Pure a | Free {Coyoneda [h (Heftier' h)] (Heftier' h a)}
ところで(1)より
Heftier h a = Return a | Op {Coyoneda [h (Heftier h)] (Heftier h a)}
です
Heftier, Return, OpがそれぞれHeftier', Pure, Freeに対応してます
よって
Heftier ≅ Heftier' ■
@viercc
Copy link

viercc commented Jan 6, 2024

Effectが実は多項式Functor

自分はたまたま多項式Functorに馴染みがあったので自然に流してしまいましたが、結構面白いことですよね
「Effectは任意の多項式Functorを記述している」という目でEffect^Hを見ると、「Effect^Hはh :: * -> *x :: *からなる"多項式"を記述している」という雰囲気があります。

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment