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' ■

=が同型なのか型（対象として等しい）のかの区別がちょっと雑ですね
とりあえず全部同型のイコールとして解釈すれば問題ないはず…

気付いたんですけど、Coyoneda関係なしにCoyoneda合成しないバージョンでもこの関係成り立ってそう…

Free f a = Pure a | Free [f (Free f a)]

Hefty' h a := Free [h (Hefty' h)] a
= Pure a | Free {h (Hefty' h) {Free [h (Hefty' h)] a}}
= Pure a | Free [h (Hefty' h) (Hefty' h a)]

Hefty h a = Return a | Op [h (Hefty h) (Hefty h a)]

∴ Hefty ≅Hefty' ■

こっちのほうはシンプルですね

論文中の定義と
https://gist.github.com/ymdryo/e8af81d454371c719c289eba1418e573?permalink_comment_id=4818728#gistcomment-4818728
で定義されたHefty（以後Hefty3）が等価であることについての大まかな流れです

論文中の定義を引用すると

data Hefty (H : Effect^H) (A : Set) where
    pure : A → Hefty H A
    impure : (op : Op^H H)
                    (ψ: (a : Op (Fork H op)) → Hefty H (Ret (Fork H op) a))
                    (k : Ret^H H op → Heft H A)
                    → Hefty H A

ここでOp (Fork H op)は高階エフェクトHが保持するスコープの集合に対する添字で、Ret (Fork H op) aはエフェクトの戻り値がaのときの各スコープの戻り値と解釈できます
この解釈に沿って、(*→*)→*→*種のGADTsで表現された高階エフェクトのうち典型的なものはすべてEffect^Hによる表現に変換できるはずです

例えば論文中の

data CatchOp^d : Set_1 where
    catch^d : Set → CatchOp^d

Catch^d : Effect^H
Op^H Catch^d = CatchOp^d
Fork Catch^d (catch^d A) = record { Op = Bool; Ret = λ _ → A }
Ret^H Catch^d (catch^d A) = A

ですが

data Catch (m : Set → Set) (a : Set) where
    catch :: m a -> m a -> m a

のように変換できます

一方、impureを非カリー化して
impure : ((op : ..., ψ : ...), k : ...) → Hefty H A
を得ることができますが、kはHeftyにco-Yonedaが合成されていることに由来する継続なので、これはco-Yonedaを取り除く変形によって消すことができます（この変形でop,ψの型は変化することに注意してください）
co-Yonedaを取り除いた後のHeftyをHefty2と書くと
impure : (op : ..., ψ: ...) → Hefty2 H A
この(op,ψ)の型が、ちょうどEffect^H表現Hを(*→*)→*→*なGADTsな形式hに書き直した場合の、h (Hefty h) (Hefty h A)と同型になっていることが示せるはずです
（i.e. Effect^Hにより表現された任意の高階エフェクト型Hについて、この同型性を満たすようなH' : (Set→Set)→Set→Setが存在する）

たとえばCatchの場合、impureは、Op^HやForkなどを展開する同型な変形を施すと
impure : (b : Set) (ψ : Bool → Hefty Catch b) (k : b → Hefty Catch A) → Hefty Catch A
となります
（わかりやすさのために、変数名opをbに置き換えました。Coyonedaの定義における量化された型変数bに合わせてあります）
co-Yonedaを脱合成すると、bがHefty Catch Aに置き換えられて
impure : (ψ : Bool → Hefty2 H (Hefty2 Catch A)) → Hefty2 Catch A
Bool→・は単に長さ2の配列、つまり(・,・)なので
impure : (ψ1 : Hefty2 Catch (Hefty2 Catch A)) (ψ2 : Hefty2 Catch (Hefty2 Catch A)) → Hefty2 Catch A

