HeftierEquiv.txt

括弧が見づらいので()に加えて[],{}も括弧の代わりに使います
つまり[]はいわゆる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' ■

Effectが実は多項式Functorだったというのも興味深いです、最初に論文でEffectの定義を見た時なんかアドホックな感じがしたんですがちゃんと理論的な裏付けができたんですね

Effectが実は多項式Functor

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