依存型理論に関する記事を書き始めたのですが、「うーむ、こりゃダメだ」と。型理論の用語法が混乱していて、警告や注意事項を適宜挿入するレベルでは対応できないな、と思いました。
型理論を語る言葉・言い回し・記法は、極めて曖昧です。その曖昧さを解決するルールは極めて複雑です。混沌とした／錯綜したグッチャングッチャンの表現のジャングルをかき分けて、型理論の神殿に辿り着くのは容易ではありません。
型理論のジャングルの様相と、ジャングル探索に必要な準備について述べたいと思います。無闇とたくさんの型理論があるので、そのなかで集合論的型理論を事例とします。集合論的型理論の基本概念をハッキリと説明した後で、（次の記事で）ジャングル的錯綜の報告と分析をする予定です。
この記事では、集合論的型理論の基本概念をできるだけ合理的で辻褄があった形で紹介します。ジャングル的錯綜は次の記事（2/2）で -- のつもりだったんだけど、愚痴として錯綜の話がちょいちょい混じってしまいました(苦笑)。まー、つい愚痴が出るほどに辟易しているってことです。
記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\twoto}{\Rightarrow}
\newcommand{\id}{\mathrm{id} }
%\newcommand{\u}[1]{\underline{#1} }
%\newcommand{\op}{\mathrm{op} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{－} }
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\tto}{ \mathrel{!\!\!\to} }
%\newcommand{\parto}{\supset\!\to}
\newcommand{\incto}{\hookrightarrow }
\newcommand{\T}[1]{ \text{#1} }
`$
内容：
- まず「型とはなんぞや？」をやめる！
- 集合論と集合論的宇宙
- 型理論は集合論ではない
- 単純型と依存性を持つ型
- シグマ型
- 用語法の中間まとめ
- シグマ型の第一射影と第二射影
- 依存性を持つ型のインスタンス
- パイ型
- そしてそれから
まず「型とはなんぞや？」をやめる！
型理論に入門するときに最初にやるべきことは、「型とはなんぞや？」と問う態度をあらためることです。
「ほぼワケワカラン疑似コード 」より：
集合 $`{\bf Type}`$ の要素（要素も集合）を型〈type〉と呼びます。もちろんこの呼び名は Sets-as-Types の立場でのことで、他の Xxx-as-Types の立場なら「型」の定義も変わります。
[脚注にて]「型とはなんぞや？」のような大上段に構えた疑問の提示は無意味で不毛で失礼なのでやめましょうね。絶対的な定義があるわけではなくて、あくまで立場に相対的に色々な定義があるのです。
「型とはなんぞや？」は意味のない問〈とい〉です。「型とは ～～ だとしよう」と約束をして話を始める、というだけのことです。約束をして合意する前には、“型の概念”はありません。型をどう約束するかには幾つもの流儀があります。
- Sets-as-Types
- Algebras-as-Types
- Coalgebras-as-Types
- Propositions-as-Types
- Categories-as-Types
- Logical Relations-as-Types*1
- ‥‥
「不毛」とか「無意味」という強い言葉を使っていますが、実際のところ、事前に唯一の正解があると想定して「型とはなんぞや？」と討論するのは、まったく無駄でバカげた行為です。議論の出発点は、何も決まってない状態からの「型をどう定義するか？」です。定義の仕方を“ナントカ as Types”または“Types as ナントカ”というキャッチフレーズで表すことがよくあります。ナントカに何を選ぶかにより型理論はまったく違ったものになります。
この記事では、Sets-as-Types の立場を採用します。「型とは何ですか？」に対して「型とは集合です」「集合を型だと約束しましょう」と答える立場です。この立場の型理論を集合論的型理論〈set-theoretic type theory〉と呼びましょう。集合論的依存型理論〈set-theoretic dependent type theory〉では、単なる集合を超えた型概念が出てきますが、基本となるのは「型とは集合です」という発想です。もちろん、他の立場（Xxx-as-Types）なら話がガラッと変わるでしょう。
集合論と集合論的宇宙
集合論的型理論の基盤は当然ながら集合論です。通常の（最も普及している）集合論はZFC集合論（選択公理が不要ならZF集合論）です。が、ZFC集合論をそのまま型理論のベースに使うのは不便です。「贅沢なタルスキー／グロタンディーク集合論」と「贅沢なタルスキー／グロタンディーク集合論 補遺」で述べたタルスキー／グロタンディーク集合論〈TG集合論〉が便利です。
型理論をする〈do type theory〉目的なら、タルスキー／グロタンディーク集合論の細部は不要で、ZFC宇宙〈フォン・ノイマン宇宙〉$`\msf{V}`$ *2のなかで選ばれて固定されたグロタンディーク宇宙 $`\mbf{U}\in \msf{V}`$ と、$`\mbf{U}`$ より上位のグロタンディーク宇宙 $`\mbf{U'}`$ （$`\mbf{U}\in \mbf{U'},\; \mbf{U}\subseteq \mbf{U'}`$ ）、ときにさらに上位のグロタンディーク宇宙 $`\mbf{U''}`$ （$`\mbf{U'}\in \mbf{U''},\; \mbf{U'}\subseteq \mbf{U''}`$ ）があれば十分です。
$`\mbf{U}`$ では大き過ぎる集まり（$`\mbf{U}`$ の控えめな真クラス、「贅沢なタルスキー／グロタンディーク集合論 補遺 // 集合のサイズの問題」参照）が出てきても、$`\mbf{U'}`$ に移行すれば単なる集合として扱えます。グロタンディーク宇宙の塔（「型コスモロジー： 型宇宙、型銀河、ユグドラシル」参照）の上のほうまで昇る必要性はほぼありません（稀にありますが）。
$`\mbf{U}`$ における集合族は、$`\mbf{U'}`$ では単なる関数です。$`\mbf{U}`$ におけるクラス族（「贅沢なタルスキー／グロタンディーク集合論 補遺 // 集合族とクラス族」参照）も、$`\mbf{U'}`$ では単なる関数です。$`\mbf{U}`$ 内で直積を作る操作 $`(\hyp\times\hyp)`$ や、$`\mbf{U}`$ 内でベキ集合を作る操作 $`\mrm{Pow}`$ も、$`\mbf{U'}`$ 内では単なる関数です。
グロタンディーク宇宙 $`\mbf{U}`$ から作られた集合圏 $`\mbf{Set}_{\mbf{U}}`$ を単に $`\mbf{Set}`$ と書き、グロタンディーク宇宙 $`\mbf{U'}`$ から作られた集合圏 $`\mbf{Set}_{\mbf{U'}}`$ を $`\mbf{SET}`$ と書くなら、すぐ上の段落で言ったことは次のように書けます。
- $`F`$ が $`\mbf{U}`$ の集合族〈family of sets〉とは：
$`F: X \to \mbf{U} \In \mbf{SET} \:\T{ for some }X\in \mbf{U}`$ - $`G`$ が $`\mbf{U}`$ のクラス族〈family of classes〉とは：
$`G: X \to \mrm{Pow}(\mbf{U}) \In \mbf{SET} \:\T{ for some }X\in \mbf{U}`$ - $`(\hyp\times\hyp)`$ が $`\mbf{U}`$ 内で直積を作る操作だとは：
$`(\hyp\times\hyp) : \mbf{U}\times\mbf{U} \to \mbf{U}\In \mbf{SET}`$ - $`\mrm{Pow}`$ が $`\mbf{U}`$ 内でベキ集合を作る操作だとは：
$`\mrm{Pow} : \mbf{U} \to \mbf{U}\In \mbf{SET}`$
グロタンディーク宇宙 $`\mbf{U''}`$ から作られた集合圏 $`\mbb{SET}`$ （こう書くと約束します）が登場することもたまにあります。
$`\mbf{U}\in \mbf{U'} \in \mbf{U''}`$ という3段階の階層的宇宙と、それに伴う3つの集合圏 $`\mbf{Set}, \mbf{SET}, \mbb{SET}`$ は必須な道具なので習熟しておいたほうがいいです。
型理論は集合論ではない
集合論的型理論は、型理論であって集合論そのものではありません。「集合が型となる」「型とは集合だ」と言っても、「要素がインスタンスとなる」「インスタンスとは要素だ」とは言えません。型のインスタンスは、集合の要素とは違った概念です。
集合論において、“要素と呼ばれるモノ”は存在しません。すべてのモノは集合で、所属関係における役割りとして要素が登場するのです。詳しくは次の過去記事で説明しています。
ある集合 $`a\in \mbf{U}`$ に対して、$`a\in X`$ となる集合 $`X`$（$`X\in \mbf{U}`$）は一意に決まりません。そんな集合はいくらでもあります。例えば、$`a \in \{a\}`$ です。任意の集合 $`Y`$ に対して、$`a \in Y\cup\{a\}`$ です。しかし、たいていの型理論では、インスタンスに対してその型は一意的に決まる必要があります*3。
したがって、「型は集合」を認めても「インスタンスは要素」は全然ダメです。これに対する対策は、「インスタンスは関数」とみなすことです。関数は、圏 $`\mbf{Set}`$ の射です。インスタンスの型は、関数（集合圏の射）の余域〈codomain〉だとします。こうすれば、「インスタンスに対してその型は一意的に決まる」と言えます。つまり：
$`\T{For }f \in \mrm{Mor}(\mbf{Set})\\
\quad \mrm{typeof}(f) := \mrm{cod}(f)
`$
特に、関数の域を単元集合 $`\mbf{1}`$ にすれば、次が成立します。
$`\quad \mbf{Set}(\mbf{1}, X) \cong X \In \mbf{Set}`$
つまり、域が $`\mbf{1}`$ である $`X`$ のインスタンスは、$`X`$ の要素と同一視できます。単純型理論は、域が $`\mbf{1}`$ である射〈関数 | 写像〉をインスタンスとして組み立てることができます。
依存型理論（の集合論的定式化）では、型とは単一の集合ではなくて集合族になります。この場合のインスタンスは、集合族から作ったバンドルのセクションです（後述）。依存型理論の型とインスタンスを理解するには、バンドル-ファミリー対応〈bundle-family correspondence〉が極めて重要です。バンドル-ファミリー対応については次の過去記事を参照してください。
他にもバンドル-ファミリー対応に言及している記事はたくさんあるので、興味があれば／必要があれば、以下のリストから過去記事を選んで参照してみてください。
単純型と依存性を持つ型
「型をどう定義するか？」を決めないと型の議論を始められないと注意しました。なので、「型とは集合です」と約束しました。単純型理論はこれで済むのですが、依存型理論だとそうもいきません。前節で触れたように、依存型理論の型は集合族です。単純型理論と依存型理論を同時に扱うときは、「型」が曖昧多義語になります。
「単純型理論の型を単純型、依存型理論の型を依存型と呼ぶ」と約束すると具合がいいのですが、実際には、「依存型」が「依存型理論の型」の意味で使われているとは限りません。「依存型」も人により文脈により意味が変わってしまうのです。シグマ型とパイ型（これらは後述）を総称して依存型と呼ぶ場合が一番多いでしょう。
ここでは、「依存型理論の型」をぎごちない言い方ですが依存性を持つ型〈type with dependency〉と呼ぶことにします。「依存性を持つ」は「インデックスを持つ〈indexed〉」とか「パラメータを持つ〈parameterized〉」と言っても同じです。が、プログラミング言語のジェネリックスのように“型パラメータを持つ型”に限定はしません。例えば、$`1, 2`$ をパラメータ〈インデックス〉とする“依存性を持つ型”は、2つの型 $`X_1, X_2`$ を一緒に考えたものです。
このような状況だと、「ホーア論理とホーアオートマトン 8/n ： ローヴェア、ゴグエン、ホーア、メイヤー // 造花は花か？」で述べた“用語法の乱れ”が発生します。
| 型とは単純型だ | 型とは依存性を持つ型だ |
|---|---|
| 型 | 単純型 |
| 依存性を持つ型 | 型 |
これで「型」という言葉の意味はハッキリしなくなります。「型」は文脈依存の曖昧多義語になります。
単純型は、“自明な依存性を持つ型”とみなすのが多数派ですが、自明ではない真の依存性〈proper dependency〉を持つ型だけを“依存性を持つ型”と呼びたい人がいれば、次の状況になります。
| 自明な依存性も依存性だ | 真の依存性が依存性だ |
|---|---|
| 単純型 | 単純型 |
| 自明な依存性を持つ型 | （依存性を持つとは認めない） |
| 非自明な依存性を持つ型 | 依存性を持つ型 |
| 依存性を持つ型 | 単純型または依存性を持つ型 |
このようなゴチャゴチャした状況は容易に出現します。「パンダ用法： 流転する呼称」を参照してください。
タルスキー／グロタンディーク集合論の言葉で事情をハッキリさせましょう。言葉を形式的に再定義します。
- $`X`$ が単純型だとは：
$`X \in \mbf{U}`$（$`X \in |\mbf{Set}|`$ でも同じ）であること。 - $`F`$ が（自明かも知れない）依存性を持つ型だとは：
$`F : X \to \mbf{U} \In \mbf{SET}\:\T{ for some }X\in \mbf{U}`$ であること。 - $`F`$ が自明な依存性を持つ型だとは：
$`F : \mbf{1} \to \mbf{U} \In \mbf{SET}`$ であること。 - $`F`$ が非自明な依存性を持つ型だとは：
$`F : X \to \mbf{U} \In \mbf{SET} \:\T{ where }X \not\cong \mbf{1}`$ であること。
形式的な定義をチャンと与えれば、曖昧性は解消します。仮に用語のほうは曖昧のままでも、形式的表現を使ったコミュニケーションで誤認を避けられます。もっとも、形式的表現が曖昧な事態もあるので安心はできませんが。
単純型からリスト型を作る $`\mrm{List}`$ のような“ジェネリックな型”は次のプロファイル（「ホーア論理とホーアオートマトン 3/n ： 言葉と習慣、Go言語 // 指標、シグニチャ、プロファイル、インターフェイス」参照）を持ちます。
$`\quad \mrm{List} : \mbf{U} \to \mbf{U}\In \mbf{SET}`$
これは、$`\mbf{U}`$ の集合族ではありません。しかし、$`\mrm{List}`$ に包含写像 $`\mbf{U}\incto \mbf{U'}`$ をポスト結合〈post-compose〉した関数を $`\mrm{List'}`$ とすると：
$`\quad \mrm{List'} : \mbf{U} \to \mbf{U'}\In \mbb{SET}
\:\T{ where }\mbf{U}\in \mbf{U'}
`$
つまり、$`\mrm{List'}`$ は $`\mbf{U'}`$ の集合族です。$`\mrm{List}`$ と $`\mrm{List'}`$ を同一視すれば：
$`\quad \mrm{List} : \mbf{U} \to \mbf{U'}\In \mbb{SET}
\:\T{ where }\mbf{U}\in \mbf{U'}
`$
宇宙のレベルを1つズラせば、ジェネリックな型も依存性を持つ型として扱えます。
ジェネリックな型を依存性を持つ型〈集合族〉とはみなさずに、そのまま $`\mbf{U}\to \mbf{U}`$ という関数、あるいは $`\mbf{Set}\to \mbf{Set}`$ という関手として扱ってもかまいません。が、依存性を持つ型〈集合族〉とみなすと新しい知見が得られることもあります。例えば、恒等関数 $`\id_\mbf{U} : \mbf{U} \to \mbf{U}`$ を集合族とみなしてシグマ型（次節で説明）を作ると、すべての付点集合〈pointed set〉達のクラスが得られます。
シグマ型
多くの場面で、依存型は、シグマ型／パイ型を意味しています。シグマ型／パイ型は、依存型理論を象徴する型だからです。今「型」と言いましたが、$`\sum, \prod`$（総和と総積の記号）または $`\Sigma, \Pi`$（ギリシャ文字大文字のシグマとパイ）は、型形成子〈type former〉です。（「型構成子〈type constructor〉」という言葉は後で議論します。）
型形成子〈type former〉とは、渡された型から新しい型を作り出す操作のことです。構文的には、そのような操作を表す記号（型形成子記号〈type former symbol〉）のことです。しばしば、構文的型形成子（記号）と意味的型形成子（実体）が区別されずに語られます。
意味的な（実体としての）シグマ型形成子〈Sigma type former〉は次のような関数〈集合圏の射〉です。
$`\quad \sum_{\mbf{U}, X} : \mrm{Fam}_{\mbf{U}}[X] \to \mbf{U} \In \mbf{SET}\\
\quad \T{where } \mrm{Fam}_{\mbf{U}}[\hyp] := \lambda\,X\in \mbf{U}.\mbf{SET}(X, \mbf{U})
`$
具体的な定義は：
$`\T{For }F \in \mrm{Fam}_{\mbf{U}}[X]\\
\T{ i.e. }F : X \to \mbf{U} \In\mbf{SET}\\
\quad \sum_{\mbf{U}, X} (F) := \bigcup_{x\in X}(\{x\}\times F(x))
`$
集合族の合併の操作 $`\bigcup`$ はグロタンディーク宇宙に備わっていることが保証されているので、$`\sum_{\mbf{U}, X}`$ はタルスキー／グロタンディーク集合論においてチャンと定義されます〈well-defined〉。
$`F\in \mrm{Fam}_\mbf{U}[X]`$ を、関数 $`\sum_{\mbf{U}, X}`$ に渡した“値”は $`\sum_{\mbf{U}, X}(F)`$ ですが、文脈から明らかなら下付きの $`{}_{\mbf{U}, X}`$ を省略して単に $`\sum(F)`$ と書きます。さらに丸括弧も省略して $`\sum F`$ とも書きます。
「型形成子は型を受け取って型を作り出す」と言いましたが、シグマ型形成子の引数となる（受け取る／渡される）型は集合族、つまり依存性を持つ型です。一方で、作り出す（出力する／戻す／返す）型は単純型です。ところが、単純型は自明な依存性を持つ型と同一視できるので、シグマ型形成子のプロファイルは次のようにも解釈できます。
$`\quad \sum_{\mbf{U}, X} : \mrm{Fam}_{\mbf{U}}[X] \to \mrm{Fam}_\mbf{U}[\mbf{1}] \In \mbf{SET}`$
このプロファイルだと、シグマ型形成子の引数となる型（“引数の型”ではない）も作り出す型も、両方ともに依存性を持つ型だと言えます。今後、より一般的なケースを考えるには、シグマ型形成子の引数も戻り値もどちらも依存性を持つ型だと思ったほうが整合性があります。
用語法の中間まとめ
ここまででも既に、用語法はだいぶややこしくなっています。注意点をまとめておきます。全般的に言えることは、記号と実体、定数と関数、関数と関数値、引数と引数型、戻り値と戻り値型など、区別して当然なことを実際にはあまり区別してない、ということです*4。
- 「型とはなんぞや？」の答えが事前に決まっているわけではない。定義して約束する必要がある。この記事では、「型とは集合である」としている。
- 原則としては「型とは集合である」としても、依存型理論の型は集合族となる。「型」が集合であるか集合族であるかは文脈で判断するか、または「単純型」と「依存性を持つ型」のように呼び分ける。
- シグマ型形成子の実体は、集合族〈依存性を持つ型〉に集合〈単純型〉を対応させる関数*5である。
- シグマ型形成子の記号として、'$`\sum`$' や '$`\Sigma`$' を使う。記号とその実体は別物だが、しばしば意図的に混同される。
- 関数としてのシグマ型形成子 $`\sum_{\mbf{U}, X}`$ の引数値は依存性を持つ型〈集合族〉、引数型は依存性を持つ型〈集合族〉達の集合だから $`\mrm{Fam}_{\mbf{U}}[X]`$ である。
- 関数としてのシグマ型形成子 $`\sum_{\mbf{U}, X}`$ の戻り値は単純型〈集合〉、戻り値型は単純型〈集合〉達の集合だから $`\mbf{U}`$ である。
- 関数としてのシグマ型形成子に実引数〈actual argument〉 $`F`$ を渡して得られる値である型 $`\sum(F) = \sum_{\mbf{U}, X}(F)`$ をシグマ型〈Sigma type〉と呼ぶ。
- シグマ型形成子が作り出した結果（関数値）としてのシグマ型は単純型〈集合〉である。シグマ型を自明な依存性を持つ型とみなすこともある。
- 上記のことを「シグマ型は単純型である」とも表現できる。が、「シグマ型は依存型であり単純型ではない」とも言える*6。
- 一般的には（一般論はまだ述べてないが）シグマ型（シグマ型形成子の値）が“非自明な依存性を持つ型”となることもある。
- シグマ型形成子（関数）とシグマ型（関数値）を区別しないことがある。
- 構文と意味を区別しないことがある。「シグマ型」がシグマ型形成子記号を表すこともあれば、シグマ型形成子（実体）を意味することもある。
「型構成子〈type constructor〉」という言葉がありますが、これは厄介な言葉です。型構成子が型形成子と同義なこともありますが、帰納的に定義される型のデータ構成子〈data constructor〉を型構成子と呼ぶことがあります*7。「データ」なのに、なんで「型」なんだ？ とツッコミたくなりますが、実際に使われている用法なのでしょうがないです。
帰納的に定義される型のデータは、値／項とも呼びます。したがって、次の4つが同義語となるケースがあります。
- 型構成子〈type constructor〉
- データ構成子〈data constructor〉
- 値構成子〈value constructor〉
- 項構成子〈term constructor〉
単に「構成子〈constructor〉」と言った場合、解釈は次の2つの可能性があります。
- 型形成子と同義（僕は、「型構成子＝型形成子」（同義語）として使っています）
- データ構成子と同義
オブジェクト指向の文脈での構成子〈コンストラクタ〉はまた別な意味を持ちます -- 文脈が違えば意味が変わるのは当然ですが。
こういう混乱した用語法が、型理論の特徴と伝統なのかも知れません（皮肉で言ってます）。過去記事でも愚痴っています。
- 型理論ってば （2012年） 人によりコミュニティにより違う様々な言葉が使われるので、結果的に有象無象の用語達が出現してしまう、という話。
- 型理論周辺、何で混乱するのか？（2025年） 型理論は、構造的に混乱誘発的らしい、という話。
シグマ型の第一射影と第二射影
集合論的単純型理論（デカルト閉圏としての集合圏の理論）を一通り習った人が、集合論的依存型理論に入って最初にやるべきことは、シグマ型（シグマ型形成子により作られた型）をチャンと理解することです。このとき、次の見方・考え方が役に立ちます。
- シグマ型を、関係〈ニ項関係〉とみなす。
- 関係に伴う第一射影と第二射影をチャンと意識する。
集合 $`A`$ から集合 $`B`$ への関係〈relation〉（正確にはニ項関係） $`R`$ とは、部分集合 $`R \subseteq A\times B`$ のことです。集合 $`R`$ だけを与えられても $`A, B`$ を再現できない（$`R\subseteq X\times Y`$ となる $`X, Y`$ はいくらでもある）ので、三つ組 $`(A, B, R)`$ が関係です。が、記号の乱用により $`R = (A, B, R)`$ と書きます。
$`(\mbf{N}, \mbf{N}, \emptyset)`$ や $`(\mbf{N},\mbf{1}, \emptyset)`$ は関係の例です。記号の乱用を使って書くと $`\emptyset = (\mbf{N}, \mbf{N}, \emptyset)`$ 、 $`\emptyset = (\mbf{N},\mbf{1}, \emptyset)`$ です。この例から、記号の乱用がいかにトンチンカンなデタラメになるかが分かるでしょう。まー、それでも記号の乱用は使うんですけどね。
シグマ型形成子とシグマ型の定義（前節）から、次が言えます。
$`\quad \sum_{\mbf{U}, X}(F) \subseteq X \times \bigcup_{x\in X} F(x)`$
簡略に書けば：
$`\quad \sum F \subseteq X \times \bigcup F`$
これは、シグマ型 $`\sum F`$ が、集合 $`X`$ から 集合 $`\bigcup F`$ への関係であることです。
一般に、関係 $`R`$ は $`R\subseteq A\times B`$ なので、関係 $`R`$ の要素は必ずペア〈順序ペア | ordered pair〉です。シグマ型は関係なので、シグマ型の要素はペアです。シグマ型の要素であるペアを依存ペア〈dependent pair〉と呼びます。
次の2つの言明は同じことです。
- $`(x, y)\in X\times \bigcup F`$ は、シグマ型 $`\sum F`$ の依存ペアである。
- $`x \in X \land y \in F(x)`$
$`(x, y)\in X\times \bigcup F`$ が $`\sum F`$ の依存ペアであることを明示するために次のような書き方もします。
$`\quad (x\in X, y\in F(x))`$
依存ペアは、シグマ型の要素のことなので、事前にシグマ型（シグマ型形成子で作られた型）が指定されないと「依存ペア」という言葉は意味を持ちません。
一般論から記号を準備します； 直積集合 $`A\times B`$ に対して、その第一射影〈{first | primary} projection〉と第二射影〈{second | secondary} projection〉を次のように書きます。
$`\quad \pi^{A, B}_1 : A\times B \to A \In \mbf{Set}\\
\quad \T{where }\pi^{A, B}_1 ( (x, y)) = x
`$
$`\quad \pi^{A, B}_2 : A\times B \to B \In \mbf{Set}\\
\quad \T{where }\pi^{A, B}_2 ( (x, y)) = y
`$
一般的な習慣ではありませんが、ここでは、$`\pi^{A, B}`$ と書いたら $`\pi^{A,B}_1`$ のことだとします。用語としては、単に「射影〈projection〉」と言ったらそれは「第一射影」のことです。
$`R\subseteq A\times B`$ が関係のとき（正確には $`(A, B, R)`$ が関係）、第一射影／第二射影の $`R`$ への制限〈restriction〉は次のように書きます。
$`\quad \pi^{A, B}_1|_R : R \to A \In \mbf{Set}`$
$`\quad \pi^{A, B}_2|_R : R \to B \In \mbf{Set}`$
制限を縦棒で表すのはよく使われる記法です。
チャンと書くと面倒なので略記が使われます。
- $`\pi^{A, B}_1, \pi^{A, B}_2`$ は $`\pi_1, \pi_2`$ と略記されかも知れない。
- $`\pi_1`$ は $`\pi`$ と略記されかも知れない。
- $`\pi^{A, B}_1|_R, \pi^{A, B}_2|_R`$ は $`\pi_1|_R, \pi_2|_R`$ と略記されかも知れない。
- $`\pi_1|_R`$ は $`\pi|_R`$ と略記されかも知れない。
- $`\pi|_R`$ は $`\pi`$ と略記されかも知れない。
略記は曖昧性を生み、解釈を困難にします。しかしそれでも略記は使われるので、略記される（曖昧化される）かも知れないという事実は知っておくべきです。
さて、話をシグマ型に戻すと、シグマ型の制限された第一射影は次のように書かれます。
- $`\pi^{X, \bigcup F}_1|_{\sum F} : \sum F \to X \In \mbf{Set}`$
- $`\pi_1|_{\sum F} : \sum F \to X \In \mbf{Set}`$ （上付きの $`{}^{X, \bigcup F}`$ を省略）
- $`\pi|_{\sum F} : \sum F \to X \In \mbf{Set}`$ （下付きの $`{}_1`$ を省略）
- $`\pi : \sum F \to X \In \mbf{Set}`$ （制限を表す $`|_{\sum F}`$ を省略）
シグマ型の制限された第一射影を、シグマ型の標準射影〈canonical projection〉と呼びます。シグマ型には、標準射影が組み込まれていると考えます。
シグマ型の制限された第二射影は忘れられがちですが、潜在的に重要な役割りを持っています。潜在的なので明示的な言及がされず、これがまた曖昧性を生み出したりします。
関係としてのシグマ型と、それに付随する第一射影・第二射影をまとめて描くと次の図式になります。この図式を常に意識しておくとよいでしょう。
$`\T{For } F: X \to \mbf{U} \In \mbf{SET}\\
\quad \xymatrix {
{X \times \bigcup F}
&{\sum F} \ar[d]_{\pi} \ar[r]^{\pi_2}
\ar@{^{(}->}[l]
&{\bigcup F}
\\
{}
&X
}\\
\quad \In \mbf{Set}
`$
$`\pi`$ が $`\pi^{X, \bigcup F}_1|_{\sum F}`$ の略記で、$`\pi_2`$ が $`\pi^{X, \bigcup F}_2|_{\sum F}`$ の略記であることもチャンと認識しましょう。
略記や省略によりいくら簡潔に表現されようが、その背後にある（それなりに複雑な）構造を忘れてはいけない、ということです。
依存性を持つ型のインスタンス
集合論的単純型理論では、「型は集合」はよいが「インスタンスは要素」は全然ダメでした。集合論的依存型理論では、「型は集合族」と定義しました。では、インスタンスは何なのでしょう？ 既に触れたように、集合論的依存型理論における型のインスタンスはセクション〈section〉です。
一般的に、関数〈写像〉 $`f:A \to B \In \mbf{Set}`$ のセクション〈section〉 $`s`$ とは、次のような関数です。（以下で、$`s;f = f\circ s`$ です。）
- $`s: B \to A \In \mbf{Set}`$
- $`s;f = \id_B`$
もとになる関数 $`f`$ を決めないとセクションという概念は決まりません。
$`f: A\to B\In \mbf{Set}`$ のセクションの全体からなる集合を $`\mrm{Sect}(f:A \to B)`$ と書きます。（以下の $`\mrm{Map}(\hyp, \hyp)`$ は $`\mbf{Set}(\hyp, \hyp)`$ と同義です。）
$`\quad \mrm{Sect}(f:A \to B) := \{
g\in \mrm{Map}(B, A) \mid g;f = \id_B \}
`$
定義から当然に：
$`\quad \mrm{Sect}(f:A\to B) \subseteq \mrm{Map}(B, A)`$
次の3つの言明は同値です*8。
- $`f:A \to B`$ にセクションが存在する。
- $`\mrm{Sect}(f:A \to B) \ne \emptyset`$
- $`f`$ は全射である。
セクションという概念を、シグマ型の標準射影に適用しましょう。$`F: X \to \mbf{U}\In \mbf{SET}`$ を集合族〈依存性を持つ型〉だとします。$`\pi : \sum F \to X`$ は（シグマ型の）標準射影です。標準射影のセクション達の集合は：
$`\quad \mrm{Sect}(\pi : \sum F \to X)`$
このセクション達の集合が、$`F`$ のパイ型〈Pi type〉です。が、しばらくのあいだは“標準射影のセクション達の集合”と呼ぶことにします。呼び名はともかくとして、集合 $`\mrm{Sect}(\pi : \sum F \to X)`$ は、依存型理論の主役です。
今の我々の立場（Sets-as-Types）では、“集合族”と“依存性を持つ型”は同じ概念の別名でした。集合族 $`F`$ に対する集合 $`\mrm{Sect}(\pi : \sum F \to X)`$ の要素を、依存性を持つ型〈集合族〉 $`F`$ のインスタンス〈instance〉と呼びます。言い方を変えると、依存性を持つ型のインスタンスとは、シグマ型のセクションのことです。
このインスタンスの定義を見て「えっ、なんで？」と思うかも知れません。この定義にたどり着くまでに、歴史的紆余曲折はあったと思います。今現在、最も扱いやすいインスタンスの定義はセクションです。
この節の残りで、依存性を持つ型〈集合族〉のインスタンスが、単純型〈集合〉のインスタンスと整合的であることを見ておきましょう。
単純型とは集合のことでした。単純型 $`X`$ のインスタンスとは、要素のポインティング関数でした。要素 $`a\in X`$ のポインティング関数を $`a^\sim`$ と書きます。（以下で、$`\mbf{1} = \{0\}`$ としています。）
$`\quad a^\sim : \mbf{1} \to X \In \mbf{Set}\\
\quad \T{where }a^\sim (0) = a
`$
単純型 $`X`$ を依存性を持つ型だとみなすときは、次のような“自明な依存性を持つ型”と考えるのでした。
$`\quad X^\sim : \mbf{1} \to \mbf{U} \In \mbf{SET}\\
\quad \T{where } X^\sim(0) = X
`$
関数 $`X^\sim`$ は、集合から宇宙への関数なので集合族です。集合族、すなわち依存性を持つ型です。依存性を持つ型 $`X^\sim`$ のシグマ型を作りましょう -- シグマ型形成子を適用することですね。
$`\quad \sum X^\sim := \bigcup_{y\in \mbf{1}} \{y\} \times X^\sim(y)`$
$`\mbf{1} = \{0\}`$ だったので、$`y\in \mbf{1}`$ となる $`y`$ は $`0`$ だけ。したがって、次のようになります。
$`\quad \sum X^\sim := \{0\} \times X^\sim(0) = \{0\}\times X = \mbf{1}\times X`$
$`X^\sim`$ のシグマ型は直積 $`\mbf{1}\times X`$ となり、シグマ型の標準射影は直積の第一射影そのものとなります。
$`\quad \pi = \pi|_{\sum X^\sim} = \pi^{\mbf{1}, X}_1 \; : \mbf{1}\times X \to \mbf{1} \In \mbf{Set}`$
前節で述べた“基本図式”を描けば、次のようです。
$`\T{For } X^\sim: \mbf{1} \to \mbf{U} \In \mbf{SET}\\
\quad \xymatrix {
{\mbf{1} \times X}
&{\mbf{1} \times X } \ar[d]_{\pi} \ar[r]^{\pi_2}
\ar@{^{(}->}[l]
&{X}
\\
{}
&\mbf{1}
}\\
\quad \In \mbf{Set}
`$
ここで、$`\pi = \pi_1`$ で、包含写像は実際は恒等写像です。
依存性を持つ型〈集合族〉 $`X^\sim`$ のインスタンスとは、標準射影〈第一射影〉 $`\pi:\mbf{1}\times X \to \mbf{1}`$ のセクション $`s`$ でした。
$`\quad s: \mbf{1} \to \mbf{1}\times X \In \mbf{Set}\\
\quad \T{where } s; \pi = s; \pi_1 = \id_{\mbf{1}}
`$
この状況は以下の図式が可換であることです。
$`\T{For some }a\in X\\
\quad \xymatrix{
\mbf{1}
&{\mbf{1} \times X} \ar[l]_{\pi_1}\ar[r]^{\pi_2}
&X
\\
{}
&\mbf{1} \ar[u]|s \ar[ul]^{\id_{\mbf{1}}}
\ar[ur]_{a^\sim}
}\\
\quad \T{commutative }\In \mbf{Set}
`$
$`s`$ の第一成分 $`s;\pi_1`$ は、$`s`$ がセクションであることから $`\id_{\mbf{1}}`$ です（この特殊状況では、$`\id_{\mbf{1}}`$ 以外の射はありませんが）。$`s`$ の第二成分 $`s;\pi_2`$ は、$`\mbf{1}`$ からの関数〈写像〉なので、適当な要素 $`a\in X`$ のポインティング関数になっています。従って、$`s`$ の成分表示（第一成分と第二成分のデカルトペアリング表示）は次のようになります。
$`\quad s = \langle s;\pi_1, s;\pi_2\rangle = \langle \id_{\mbf{1}}, a^\sim\rangle`$
これは、セクション $`s`$ が「第二成分だけで決まる」ことを意味します。その第二成分はポインティング関数です。ポインティング関数は要素で決まります。したがって、次の規準的同型〈canonical isomorphism〉があります。
$`\quad \mrm{Sect}(\pi: \mbf{1}\times X \to \mbf{1}) \cong \mrm{Map}(\mbf{1}, X)
\cong X
`$
次の3つは一対一に対応します。
- 標準射影〈第一射影〉 $`\pi: \mbf{1}\times X \to \mbf{1}`$ のセクション
- $`X`$ へのポインティング関数
- $`X`$ の要素
標準射影のセクションは、型理論の言葉では“自明な依存性を持つ型のインスタンス”と呼ぶのでした。ポインティング関数は、型理論の言葉では“単純型のインスタンス”と呼ぶのでした。上記の一番目と二番目が一対一対応することは、次のように言えます。
- “自明な依存性を持つ型のインスタンス”と“単純型のインスタンス”は一対一対応する。
これにより、単純型と自明な依存性を持つ型は同一視可能です。もう少し正確に言うと、単純型を自明な依存性を持つ型とみなす標準的な方法があります。この“みなし〈変換〉”により、単純型のインスタンスと自明な依存性を持つ型のインスタンスは一対一対応します。
パイ型
既に触れたように、パイ型とはセクションの集合のことです。もっとハッキリと定義するために、パイ型形成子から定義しましょう。パイ型形成子〈Pi type former〉$`\prod_{\mbf{U}, X}`$ とは次のような関数です。
$`\quad \prod_{\mbf{U}, X} : \mrm{Fam}_\mbf{U}[X] \to \mbf{U} \In \mbf{SET}\\
\T{For }F \in \mrm{Fam}_\mbf{U}[X]\\
\T{ i.e. }F : X \to \mbf{U} \In \mbf{SET}\\
\quad \prod_{\mbf{U}, X}(F) := \mrm{Sect}(\pi : \sum F \to X)
`$
関数としてのパイ型形成子に実引数〈actual argument〉 $`F`$ を渡して得られる値である型 $`\prod(F) = \prod_{\mbf{U}, X}(F)`$ をパイ型〈Pi type〉と呼びます。パイ型（パイ型形成子の値）は単純型ですが、単純型は自明な依存性を持つ型とみなせることに注意してください。
集合としてのパイ型の要素はセクションです。セクションは関数なので、パイ型は関数空間だとみなせます。パイ型の要素としてのセクションを依存関数〈dependent function〉と呼ぶこともあります。標語的に言えば、パイ型は依存関数空間型です。
シグマ型 $`\sum F`$ は、依存ペア達の集合でした。そして、通常の直積集合 $`X\times \bigcup F`$ に埋め込めます。パイ型 $`\prod F`$ は、依存関数達の集合です。そして、通常の関数空間〈関数集合 | 写像集合〉に埋め込めます。ただし、二種類の埋め込みがあります。
- $`\prod F \incto \mrm{Map}(X, \sum F)`$
- $`\prod F \to \mrm{Map}(X, \bigcup F)`$
一番目は、定義から自明な包含写像です。二番目は、セクションの第二成分を取ることによる埋め込み写像です。この二種類の埋め込みはほとんど同じですが微妙に違います。「ほとんど同じだが微妙に違う」はたいていトラブルの原因になります。微妙な違いに敏感になったほうがいいです。
パイ型が定義できたので、依存性を持つ型〈集合族〉 $`F`$ のインスタンスに別定義を追加できます。$`F`$ のインスタンスとは：
- シグマ型 $`\sum F`$ の（標準射影の）セクション
- パイ型 $`\prod F`$ の（集合としての）要素
シグマ型 $`\sum F`$ を集合とみての要素〈依存ペア〉は、$`F`$ のインスタンスとは呼ばないので注意してください。しかし、依存ペアは、単純型としてのシグマ型 $`\sum F`$ のインスタンスにはなります。「依存性を持つ型のインスタンス〈セクション〉、単純型のインスタンス〈ポインティング関数〉、集合の要素」の三者のあいだの関係と違いには十分注意してください。
シグマ型には標準射影が内在的に〈組み込みで〉備わっていました。標準射影は、依存ペアの第一成分を取り出す写像です。パイ型にも有意義な写像が備わっているでしょうか？ パイ型の要素は関数なので、評価写像〈evaluation map〉が備わっています。左から引数を渡す $`\mrm{ldev}`$（left dependent evaluation）なら次のようです。
$`\quad \xymatrix {
{X \times \prod F} \ar[d]_{\pi_1}
\ar[r]^{\mrm{ldev}}
&{\sum F} \ar[d]^{\pi}
\\
X \ar@{=}[r]
&X
}\\
\quad \T{commutative }\In \mbf{Set}
`$
依存関数の評価写像は重要ですが、ここではこれ以上は踏み込まないことにします。
そしてそれから
この記事で、次のような集合論的型理論の基本概念を説明しました。
- 単純型
- 単純型のインスタンス
- 依存性を持つ型
- シグマ型形成子
- シグマ型
- シグマ型の標準射影
- 依存性を持つ型のインスタンス
- パイ型形成子
- パイ型
上記の言葉は、この記事と次の記事では標準として使います。しかし、この標準はローカル標準です。実際に使われている用語法・記法は、錯綜したものです。次の記事で、その錯綜を分析します。
*1:"Logical Relations as Types: Proof-Relevant Parametricity for Program Modules", Jonathan Sterling, Robert Harper
*2:「贅沢なタルスキー／グロタンディーク集合論 // グロタンディーク宇宙」から、フォン・ノイマン宇宙をサンセリフ体の '$`\msf{V}`$' で書くことにしました。
*3:インスタンスの型が複数あってもよい型理論もありますが、その場合でも“最小の型”は一意的に、あるいは同型を除いて一意的に決まることを要求します。
*4:区別すべきものを区別しないことは、型理論に限らず広く見られる現象です。これは、「一度区別できた後では、いちいち区別するのがめんどくさくなる」という誰でもが持っている横着さのせいでしょう。
*5:集合が値、集合族が関数なので、シグマ型形成子は汎関数に相当します。
*6:こういう、一見矛盾するような文言が出現してしまうことが、曖昧な用語法の困ったところです。
*7:データ構成子の場合、構文論と意味論の区別はしにくいです。「データ構成子記号をそのままセマンティクスにも使う」ことが多いです。
*8:選択公理を仮定しています。
