型理論が気持ちよく出来る圏とは - 檜山正幸のキマイラ飼育記 (はてなBlog)

$\newcommand{\cat}[1]{\mathcal{#1}}$ デカルト閉圏では、単純型理論とラムダ計算が気持ちよく出来ます。が、実用上、もう少し広い範囲の型 -- 依存型と再帰的型も扱えたほうがいいですね。依存型と再帰的型も扱えて、手で触れる感じ（あくまで“感じ”）の圏を考えましょう。

内容：

実用上必要そうな型
どんな圏ならいいのか
トレース付きデカルト圏

実用上必要そうな型

プログラミング言語でサポートされているのが望ましい型には、次のものがあるのでしょう。

幾つかの組み込み型
直積型
関数型
シグマ型
パイ型
再帰的型

組み込み型については特に議論する気はありません。整数型、ブール型、実数型（浮動小数点数型）など、目的・用途に応じて決めればいいですね。

直積型の圏論的な対応物はデカルト構造で、関数型の圏論的な対応物はデカルト閉構造です。したがって、デカルト閉圏をモデル〈意味論的世界〉にすれば、直積型と関数型はうまく記述できます。

「直積が入っているのに、なぜ直和がない？」と思われたかも知れませんが、直和はシグマ型の仲間に入れることにします。もちろん、直和型だけ切り出して単独で議論してもかまいません（好みの問題）。

シグマ型とパイ型は依存型と呼ばれる型で、直積型／直和型／関数型の一般化になっています。おおよそ、シグマ型は「たくさんの型を直和した型」、パイ型は「たくさんの型を直積した型」です。「同じ型をたくさん直積した型」は関数型になります。

以上に挙げた型に関しては、次の記事で解説しています。ここではこれ以上の説明はしません。

リスト、タプル、タグ付きデータ、関数、依存関数

リスト型やツリー型は（通常は）再帰的に定義される型です。例えば、末端〈リーフ〉に型 A の値を割り当てた二分木の型は次のように定義されます。

type BinTree<A> := A | tree{left: BinTree<A>, right: BinTree<A>}

構文は適当な擬似言語ですが、意味はわかるでしょう。このツリー型をもっと簡潔に書けば、次の方程式を満たす T です。

T = A + T×T

型に対する方程式の解であって、しかも最小のものが再帰的型になります。実用上は再帰的型がないのは辛いです。

どんな圏ならいいのか

型は圏 $\cat{C}$ の対象、関数は圏 $\cat{C}$ の射とみなすことにして、どんな $\cat{C}$ なら前節に挙げた型達をサポートできるでしょうか？

最初に、 $\cat{C}$ は完全に抽象的〈公理的〉に与えられる圏ではなくて、集合圏 ${\bf Set}$ の部分圏だと仮定します。集合に関する議論が使えないのはちと辛いからです。

それと、あまりに小さい圏だと実用性がないので、ある程度の対象を持っているとします。この条件は次の形で表現します。

任意の自然数 $n\in {\bf N}$ に対して、 $\{1, \cdots, n\} \in |\cat{C}|$

特別な場合は：

$\{\}\in |\cat{C}|$
$\{1\}\in |\cat{C}|$
$\{1, 2\}\in |\cat{C}|$

よって、空型、ユニット型〈シングルトン型〉、ブール型〈二元型〉は $\cat{C}$ に含まれます。

直積型と関数型のサポートのために、 $\cat{C}$ はデカルト閉圏だとします。デカルト閉構造は、親の圏である ${\bf Set}$ から受け継ぎます。デカルト閉構造を備えた圏 $\cat{C}$ は（記号の乱用で）次のように書けます。

$\quad \cat{C} = (\cat{C}, \times, {\bf 1}, [-,-])$

ここで：

$A, B\in |\cat{C}|$ に対して $A\times B$ が直積型となる。
${\bf 1}$ がユニット型となる。
$A, B\in |\cat{C}|$ に対して $[A, B]$ が関数型となる。

ユニット型 ${\bf 1}$ の唯一の要素は何でも（決めれば）かまいません。例えば ${\bf 1} = \{1 \}$ 。リスト型があるなら、空リストを唯一の要素にすると何かと便利です； ${\bf 1} = \{ () \}$ 。とはいえ、唯一の要素の正体を特定したくはないので ${\bf 1} = \{ * \}$ と書きます。

シグマ型とパイ型は型ファミリーに対して定義されます（「リスト、タプル、タグ付きデータ、関数、依存関数」参照）。型ファミリーのインデックス集合も $\cat{C}$ から取ることにすると、シグマ型とパイ型の存在要請は次のように書けます。

任意の $A\in |\cat{C}|$ に対する任意の型ファミリー $F:A \to |\cat{C}|$ に対して、シグマ型 $\Sigma(F)$ が存在する。
任意の $A\in |\cat{C}|$ に対する任意の型ファミリー $F:A \to |\cat{C}|$ に対して、パイ型 $\Pi(F)$ が存在する。

$A\in |\cat{C}|$ は集合なので、離散圏とみなすことができます。 $A$ を離散圏とみなせば、型ファミリーは関手です。この再解釈をすると、上記の条件は次のように書けます。

任意の $A\in |\cat{C}|$ を離散圏とみなして、任意の関手 $F:A \to \cat{C}$ に対して、余極限 $\mathrm{colim}\, F$ が存在する。
任意の $A\in |\cat{C}|$ を離散圏とみなして、任意の関手 $F:A \to \cat{C}$ に対して、極限 $\mathrm{lim}\, F$ が存在する。

離散圏からの関手の極限が存在する圏を離散完備〈complete w.r.t. discrete diagrams〉、余極限が存在するなら離散余完備〈cocomplete w.r.t. discrete diagrams〉といいます。

$\cat{C}$ に対する条件（要望、要件）をまとめると：

$\cat{C}$ はデカルト閉圏である。
$\cat{C}$ は離散余完備である。
$\cat{C}$ は離散完備である。

トレース付きデカルト圏

[追記]この節の記述には、圏 $\cat{C}$ とその外の圏（圏の圏）の混同がありますね。まったく間違ったことが書いてあるわけではないので修正はしまんせん。が、混同している部分に対する説明はいずれ別記事に書く予定です。[/追記]

再帰的型の話が残っていますね。再帰的型を定義する方程式は次の形になります。

$\quad x = h(a, x)$

$a$ は事前に決めるパラメータだとして、解 $x$ は関数 $h$ の不動点となります。このことから、上の形の方程式は（パラメータ付き）不動点方程式〈{fixed-point | fixpoint} equation〉と呼ばれます。

再帰的型がうまく定義できる圏とは、不動点方程式が解ける圏です。カザネスク／ステファネスク／ハイランド／長谷川の定理によると、不動点方程式が解けるデカルト圏はトレース付きデカルト圏〈traced cartesian category〉と同じことになります。このことについては、以下の記事を参照してください。