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^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 :: *からなる"多項式"を記述している」という雰囲気があります。