型付きラムダ計算の意味論はデカルト閉圏で展開できます。したがって、型付きラムダ計算はデカルト閉圏に対する計算系だとみなしてかまいません。しかしながら、関数型プログラミング言語やその処理系は、デカルト閉圏を直接的に扱っているわけではありません。デカルト閉圏を変形した構造に基づいて計算をしています。
デカルト閉圏 $`\mathcal{C}`$ に対して、それを変形した構造を $`/\mathcal{C}/`$ と書くことにします。$`/\mathcal{C}/`$ はラムダ計算のための型システムです。圏 $`\mathcal{C}`$ と型システム $`/\mathcal{C}/`$ は似てはいますが少し違います。「似てるけど少し違う」という状況は、タチの悪い落とし穴になるリスクがあります。“少しの違い”をハッキリさせておきましょう。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\hyp}{\text{-}}
\newcommand{\u}[1]{\overline{#1} }
\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\Ev}{\triangleleft}
\newcommand{\In}{\text{ in } }
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\For}{\Keyword{For } }
\newcommand{\Let}{\Keyword{Let } }
\newcommand{\When}{\Keyword{When } }
`$
内容：
デカルト閉圏から型システムへ
型付きラムダ計算の場合は、はじめに型システムありきなのですが、ここでは逆に、デカルト閉圏ありきで出発します。$`\cat{C} = (\cat{C}, \times, {\bf 1}, [\hyp, \hyp], \mrm{ev})`$ （記号の乱用）をデカルト閉圏とします*1。念のために言っておくと：
- $`\times`$ は、直積を与えるモノイド積。
- $`{\bf 1}`$ は、直積の単位対象、終対象でもある。
- $`[\hyp, \hyp]`$ は、内部ホム〈指数対象〉を与える演算（反変・共変な双関手）。
- $`\mrm{ev}`$ は、評価射 $`\mrm{ev}_{A, B}: [A, B]\times A \to B\In \cat{C}`$ の族。
デカルト閉圏の基本的な性質として以下の同型（カリー同型）が成立します*2。
$`\For A, B, C\in |\cat{C}|\\
\quad \cat{C}(A\times B, C) \cong \cat{C}(A, [B, C])
`$
デカルト閉圏については、「集合圏における依存カリー同型」の前半に、もう少し詳しく書いています。
与えられたデカルト閉圏 $`\cat{C}`$ から次のような構造 $`/\cat{C}/`$ を作ります。
- $`/\cat{C}/ = (|\cat{C}|, \times, \to, \u{(\hyp)}, (\hyp)^\wedge, (\hyp)_\vee,\Ev)`$
- $`|\cat{C}|`$ は、圏 $`\cat{C}`$ の対象の集合（大きい集合かも知れない）。
- $`\times`$ は、圏 $`\cat{C}`$ の直積を対象に制限した二項演算（同じ記号 '$`\times`$' を使う）。
- $`\to`$ は、圏 $`\cat{C}`$ の内部ホム〈指数〉を対象に制限した二項演算（矢印記号 '$`\to`$' を使う理由は後述）。
- $`\u{(\hyp)}`$ は、圏 $`\cat{C}`$ の対象に集合（集合圏 $`{\bf Set}`$ の対象）を対応させる写像。外延化写像〈extensionalize map〉と呼ぶことにします。
- $`(\hyp)^\wedge`$ は、圏 $`\cat{C}`$ の射のフルカリー化 $`(\hyp)_{A, B}^\wedge`$ の族。
- $`(\hyp)_\vee`$ は、圏 $`\cat{C}`$ の射〈ポインティング射〉のフル反カリー化 $`(\hyp)^{A, B}_\vee`$ の族。
- $`\Ev`$ は、外部評価写像〈external evaluation map〉 $`\Ev_{A, B}: \cat{C}({\bf 1}, [A, B])\times \cat{C}({\bf 1}, A) \to \cat{C}({\bf 1}, B)`$ の族。内部評価射 $`\mrm{ev}_{A, B}`$と は違う。
$`/\cat{C}/`$ は、デカルト閉圏 $`\cat{C}`$ に対して作るものであり、それだけが自律的に定義される構造ではありません。具体的にどう作るかは次節で説明します。
ここで、記号に関する注意を述べます。「矢印の混乱に対処する： デカルト閉圏のための記法 // 矢印記号の憂鬱」に挙げた表を再掲すると：
| 型理論 | 論理 | 圏論 |
|---|---|---|
| 関数集合型 $`\to`$ | 含意 $`\Rightarrow`$ | 指数対象 $`[\_, \_]`$ |
| 型判断の区切り $`\vdash`$ | シーケントの区切り $`\to`$ | 射のプロファイルの区切り $`\to `$ |
| 証明可能性 $`\vdash`$ | ||
| 2-射のプロファイルの区切り $`\Rightarrow`$ |
同じ記号でも、分野ごとに意味・使用法が違います。単純な矢印記号 '$`\to`$' に関して言えば、圏論で $`f: A \to B`$ と書いた場合と、関数型プログラミング言語で $`f: A \to B`$ （実際はUnicode文字テキストですが）と書いた場合では意味が違います。しかし、どちらかが矢印記号を手放すなんてことはあり得ないのでオーバーロードは諦めるしかありません。この記事でだけ変更しても（過去に変更したことはありますが）、世間が変わるわけはありません。
そこで、同じ矢印記号を違う意味で使います。
- 圏論では、射のプロファイル（域と余域の仕様）の区切り記号として使う。$`f: A \to B`$ は $`\mrm{dom}(f) = A \land \mrm{cod}(f) = B`$ の意味。
- 型理論／ラムダ計算では、型（圏の対象）に対する二項演算の演算子記号として使う。詳しくは後述。
デカルト閉・型システム
集合圏 $`{\bf Set}`$ はもちろんデカルト閉圏ですが、$`\cat{C}`$ が集合圏だとは限りません。例えば、自然数の集合 $`{\bf N}`$ のベキ集合 $`\mrm{Pow}({\bf N})`$ は包含順序で順序集合ですが、そこからやせた圏〈thin category〉を作れます。集合の共通部分 $`A\cap B`$ と演算 $`A^c \cup B`$ を一緒に考えるとデカルト閉圏が出来上がります -- この圏を $`\cat{C}`$ としても構いません。ωCPO（ボトム有り）を知っていれば、ωCPOと順序連続写像の圏はデカルト閉圏 $`\cat{C}`$ のよい例になります。
前節で紹介した $`/\cat{C}/ = (|\cat{C}|, \times, \to, \u{(\hyp)}, (\hyp)^\wedge, (\hyp)_\vee,\Ev)`$ の各構成素を定義します。$`\cat{C}`$ の直積、$`{\bf Set}`$ の直積、$`{\bf SET}`$ の直積がすべて '$`\times`$' をオーバーロードしているので、注意してください。終対象 $`{\bf 1}`$ もオーバーロードしています。
直積の対象への制限：
$`(\times) : |\cat{C}|\times |\cat{C}| \to |\cat{C}| \In {\bf SET}\\
\For A, B \in |\cat{C}|\times |\cat{C}| \\
\quad A \times B := (A \times B \In \cat{C})`$
内部ホム〈指数〉の対象への制限（演算子記号は矢印記号にする）：
$`(\to) : |\cat{C}|\times |\cat{C}| \to |\cat{C}| \In {\bf SET}\\
\For A, B \in |\cat{C}|\times |\cat{C}| \\
\quad A \to B := ([A, B] \In \cat{C})`$
外延化はポインティング射（終対象からの射）の集合：
$`\u{(\hyp)} : |\cat{C}| \to |{\bf Set}| \In {\bf SET}\\
\For A \in |\cat{C}| \\
\quad \u{A} := \cat{C}({\bf 1}, A) \in |{\bf Set}|`$
フルカリー化、$`\cat{C}`$ のカリー化をそのまま使用：
$`(\hyp)^\wedge \in \prod_{(A, B)\in |\cat{C}|\times |\cat{C}|} {\bf Set}(\cat{C}(A, B), \u{A \to B})\\
\For A, B \in|{\bf Cat}|\\
\quad (\hyp)_{A, B}^\wedge : \cat{C}(A, B) \to \u{A \to B} = \cat{C}({\bf 1}, [A, B]) \In {\bf Set}\\
\For f : A \to B \In \cat{C}\\
\quad (\hyp)_{A, B}^\wedge(f) = f^\wedge := (f^\wedge \In \cat{C})`$
フル反カリー化、$`\cat{C}`$ の反カリー化をそのまま使用：
$`(\hyp)_\vee \in \prod_{(A, B)\in |\cat{C}|\times |\cat{C}|} {\bf Set}(\u{A \to B}, \cat{C}(A, B))\\
\For A, B \in|{\bf Cat}|\\
\quad (\hyp)^{A, B}_\vee : \u{A \to B} = \cat{C}({\bf 1}, [A, B]) \to \cat{C}(A, B) \In {\bf Set}\\
\For g : {\bf 1} \to [A, B] \In \cat{C}\\
\quad (\hyp)^{A, B}_\vee(g) = g_\vee := (g_\vee \In \cat{C})`$
外部評価写像、評価射を使って定義：
$`\Ev \in \prod_{(A, B)\in |\cat{C}|\times |\cat{C}|} {\bf Set}(\u{A \to B}\times \u{A}, \u{B}))\\
\For A, B \in |\cat{C}| \\
\quad \Ev_{A, B} : \u{A \to B}\times \u{A} \to \u{B} \In {\bf Set}\\
\For f \in \u{A \to B} = \cat{C}({\bf 1}, [A, B])\\
\For a \in \u{A} = \cat{C}({\bf 1}, A)\\
\quad f\Ev a = f \Ev_{A, B}a := \mrm{ev}_{A, B}\circ \langle f, a\rangle = \Delta_{\bf 1} ; (f \times a) ; \mrm{ev}_{A, B}`$
以上のようにして定義した $`/\cat{C}/`$ をデカルト閉圏 $`\cat{C}`$ から作られたデカルト閉・型システム〈Cartesian closed type system〉と呼ぶことにします。以下のように約束して、言葉づかいを型システムらしくします。矢印記号のオーバーロードに注意しながら読んでください。
- 圏 $`\cat{C}`$ の対象を型〈type〉と呼ぶ。
- 圏 $`\cat{C}`$ の射を関数〈function〉と呼ぶ。
- 特に、プロファイルが $`{\bf 1} \to A \In \cat{C}`$ であるポインティング射を値〈value〉またはデータ〈data〉と呼ぶ。データは関数〈射〉の一種であり、外延化 $`\u{A} = \cat{C}({\bf 1}, A)`$ の要素である。
- $`A\times B\in |\cat{C}|`$ をペア型〈pair type〉と呼ぶ。
- $`(A \to B) \in |\cat{C}|`$ を関数空間型〈function space type〉と呼ぶ。
- 関数空間型 $`(A \to B)\in |\cat{C}|`$ へのデータ $`g:{\bf 1} \to (A\to B) =[A, B] \In \cat{C}`$ を関数データ〈function data〉と呼ぶ。
- 関数 $`f: A \to B \In \cat{C}`$ のフルカリー化 $`f^\wedge`$ をフルラムダ抽象〈full lambda abstraction〉とも呼ぶ。
- 関数データ $`g:{\bf 1} \to (A \to B) \In \cat{C}`$ とデータ $`a:{\bf 1} \to A \In \cat{C}`$ に対する $`g \Ev a`$ を適用〈application〉とも呼ぶ。
ラムダ計算の抽象機械（概念的な実行エンジン）は、一般的な関数 $`f:A \to B \In \cat{C}`$ を扱えるわけではなくて、関数データとデータの適用を実行できるだけです。関数 $`f`$ の代わりに、フルカリー化した関数データ $`f^\wedge`$ を処理します。
抽象機械からは見えてないにしても、背後に完全なデカルト閉圏 $`\cat{C}`$ が存在しているので、概念的対象物としては $`\cat{C}`$ の射を自由に使ってかまいません。
矢印記号のオーバーロード解決
この記事で言いたかったことは、矢印記号のオーバーロード〈多義的使用〉はそのままにしても、オーバーロード解決（意味の判別）の手段はあるよ、ってことです。
$`f: A \to B`$ と書かれていても、それだけでは意味不明です。次のように約束します。
- $`f:A \to B \In \cat{C}`$ と書かれていたら圏論的に解釈する。
- $`f:A \to B \In /\cat{C}/`$ と書かれていたら型理論的に解釈する。
この解釈に従うと、次はすべて同じ意味です。
- $`f: A \to B \In /\cat{C}/`$
- $`f \in \u{A \to B} \In {\bf Set}`$
- $`f \in \cat{C}({\bf 1}, [A, B]) \In {\bf Set}`$
- $`f: {\bf 1} \to [A, B] \In \cat{C}`$
- $`f_\vee : A \to B \In \cat{C}`$
次も同じ意味だと言っていいかも知れません（要素とポインティング写像の同一視）。
- $`f: {\bf 1} \to \cat{C}({\bf 1}, [A, B]) \In {\bf Set}`$
次もすべて同じ意味です。
- $`f : A \to B \In \cat{C}`$
- $`f^\wedge :{\bf 1} \to [A, B] \In \cat{C}`$
- $`f^\wedge \in \cat{C}({\bf 1}, [A, B]) \In {\bf Set}`$
- $`f^\wedge \in \u{A \to B} \In {\bf Set}`$
- $`f^\wedge : A \to B \In /\cat{C}/`$
$`f : A \to B \In \cat{C}`$ と $`f: A \to B \In /\cat{C}/`$ は似てるけど少し違います。しかし、$`f : A \to B \In \cat{C}`$ と $`f^\wedge: A \to B \In /\cat{C}/`$ は同じです。もし、$`f`$ と $`f^\wedge`$ を意図的に混同するなら、$`f : A \to B \In \cat{C}`$ と $`f: A \to B \In /\cat{C}/`$ は同じとみなせます（ホントは違うけどね）。