これは(*→*)→*→*なGADTsにより表現されたCatchを利用した場合の、
Hefty3 (Catch (Hefty3 Catch))
のOpコンストラクタと等価になっています。（Effectのレコードの中のOpとは無関係なことに注意、名前が被ってしまった）
つまりHefty3のhにCatchを代入すると、CatchのmがHefty3 Catchになるので
Op : Hefty3 Catch (Hefty3 Catch a) → Hefty3 Catch (Hefty3 Catch a) → Hefty3 Catch a
です

以上、pureに関してはそのままReturnに対応していて、impureについても高階エフェクトのエンコードを適切に取り直せばOpと同型に対応している（同型に対応させることができるようなエンコードの変換が常に可能）、という話でした

ところでEffect^Hだと

data UnliftIO m a where
withRunInIO : ((forall x. m x -> IO x) -> IO a) -> UnliftIO m a

のような、mが出現する位置が特殊だがHFunctorにはなるタイプの高階エフェクトを表現できない気がします

この(op,ψ)の型が、ちょうどEffect^H表現Hを(*→*)→*→*なGADTsな形式hに書き直した場合の、h (Hefty h) (Hefty h A)と同型になっていること

これは一度示したことがあるのですが、どこにも書いていませんでしたし、意外と難しかったので転記してみます。

impure :
  (op : Op^H H)
  (ψ: (a : Op (Fork H op)) → Hefty H (Ret (Fork H op) a))
  (k : Ret^H H op → Hefty H A)
  → Hefty H A

において、ψの型は以下のように変形できます。

(a : Op (Fork H op)) → Hefty H (Ret (Fork H op) a)
 ≅ 〈Hefty H (-) に Yoneda〉
(a : Op (Fork H op)) → ∀ r. (Ret (Fork h op) a → r) → Hefty H r
 ≅ 〈rとaのスコープを交換〉
∀r. (a : Op (Fork H op)) → (Ret (Fork h op) a → r) → Hefty H r
 ≅ 〈カリー化〉
∀r. Σ[a ∈ Op (Fork H op)] (Ret (Fork h op) a → r) → Hefty H r

ここで、変形後の関数の引数部分は、Effectである

Fork H op = record { Op = Op (Fork H op), Ret = Ret (Fork h op) } : Effect

を、Functorとしての表現に戻したものになっています。

• 注. Effectが表現するFunctorは、

  ToFunctor : Effect → Set → Set
  ToFunctor eff x = Σ[ a ∈ Op eff ] (Ret eff a → x)
  

  と同型です。これは任意のFunctorを表現できているわけではなく、いわゆる多項式Functorです。

すなわち、

ψの型
 ≅
∀r. ToFunctor (Fork H op) → Hefty H r
 =
ToFunctor (Fork H op) ~> Hefty H

となっています。これをimpure自体の型に代入すると

impureの型
 ≅
  (op : Op^H H)
  (ψ: ToFunctor (Fork H op) ~> Hefty H)
  (k : Ret^H H op → Hefty H A)
  → Hefty H A

となります。

この関数の引数部分を切り出したToHFunctor、すなわち以下の定義

ToHFunctor : Effect^H → (Set → Set) → Set → Set
ToHFunctor H h x = Σ[ op ∈ Op^H H ] (ToFunctor (Fork H op) ~> h) (Ret^H H op → x)

が、HFunctorを各Effect^Hに対して定義しており、impureの型はToHFunctor H (Hefty H) (Hefty H A) -> Hefty H Aと一致していることは簡単に確かめられます。問題は、高階エフェクトとして使ったどんな種類のHFunctor hもEffect^Hとして表現できているかです。

残念ながら、これが任意のHFunctorを表している訳ではなさそうです。ですが、Effect^Hで定義できるHFunctorが

• 和 (HSum)
• 積 (HProduct)
• 合成 (Compose, HCompose)

で閉じていることは確かめられます。すなわち、
和・積・合成によって既知の高階エフェクトを組み立てて得られるようなHFunctorはEffect^Hで定義できます。

