日記 (2020 年 4 月 10 日)
Haskell などの純粋関数型言語では、 全ての関数は純粋である必要があるので、 副作用を伴う計算 (アクション) をそのまま扱うことはできない。
そのような言語でアクションを扱う方法として、 モナドというものがある。
これは、 各型 A に対して副作用の内容を包んだ値を扱える新しい型 #A を用意しておき、 副作用のある関数が返す値として A 型の値ではなく #A 型の値にするというアイデアである。
もちろん、 #A としてどんな型を用いても良いというわけではなく、 このアイデアがうまく動くためには、 次に述べる 2 種類の操作が定まっている必要がある。
まず、 副作用がない関数もアクションの一種として扱えるように、 A 型の値から #A 型の値を作る操作 η が必要である。
また、 何らかのアクションを実行して得られた #A 型の値を用いて別のアクションを実行できるように、 任意のアクション f:A→#B を引数の型が副作用付きの型になった f∗:#A→#B に変換する操作 -∗ も必要である。
さらに、 詳細は省略するが、 この 2 つの操作が互いによく振る舞うように、 いくつかの条件 (いわゆるモナド則) が満たされている必要がある。
このような組 (#,η,-∗) は Kleisli トリプルと呼ばれ、 計算の概念を圏論的に扱う枠組みとして、 Moggi†1 の研究以来注目されてきた。
Kleisli トリプルはモナドという概念と等価であることが知られており、 それゆえに、 このアイデアをプログラミング言語に落とし込んだものもモナドと呼ばれている。
圏論的には、 Kleisli トリプルよりモナドの方が扱いやすいため、 以降はモナドの方を扱うことにする。
モナドとは、 以下で定義される概念である。
定義 1.
圏 上の自己関手 #:→ を考える。
対象 A に対し、 自然な射 μA:##A→#A,ηA:A→#A が定まっていて、 任意の対象 A に対し、 図式
###A##A##A#Aμ#A#μAμAμA#A##A#A#Aη#A#ηAμA
が全て可換であるとする。
このとき、 (#,μ,η) をモナド (monad) という。
Haskell などに導入されているモナドの圏論的解釈を考えると、 確かにそれは圏論の意味でのモナドになっているのだが、 実はより狭い概念である強モナドになっている。
強モナドとは、 以下で定義される概念で、 モナドに追加の構造を加えたものである。
定義 2.
有限直積をもつ圏 上のモナド (#,μ,η) を考える。
対象 A,B に対し、 両方の変数に関して自然な射 τAB:A×#B→#(A×B) が定まっていて、 任意の対象 A,B,C に対し、 図式
(A×B)×#C#((A×B)×C)A×(B×#C)A×#(B×C)#(A×(B×C))τA×B,Cid×τBCτA,B×C #A1×#A#(1×A)τ1A A×##B#(A×#B)##(A×B)A×#B#(A×B)τA,#B#τABτABid×μBμA×B A×BA×#B#(A×B)τABid×ηBηA×B
が全て可換であるとする。
このとき、 (#,η,μ) を強モナド (strong monad) といい、 τ を強度 (strength) という。
それでは、 なぜただのモナドではなく強モナドに対応するのだろうか。
その理由を観察するため、 モナドをもつプログラミング言語と強モナドをもつ圏との対応を実際に示してみよう。
そのために、 まずモナドをもつプログラミング言語を型システムとして形式化する。
定義 3.
型システム Monad を以下のように定める。
まず、 型 A と項 M を、
A ::= α∣1∣A×A∣#A M ::= a∣⋆∣⟨M,M⟩∣fstM∣sndM∣returnM∣M{a↦M}
で定める。
ここで、 α と a はそれぞれ原子型と変項を表す。
次に、 項の型割り当ての推論規則を、
Γ,a:A,Γ⊢a:A ⊢⋆:1 Γ⊢M:A Γ⊢N:B Γ⊢⟨M,N⟩:A×B Γ⊢M:A×B Γ⊢fstM:A Γ⊢M:A×B Γ⊢sndM:B Γ⊢M:A Γ⊢returnM:#A Γ⊢M:#A Γ,a:A⊢N:#B Γ⊢N{a↦M}:#B
で定める。
最後に、 同じ型を割り当てられた項の間の等号を、
⋆ = M fst⟨M,N⟩ = M snd⟨M,N⟩ = N ⟨fstM,sndM⟩ = M M{a↦N{b↦P}} = (M{a↦N}){b↦P} M{a↦returnN} = M[a:=N] (returna){a↦M} = M
で定め、 合同関係になるように拡張する。
形式理論における型 #A がモナド型を表していて、 returnM と N{a↦M} はそれぞれモナドの return と bind に対応するものである。
N{a↦M} の代わりに M>>=λa.N と書けば、 Haskell に慣れている人にとって意図が分かりやすいであろう。
また、 等号の定義の最後の 3 つの式は、 モナド則を表現している。
型システムと圏との対応は、 次のように定義される。
定義 4.
型システム を考える。
有限直積をもつ圏 に対し、 変換 - が、
- の型 A に対し、 の対象 A が定まっている。
- における項の型割り当て Γ⊢M:A に対し、 の射 Γ⊢M:A:Γ→A が定まっている。
ここで、 Γ≡b1:B1,⋯,bn:Bn と書くとき、 Γ=B1×⋯×Bn と定めた。
なお、 記法を簡略化して、 Γ⊢M:A の代わりに単に M と書くこともある。
を満たすように定まっている。
このとき、 - を の解釈 (interpretation) という。
定義 5.
型システム を考える。
有限直積をもつ圏 と解釈 - が、 次の条件を満たすとする。
すなわち、 における同じ型をもつ任意の型割り当て Γ⊢M:A および Γ⊢N:A に対し、 において M=N ならば の射として M=N が成り立つ。
このとき、 (,-) を のモデル (model) という。
では、 圏が強モナドをもつときに、 それが型システム Monad のモデルになることを示そう。
定理 6.
有限直積をもつ圏 が強モナド (#,μ,η,τ) をもつとする。
このとき、 は Monad のモデルである。
証明.
まず、 型の解釈を
1=1 A×B=A×B#A=#A
によって再帰的に定める。
原子型の解釈は自由に選んで良い。
次に、 項の解釈も再帰的に定める。
bind に対応する型割り当て規則以外の場合は、
Γ,a:A,Γ⊢a:A = prA ⊢⋆:1 = id1 Γ⊢⟨M,N⟩:A×B = (Γ⊢M:A,Γ⊢N:B) Γ⊢fstM:A = prA∘Γ⊢M:A×B Γ⊢sndM:B = prB∘Γ⊢M:A×B Γ⊢returnM:#A = ηA∘Γ⊢M:A
によって定める。
なお、 式中の pr で書かれた射は、 直積からの適切な射影を表す。
bind に対応する型割り当てについては、 強モナドに定まっている強度を用いて、
Γ⊢N{a↦M}:#B=❲ΓΓ×#A#(Γ×A)##B#B(id,M)τΓ,A#NμB❲
と定める。
このようにすると解釈 - が定まり、 これは項の等号を保存することが (手間はかかるが) 難しくない計算で確かめられる。
以上により、 (,-) はモデルになる。
この証明において強モナドに定まった強度が必要なのは、 N{a↦M} という形の項の解釈を定める箇所である。
このような項を解釈するためには、 2 つの射 m:Γ→#A,n:Γ×A→#B を用いて Γ→#B という形の射を作る必要がある。
m と n を組み合わせてこの形の射を作ろうとすると、 n の始域を Γ×A から Γ×#A にしたいが、 モナドの構造を用いて対象の全体に # を付けることはできても、 直積の片方にのみ # を付けることは一般には不可能である。
そこで、 Γ×#A→#(Γ×A) という形の射、 すなわち強度が必要になるのである。
参考文献
- E. Moggi (1991) 「Notions of computation and monads」 『Information and Computation』 93:55–92