日記 (2020 年 5 月 12 日)
4 月 18 日までのアローに関する日記の続き。
これまでは、 Haskell に定まったいるアローを形式化し、 それに対応する圏論的構造を模索するという内容で、 最終的に豊穣 Freyd 圏に辿り着いた。
ここからは、 アローにさらなる構造を加えたシステムを取り上げ、 その付加的構造に対応する圏論的構造を模索することを考える。
まずは、 アローを値に適用するという操作そのものをアローとして扱うことを許したシステムを考える。
今回扱うのは、 以下の型システムである。
定義 5.1.
型システム ArrowApply を Arrow の拡張として以下のように定める。
まず、 型については拡張せず、 項 M について、
M ::= ⋯∣app
と拡張する。
次に、 項の型割り当ての推論規則に、
⊢app:[[A,B]×A,B]
を追加する。
最後に、 同じ型を割り当てられた項の間の等号に、
first(arr(λa.arr(λb.⟨a,b⟩)))⋙app = arrid first(arr(λg.F⋙g))⋙app = secondF⋙app first(arr(λf.f⋙G))⋙app = app⋙G
を追加し、 合同関係になるように拡張する。
これは Haskell での定義をそのまま写し取ったものであるが、 実は同値な体系を別の方法で定式化することもできる。
それを示すのが、 次の補題と命題である。
補題 5.2.
型システム Arrow において、 型多相な閉じた項 sharp を、
sharp : [A×B,C]⇀(A⇀[B,C]) ≡ λh.λa.arr(λb.⟨a,b⟩)⋙h
によって定めると、 これは全ての型変数に関して自然である。
すなわち、 3 種類の等式
sharp(first(arrM)⋙H) = M⊳sharpH sharp(secondF⋙H) = λa.F⋙sharpHa sharp(H⋙G) = λa.sharpHa⋙G
が全て成り立つ。
命題 5.3.
型システム Arrow において、 2 条件
- 型多相な閉じた項 app:[[A,B]×A,B] であって、 3 種類の等式
first(arr(λa.arr(λb.⟨a,b⟩)))⋙app = arrid first(arr(λg.F⋙g))⋙app = secondF⋙app first(arr(λf.f⋙G))⋙app = app⋙G
を全て満たすものが存在する。
- 型多相な閉じた項 flat:(A⇀[B,C])⇀[A×B,C] であって、 sharp の逆関数となっているものが存在する。
すなわち、 2 種類の等式
flat(sharpH) = H sharp(flatM) = M
が全て満たされる。
は同値である。
これにより、 アローの適用を行うアローの構造を加えた ArrowApply を定義するにあたって、 最初に行ったように 3 つの等式を満たす app をプリミティブな演算として入れても良いし、 上の定理中の 2 つの等式を満たす flat をプリミティブな演算として入れても良いことになる。
証明.
条件 1 ⇒ 条件 2:まず、
flat : (A⇀[B,C])⇀[A×B,C] ≡ λm.first(arrm)⋙app
とおく。
これが条件 2 にある 2 つの等式を満たすことを示す。
1 つ目の等式を示す。
まず、
flat(sharpH) = first(arr(λa.arr(λb.⟨a,b⟩)⋙H))⋙app♡1
である。
ここで、
λa.arr(λb.⟨a,b⟩)⋙H = (λa.arr(λb.⟨a,b⟩))⊳(λf.f⋙H)
であるから、
first(arr(λa.arr(λb.⟨a,b⟩)⋙H))⋙app = first(arr(λa.arr(λb.⟨a,b⟩))⋙first(arr(λf.f⋙H))⋙app = first(arr(λa.arr(λb.⟨a,b⟩))⋙app⋙H = arrid⋙H = H♡2
が成り立つ。
式 ♡1,♡2 を合わせれば、 導きたかった式が得られる。
2 つ目の等式を示す。
まず、
sharp(flatM) = λa.arr(λb.⟨a,b⟩)⋙first(arrM)⋙app = λa.arr(λb.⟨a,b⟩)⋙arr(M×id)⋙app = λa.arr((λb.⟨a,b⟩)⊳(M×id))⋙app = λa.arr(λb.⟨Ma,b⟩)⋙app♤1
が成り立つ。
さて、
lu≡λb.⟨⋆,b⟩
とおくと、 lu と snd は互いに逆関数になっているから、
λb.⟨Ma,b⟩ = λb.⟨arrlu⋙arrsnd⋙Ma,b⟩ = (λb.⟨arrlu,b⟩)⊳((λf.f⋙arrsnd⋙Ma)×id)
が成り立つ。
したがって、
G≡arrsnd⋙Ma
とおけば、
λa.arr(λb.⟨Ma,b⟩)⋙app = λa.arr(λb.⟨arrlu,b⟩)⋙arr((λf.f⋙G)×id)⋙app = λa.arr(λb.⟨arrlu,b⟩)⋙first(arr(λf.f⋙G))⋙app = λa.arr(λb.⟨arrlu,b⟩)⋙app⋙G♤2
が成り立つ。
さらに、
λb.⟨arrlu,b⟩ = lu⊳snd⊳(λb.⟨arrlu,b⟩) = lu⊳((λu.arrlu)×id) = lu⊳((λu.arr(λb.⟨⋆,b⟩))×id) = lu⊳((λu.arr(λb.⟨u,b⟩))×id)
であるから、
λa.arr(λb.⟨arrlu,b⟩)⋙app⋙G = λa.arrlu⋙arr((λu.arr(λb.⟨u,b⟩))×id)⋙app⋙G = λa.arrlu⋙first(arr(λu.arr(λb.⟨u,b⟩))⋙app⋙G = λa.arrlu⋙arrid⋙G = λa.arrlu⋙G = λa.arrlu⋙arrsnd⋙Ma = λa.Ma = M♤3
である。
式 ♤1,♤2,♤3 を合わせれば、 導きたかった式が得られる。
条件 2 ⇒ 条件 1:この場合は、
app : [[A,B]×A,B] ≡ flatid
とおけば良い。
これが条件 1 にある 3 つの等式を満たすことを示す。
仮定により sharp は逆関数をもつから、 示したい等式の両辺に sharp を適用した等式を示せば良い。
1 つ目の等式を示す。
左辺に sharp を適用したものは、
sharp(first(arr(λa.arr(λb.⟨a,b⟩)))⋙app) = (λa.arr(λb.⟨a,b⟩))⊳sharpapp = (λa.arr(λb.⟨a,b⟩))⊳sharp(flatid) = λa.arr(λb.⟨a,b⟩)
と計算できる。
また、 右辺に sharp を適用したものは、
sharp(arrid) = λa.arr(λb.⟨a,b⟩)⋙arrid = λa.arr(λb.⟨a,b⟩)
と計算できる。
両者は一致しているので、 これで示された。
2 つ目の等式を示す。
左辺に sharp を適用したものは、
sharp(first(arr(λg.F⋙g))⋙app) = (λg.F⋙g)⊳sharpapp = (λg.F⋙g)⊳sharp(flatid) = λg.F⋙g
と計算できる。
また、 右辺に sharp を適用したものは、
sharp(secondF⋙app) = λg.F⋙sharpappg = λg.F⋙sharp(flatid)g = λg.F⋙g
と計算できる。
両者は一致しているので、 これで示された。
3 つ目の等式も全く同様に示すことができる。
さて、 定理 4.3 により、 型システム Arrow は豊穣 Freyd 圏 (;,J) とちょうど対応することが分かっていた。
この対応を用いて、 上の命題の条件 2 を圏の言葉で述べると次のようになる。
すなわち、 の対象 A,B,C に対し、
φABC=h:[A×B,C]⊢λa.arr(λb.⟨a,b⟩)⋙h:A⇀[B,C]
と定めると、 これが で逆射 ψABC:A⇀[B,C]→[A×B,C] をもつ。
このとき、 補題 5.2 によって φABC は全ての変数について自然だから、 特に における自然な同型
[A×B,C]≅A⇀[B,C]
が成り立つことになる。
これは、 -豊穣関手 J-⋉B:→ および [B,-]:→ が -豊穣随伴を成すということである。
この随伴の単位は、
ηAB=u:1⊢λa.arr(λb.⟨a,b⟩):A⇀[B,A×B]
で与えられる。
また、 随伴の余単位は、 証明中で定義した app で与えられる。
以上の観察から、 次のような圏を考えるのは自然であろう。
定義 5.4.
豊穣 Freyd 圏 (;,J) において、 -豊穣関手 J-⋉B:→ および [B,-]:→ が -豊穣随伴を成しており、 この随伴の単位が上記の η で与えられるとする。
このとき、 (;,J) は閉 (closed) であるという。
そして、 これまでの議論から直ちに以下が分かる。
定理 5.5.
ArrowApply における型割り当て Γ⊢M:A および Γ⊢N:A に対し、 任意の閉である豊穣 Freyd 圏で M=N が成り立つための必要十分条件は、 ArrowApply で M=N が成り立つことである。
ところで、 今回扱った ArrowApply の構造はモナドの構造と同値であることが、 Lindley–Wadler–Yallop†2 などによって証明されている。
型システムとしてのモナドは圏論としては強モナドと対応する (例えば 4 月 10 日を参照) ので、 これと今回の結果を合わせれば、 以下が示せたことになる。
定理 5.6.
カルテシアン閉圏 上において、 強モナド (;M,μ,η,τ) と豊穣 Freyd 圏 (;,J) の間には 1 対 1 対応が存在する。
なお、 豊穣 Freyd 圏の間の関手を適切に定め、 それによって豊穣 Freyd 圏が成す圏を考えれば、 上の対応は圏同値に拡張することができる。
参考文献
- R. Atkey (2011) 「What is a categorical model of arrows?」 『Electronic Notes in Theoretical Computer Science』 229:19–37
- S. Lindley, P. Wadler, J. Yallop (2011) 「Idioms are oblivious, arrows are meticulous, monads are promiscuous」 『Electronic Notes in Theoretical Computer Science』 229:97–117