HSumに関しては簡単ですので省略します。

-- HFunctorの積
newtype HProduct h1 h2 f x = Pair (h1 f x) (h2 f x)

effSum : Effect → Effect → Effect
effSum e1 e2 = record {
  Op = Op e1 + Op e2 ;
  Ret a = case a of λ {
    inj₁ a → Ret e1 a ;
    inj₂ a → Ret e2 a
  }
}

ToFunctor (effSum e1 e2) ≅ Data.Functor.Sum (ToFunctor e1) (ToFunctor e2)

effH-Product : Effect^H → Effect^H → Effect^H
effH-Product e1 e2 = record {
  Op^H = Op^H e1 × Op^H e2 ;
  Fork (op1 , op2) = effSum (Fork op1) (Fork op2) ;
  Ret^H (op1 , op2) = Ret^H op1 + Ret^H op2
}

ToHFunctor (e := effH-Product e1 e2) h x
 =
Σ[ op ∈ Op^H e ] ((ToFunctor (Fork e op) ~> h)×(Ret^H e op -> x))
 ≅
Σ[ (op1, op2) ∈ Op^H e1 × op^H e2 ] (
  (Sum (ToFunctor (Fork e1 op)) (ToFunctor (Fork e2 op)) ~> h)
   × (Ret^H e1 + Ret^H e2 -> x)
)
 ≅
Σ[ (op1, op2) ∈ Op^H e1 × op^H e2 ] (
  (ToFunctor (Fork e1 op) ~> h) × (ToFunctor (Fork e2 op) ~> h)
  × (Ret^H e1 -> x) × (Ret^H e2 -> x)
)
 ≅
(
  Σ[ op1 ∈ Op^H e1 ] ((ToFunctor (Fork e1 op) ~> h) × (Ret^H e1 -> x))
   × 
  Σ[ op2 ∈ Op^H e2 ] ((ToFunctor (Fork e2 op) ~> h) × (Ret^H e2 -> x))
)
 ≅
(
  Σ[ op1 ∈ Op^H e1 ] ((ToFunctor (Fork e1 op) ~> h) × (Ret^H e1 -> x))
   × 
  Σ[ op2 ∈ Op^H e2 ] ((ToFunctor (Fork e2 op) ~> h) × (Ret^H e2 -> x))
)
 ≅
ToFunctor e1 h x × ToFunctor e2 h x
 ≅
HProduct (ToFunctor e1) (ToFunctor e2) h x

合成(Compose)についても

effH-Compose : Effect^H -> Effect^H -> Effect^H
effH-Compose e1 e2 = record {
  Op^H = Σ[ op1 ∈ Op^H e1 ] (Ret^H e1 op -> Op^H e2) ;
  Fork (op1 , op2s : Ret^H e1 op1 -> Op^H op2) = record {
    Op = Op (Fork e1 op1) + (Π(a1 : Ret^H e1 op1) → Op (Fork e2 (op2s a1))) ;
    Ret a = case a of λ {
      inj₁ a1 → Ret (Fork e1 op1) ;
      inj₂ aToOp2 → Σ[ a1 ∈ Ret^H e1 op1 ] (Ret (Fork e2 (op2s a1)) (aToOp2 a1))
    }
  } ;
  Ret^H (op1 , op2s) = Σ[ a1 ∈ Ret^H e1 op1 ] (Ret^H e2 (op2s a1))
}

とするとtoHFunctor (effH-Compose e1 e2) h x ≅ ToHFunctor e1 h (ToHFuncto e2 h x)にできます。

きちんと計算はしていないのですが、HComposeについても同様にできるはずです。

👍

おお、もう既に自分以外が取り組んでいただいていた…共有助かります！！

Effect^Hが和・積・合成について閉じているというのは（HFunctorのサブセットとはいえ）かなり良い感じの性質ですね…

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

Effectが実は多項式Functor

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