日記 (2020 年 5 月 12 日)

4 月 18 日までのアローに関する日記の続き。 これまでは、 Haskell に定まったいるアローを形式化し、 それに対応する圏論的構造を模索するという内容で、 最終的に豊穣 Freyd 圏に辿り着いた。 ここからは、 アローにさらなる構造を加えたシステムを取り上げ、 その付加的構造に対応する圏論的構造を模索することを考える。 まずは、 アローを値に適用するという操作そのものをアローとして扱うことを許したシステムを考える。

今回扱うのは、 以下の型システムである。

定義 5.1.

型システム ArrowApplyArrow の拡張として以下のように定める。 まず、 型については拡張せず、 項 M について、 M ::= app と拡張する。 次に、 項の型割り当ての推論規則に、 app:[[A,B]×A,B] を追加する。 最後に、 同じ型を割り当てられた項の間の等号に、 first(arr(λa.arr(λb.a,b)))app = arrid first(arr(λg.Fg))app = secondFapp first(arr(λf.fG))app = appG を追加し、 合同関係になるように拡張する。

これは Haskell での定義をそのまま写し取ったものであるが、 実は同値な体系を別の方法で定式化することもできる。 それを示すのが、 次の補題と命題である。

補題 5.2.

型システム Arrow において、 型多相な閉じた項 sharp を、 sharp : [A×B,C](A[B,C]) λh.λa.arr(λb.a,b)h によって定めると、 これは全ての型変数に関して自然である。 すなわち、 3 種類の等式 sharp(first(arrM)H) = MsharpH sharp(secondFH) = λa.FsharpHa sharp(HG) = λa.sharpHaG が全て成り立つ。

証明.

省略する。

命題 5.3.

型システム Arrow において、 2 条件

  1. 型多相な閉じた項 app:[[A,B]×A,B] であって、 3 種類の等式 first(arr(λa.arr(λb.a,b)))app = arrid first(arr(λg.Fg))app = secondFapp first(arr(λf.fG))app = appG を全て満たすものが存在する。
  2. 型多相な閉じた項 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))app1 である。 ここで、 λa.arr(λb.a,b)H = (λa.arr(λb.a,b))(λf.fH) であるから、 first(arr(λa.arr(λb.a,b)H))app = first(arr(λa.arr(λb.a,b))first(arr(λf.fH))app = first(arr(λa.arr(λb.a,b))appH = arridH = H2 が成り立つ。 式 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)app1 が成り立つ。 さて、 luλb󰎘.,b󰎘 とおくと、 lusnd は互いに逆関数になっているから、 λb.Ma,b = λb.arrluarrsndMa,b = (λb.arrlu,b)((λf.farrsndMa)×id) が成り立つ。 したがって、 GarrsndMa とおけば、 λa.arr(λb.Ma,b)app = λa.arr(λb.arrlu,b)arr((λf.fG)×id)app = λa.arr(λb.arrlu,b)first(arr(λf.fG))app = λa.arr(λb.arrlu,b)appG2 が成り立つ。 さらに、 λb.arrlu,b = lusnd(λ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)appG = λa.arrluarr((λu.arr(λb󰎘.u,b󰎘))×id)appG = λa.arrlufirst(arr(λu.arr(λb󰎘.u,b󰎘))appG = λa.arrluarridG = λa.arrluG = λa.arrluarrsndMa = λa.Ma = M3 である。 式 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.Fg))app) = (λg.Fg)sharpapp = (λg.Fg)sharp(flatid) = λg.Fg と計算できる。 また、 右辺に sharp を適用したものは、 sharp(secondFapp) = λg.Fsharpappg = λg.Fsharp(flatid)g = λg.Fg と計算できる。 両者は一致しているので、 これで示された。

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 が成り立つための必要十分条件は、 ArrowApplyM=N が成り立つことである。

証明.

定理 4.3命題 5.3 から従う。

ところで、 今回扱った ArrowApply の構造はモナドの構造と同値であることが、 Lindley–Wadler–Yallop†2 などによって証明されている。 型システムとしてのモナドは圏論としては強モナドと対応する (例えば 4 月 10 日を参照) ので、 これと今回の結果を合わせれば、 以下が示せたことになる。

定理 5.6.

カルテシアン閉圏 󰒚 上において、 強モナド (󰒚;M,μ,η,τ) と豊穣 Freyd 圏 (󰒚;󰒛,J) の間には 1 対 1 対応が存在する。

なお、 豊穣 Freyd 圏の間の関手を適切に定め、 それによって豊穣 Freyd 圏が成す圏を考えれば、 上の対応は圏同値に拡張することができる。

参考文献

  1. R. Atkey (2011) 「What is a categorical model of arrows?」 『Electronic Notes in Theoretical Computer Science』 229:19–37
  2. 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