日記 (2020 年 4 月 15 日)
Haskell などの純粋関数型言語で副作用を伴う計算 (アクション) を扱う構造には、 よく知られているモナドの他にアローというものがある。
これは、 Hughes†2 によってモナドの一般化として導入された概念である。
相変わらず私は型システムを見ると圏論的意味論が気になる人間なので、 このアローの圏論的意味論についてこれから触れていこうと思う。
まず、 アローを考える前に、 ベースとなる型システムの定式化を行っておく。
ここでは、 通常の単純型付きラムダ計算の体系に直積を追加したものを用いる。
定義 1.1.
型システム λ1× を以下のように定める。
まず、 型 A と項 M を、
A ::= α∣1∣A×A∣A⇀A M ::= a∣⋆∣⟨M,M⟩∣fstM∣sndM∣λa.M∣MM
で定める。
ここで、 α と a はそれぞれ原子型と変項を表す。
次に、 項の型割り当ての推論規則を、
Γ,a:A,Γ⊢a:A ⊢⋆:1 Γ⊢M:A Γ⊢N:B Γ⊢⟨M,N⟩:A×B Γ⊢M:A×B Γ⊢fstM:A Γ⊢M:A×B Γ⊢sndM:B Γ,a:A⊢M:B Γ⊢λa.M:A⇀B Γ⊢M:A⇀B Γ⊢N:#A Γ⊢MN:B
で定める。
最後に、 同じ型を割り当てられた項の間の等号を、
⋆ = M fst⟨M,N⟩ = M snd⟨M,N⟩ = N ⟨fstM,sndM⟩ = M (λa.M)N = M[a:=N] λa.Ma = M
で定め、 合同関係になるように拡張する。
ただし、 最後の等式において M は自由変項に a を含まないものとする。
型システムの圏論的意味論とは、 型システムに定まっている型と項をそれぞれ特定の圏の対象と射に対応させることを考えるものである。
この対応は解釈と呼ばれ、 次のように定式化される。
なお、 解釈は 2 重の角括弧 (いわゆるオックスフォードブラケット) で囲んで表記するのが通例だが、 表記が煩雑になるのを防ぐため、 ここではオーバーラインで表記することにする。
定義 1.2.
型システム を考える。
有限直積をもつ圏 に対し、 変換 - が、
- の型 A に対し、 の対象 A が定まっている。
- における項の型割り当て Γ⊢M:A に対し、 の射 Γ⊢M:A:Γ→A が定まっている。
ここで、 Γ≡b1:B1,⋯,bn:Bn と書くとき、 Γ=B1×⋯×Bn と定めた。
なお、 記法を簡略化して、 Γ⊢M:A の代わりに単に M と書くこともある。
を満たすように定まっている。
このとき、 - を の での解釈 (interpretation) という。
型システムの圏論的意味論は、 単純型付きラムダ計算とカルテシアン閉圏がちょうど対応するという、 Lambek†4 による有名な結果が起源である。
この結果は次のように述べることができる。
定理 1.3.
単純型付きラムダ計算 λ1× は、 任意のカルテシアン閉圏で標準的な解釈をもつ。
さらに、 λ1× における型割り当て Γ⊢M:A および Γ⊢N:A に対し、 λ1× において M=N が成り立つための必要十分条件は、 任意のカルテシアン閉圏において M=N が成り立つことである。
さて、 本題に移ろう。
Hughes によって導入されたアローの定式化として、 以下のような λ1× を拡張した型システムを考えることにする。
基本的に Haskell における定義をそのまま写し取っただけである。
定義 1.4.
型システム Arrow を λ1× の拡張として以下のように定める。
まず、 型 A と項 M を、
A ::= ⋯∣[A,A] M ::= ⋯∣arrM∣M⋙M∣firstM
と拡張する。
次に、 項の型割り当ての推論規則に、
Γ⊢M:A⇀B Γ⊢arrM:[A,B] Γ⊢F:[A,B] Γ⊢G:[B,C] Γ⊢F⋙G:[A,C] Γ⊢F:[A,B] Γ⊢firstF:[A×C,B×C]
を追加する。
最後に、 同じ型を割り当てられた項の間の等号に、
arrid⋙F = F F⋙arrid = F (F⋙G)⋙H = F⋙(G⋙H) arr(M⊳N) = arrM⋙arrN first(arrM) = arr(M×id) firstF⋙arr(id×M) = arr(id×M)⋙firstF first(F⋙G) = firstF⋙firstG firstF⋙arrfst = arrfst⋙F first(firstF)⋙arrassoc = arrassoc⋙firstF
を追加し、 合同関係になるように拡張する。
ここで、
id : A⇀A ≡ λa.a fst : A×B⇀A ≡ λp.fstp assoc : (A×B)×C⇀A×(B×C) ≡ λp.⟨fst(fstp),⟨snd(fstp),sndp)⟩⟩ ⊳ : (A⇀B)×(B⇀C)⇀(A⇀C) ≡ λm.λn.λa.n(ma) × : (A⇀B)×(B⇀D)⇀(A×C⇀B×D) ≡ λm.λn.λp.⟨m(fstp),n(sndp)⟩
で定めている。
すなわち順に、 恒等関数, 直積から第 1 成分への射影関数, 3 つの直積の結合を変える関数, 関数の合成演算, 関数の直積演算である。
我々の課題は、 λ1× にカルテシアン閉圏が対応したのと同様の意味で、 Arrow に対応する圏のクラスを見出すことである。
そのような圏のクラスとは Freyd 圏であるという研究がすでに存在しており、 Jacobs–Heunen–Hasuo†3 や Atkey†1 で詳しく述べられているので、 これらを参考にしつつ次回以降まとめていこうと思う。
参考文献
- R. Atkey (2011) 「What is a categorical model of arrows?」 『Electronic Notes in Theoretical Computer Science』 229:19–37
- J. Hughes (2000) 「Generalising monads to arrows」 『Science of Computer Programming』 37:67–111
- B. Jacobs, C. Heunen, I. Hasuo (2009) 「Categorical semantics for arrows」 『Journal of Functional Programming』 19:403–438
- J. Lambek (1980) 「From lambda calculus to cartesian closed categories」 『To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism』 376–402