このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

依存型と総称型の圏論的解釈

雑記／備忘

去年〈2020年〉の10月に「多相関数と依存型をちゃんと理解しよう」という記事を書いたのですが、基本的な用語を間違っていました。[追記]いや、間違いでもないようです。この記事のコメント欄参照。[/追記]

記号 間違った 呼び方 1 正しい 呼び方 2 別な呼び方
$`\prod`$ 依存積型 依存指数型／依存関数型 パイ型
$`\sum`$ 依存和型 依存積型 シグマ型

$`\prod`$ だから積、$`\sum`$ だから和だろうと安直に思い込んでいて確認しなかったのです。ごめんなさい*1。[追記]「ごめんなさい」は、間違いかどうかの確認もちゃんとしてなかったことです。[/追記]

正しく別な言い方は、$`\prod_{x:X}F(x)`$ は非依存指数型（普通の指数型）の依存版だから依存指数型、$`\sum_{x:X}F(x)`$ は非依存積型（普通の積型）の依存版だから依存積型というネーミングでした。ですが、なんかまた間違える混乱する気がするので、今後は見たままのパイ型／シグマ型を使おうと思います。

さてこの記事では、パイ型とシグマ型を圏論的に扱ってみます。また、依存型と総称型の区別と境界線がよく分からない（たぶん人によりけり）ので、自分〈檜山〉なりの整理を試みます。

内容：

要旨と注意

デカルト閉圏Cを舞台として型理論の話をします。

Cの対象を“型”と呼びます。Type := |C| ってことです。デカルト閉圏Cの射を“関数”と呼びます。注意すべきは、関数型プログラミング言語で「関数」と言っているモノは、今言った「関数＝Cの射」ではないことです。関数型プログラミングの関数の実体は関数データです。関数データとは、デカルト閉圏Cにおける f:1 → [A, B] in C という形の射です。

関数 F:A → B in C と関数データ f:1 → [A, B] in C が区別しにくく混乱しがちなのは同じ矢印記号「→」が使われているからでしょう（矢印記号は他にも色々な意味で使われます*2）。さらに、関数型プログラミング言語で矢印を使っているのは意図的で、関数と関数データを同一視したいからです。

直感的・雰囲気的な理解には、関数と関数データを同一視するのが便利です。しかし、デカルト閉圏Cで、型や関数に対する意味論を正確に記述しようとするときは、関数 F:A → B in C と関数データ f:1 → [A, B] in C を区別する必要があります。ここではもちろん区別します。矢印「→」は射のプロファイルに使い、指数対象〈関数対象 | 関数型〉を表すには [A, B] または BA を使います。

「多相関数と依存型をちゃんと理解しよう」において、型ファミリーと型カインドという概念を導入しました。これらを若干一般化して、デカルト閉圏Cに対するC-ファミリー〈C値ファミリー〉とC-カインド〈C内カインド〉を定義します（後述）。

C-ファミリーとは、Cに値を取る（Cを余域とする）関手のことです。C-カインドとは、Cの部分圏です。それだけです。「ファミリー＝関手」「カインド＝部分圏」という同義語をあえて導入するのは、型理論的フレーバーを持たせるためです。フレーバー〈香り | 雰囲気〉だけの違いなので、中身〈意味的実体〉は同じです。

ファミリーとカインドを中心として型理論の話をします。ファミリーとカインドの議論は関手と部分圏の議論なので、圏論の普通の手法を普通に使います。

ファミリーとカインド

Setを集合圏とします。Cは集合圏Setの部分圏であり、Setのデカルト閉構造をそのまま受け継いでデカルト閉圏になっているとします。Cの例としては、空集合0と単元集合1だけを対象とする圏や、すべての有限集合を対象とする圏があります。Set自身をCに取ってもかまいません。

もう少し一般化したいのならば、集合圏Setへの構造忘却関手（忠実関手、埋め込みである必要はない）を持つデカルト閉圏まで許すといいでしょう。こうすると、CとしてωCPO〈可算完備順序集合〉の圏なども取れます。今日は、C ⊆ Set の前提で考えます。

CATは、必ずしも小さくはない圏を許す“圏の圏”とします。Set∈|CAT| です。圏と対象だけでなく自然変換も考えるので、CATは2-圏です。CATに関して次の記法を使います（下図も参照）。この記事で使ってない記法もあるけど、まとめとして。

関手 F: D → C in CAT
自然変換（2-射） α::F ⇒ G:D → C in CAT
自然変換の成分 αX:F(X) → G(X) in C
関手圏 [D, C] in CAT
自然変換（別記法） α:F → G in [D, C]
自然変換の縦結合 α;β::F ⇒ H:D→C in CAT
関手の結合 F＊J:D → B in CAT
自然変換の横結合 α＊γ::F＊J ⇒ G＊K:D→B in CAT

$`\newcommand{\cat}[1]{ \mathcal{#1} }%
\xymatrix@R-1pc {
{}
&*{\scriptstyle F} \ar@{=>}[d]^{\alpha}
&
\\
*{\cat{D}} \ar@/^18pt/[rr] \ar[rr]|G \ar@/_18pt/[rr]
& *++{} \ar@{=>}[d]^{\beta}
& *{\cat{C}}
\\
{}
&*{\scriptstyle H}
&
}\\
\xymatrix {
*{\cat{D}} \ar@/^10pt/[rr]^F \ar@/_10pt/[rr]_G
& *{\Downarrow\alpha}
& *{\cat{C}} \ar@/^10pt/[rr]^J \ar@/_10pt/[rr]_K
& *{\Downarrow\gamma}
&*{\cat{B}}
}
`$

C-ファミリー〈C-family〉は、圏Cを余域とする関手 F:D → C in CAT のことです。関手をファミリーと呼ぶとき、関手の域である圏をインデックス域〈{index | indexing} domain〉またはパラメータ域〈{parameter | parameterization} domain〉と呼びます。

C-ファミリー F:D → C in CAT のインデックス域Dが離散圏のとき、Fは、Cの対象のインデックス付きファミリー〈添字族〉になります。Cの対象を“型”と呼ぶなら型ファミリーですね。

Cの部分圏をC-カインド〈C-kind〉と呼びます。C-カインドが離散圏なら、Cの対象＝型の集まりなので、C-カインドは“型の型”と言えます。離散圏ではないC-カインドも考えますが。

反レイフィケーションとパイ型

次のような関手 J:C → CAT を考えます。

  • A∈|C| に対して、J(A) := (離散圏とみなした A)
  • f:A → B in C に対して、J(f) := (離散圏のあいだの関手とみなした f)

Cは集合圏Setの部分圏としていたので、この定義は意味があります。Jは、圏Cを“圏の圏”CATにスッポリと埋め込む関手になっています。この関手 J:C → CAT を反レイフィケーション〈dereification〉と呼ぶことにします。Cの外にあるナニモノカをC内に落とし込む操作がレイフィケーション〈物象化〉なので、Jはその逆の操作ということで「反」を付けています。後でレイフィケーションも出てきます。

以下、反レイフィケーションを使ってパイ型を定義します。

対象 A∈|C| に対して次のC-ファミリーを考えます。

  • F:J(A) → C in CAT

J(A) は小さい離散圏なので、関手Fは、集合でインデックスされたCの対象族と同じことです。しかし、関手として扱うことが重要です。

ファミリー＝関手 F:J(A) → C の極限（極限錐の頂点対象）を Lim(F) あるいは LimJ(A)(F) と書きます。この極限を、C-ファミリーFのパイ型〈Pi type〉と呼びます。定義より、パイ型は（存在すれば）同型を除いて一意に決まります。

関手の極限に馴染みがない方は次の記事を参照してください。

パイ型＝関手の極限は、必ずしも存在するとは限りません。そこで、パイ型が常に存在するような圏を考えます。任意の対象 A∈|C| と任意の関手 F:J(A) → C に対して極限が存在するような圏を自己完備〈self complete〉な圏と呼ぶことにします。自己完備な圏なら、パイ型を自由に作れます。先に出したCの例である、0と1だけの圏、有限集合の圏、集合圏はいずれも自己完備です。

以下、Cは自己完備な圏だと仮定します。すると、任意のファミリー〈関手〉 F:J(A) → C in CAT に対してパイ型〈極限〉を作れます。パイ型の表記には色々な書き方があります。

  1. $`\Pi(F)`$
  2. $`\Pi_A(F)`$
  3. $`\prod_{a:A}F(a) `$
  4. $`\prod a:A.F(a)`$

大文字ギリシャ文字 $`\Pi`$ を使うか総積記号 $`\prod`$ を使うか、a:X が下付きか普通サイズかなどのバリエーションがあります。コロンの代わりに集合の所属記号'∈'も使われますが、型理論だとコロンが主流でしょう。書き方のバリエーションに惑わされないように注意してください。二番目の書き方でパイ型の定義を書けば：

$`\Pi_A(F) := Lim_{J(A)}(F) `$

Fの極限対象である $`\Pi_A(F) `$ からの射影は $`\pi(F)_a: \Pi_A(F) \to F(a) \mbox{ for }a\in A`$ と書きましょう。J(A) が離散圏なので、要求される可換図式はありません。

XをCの任意の対象、$`\psi_a: X \to F(a) \mbox{ for }a \in A `$ を“Xを頂点とする錐〈cone〉”だとします。極限の定義から、$`f:X → \Pi_A(F) \mbox{ in }\mathcal{C}`$ が一意的に定まり、次の図式を可換にします。

$`\require{AMScd}
\forall a\in A.\\
\begin{CD}
X @>{f}>> \Pi_A(F) \\
@V{\psi_a}VV @VV{\pi(F)_a}V \\
F(a) @= F(a)
\end{CD}\\
\mbox{commutes in }{\mathcal{C}}
`$

逆に、$`f:X \to \Pi_A(F)`$ があれば、$`\psi_a := f;\pi(F)_a`$ と定義して $`\psi_a:X \to F(a) \mbox{ for }a\in A`$ が再現します。以上の事実は極限の定義そのものですが、依存型理論として重要な事実です。

特に、XがCの終対象1のときは、次のようになります。

$`
\forall a\in A.\\
\begin{CD}
{\bf 1} @>{f}>> \Pi_A(F) \\
@V{\psi_a}VV @VV{\pi(F)_a}V \\
F(a) @= F(a)
\end{CD}\\
\mbox{commutes in }{\mathcal{C}}
`$

このとき、f はパイ型である集合 $`\Pi_A(F)`$ の要素〈データ〉*3とみなせます。つまり、終対象を頂点としてFを底面とする錐はパイ型の要素〈データ〉を一意に定めます。逆に、パイ型の要素は錐を定めます。この場合の錐は a∈A に依存した型 F(a) の要素達です。

シグマ型

シグマ型はパイ型の双対になり、話はパイ型と並行に進みます。C-ファミリー F:J(A) → C in CAT があるとき、関手としての余極限がシグマ型〈Sigma type〉です。

$`\Sigma_A(F) := Colim_{J(A)}(F) `$

シグマ型が自由に作れるためには、圏Cが自己余完備〈selef cocomplete〉である必要があります。

Fの余極限対象である $`\Sigma_A(F) `$ からの入射〈injection〉は $`\iota(F)_a: F(a) \to \Sigma_A \mbox{ for }a\in A`$ と書きます。J(A) が離散圏なので、要求される可換図式はありません。

YをCの任意の対象、$`\omega_a: F(a) \to Y \mbox{ for }a \in A `$ を“Yを余頂点とする余錐〈cocone〉”だとします。余極限の定義から、$`g:\Sigma_A(F) → Y \mbox{ in }\mathcal{C}`$ が一意的に定まり、次の図式を可換にします。

$`
\forall a\in A.\\
\begin{CD}
F(a) @= F(a) \\
@V{\iota(F)_a}VV @VV{\omega_a}V \\
\Sigma_A(F) @>{g}>> X \\
\end{CD}\\
\mbox{commutes in }{\mathcal{C}}
`$

逆に、$`g:\Sigma_A(F) \to Y`$ があれば、$`\omega_a := \iota(F)_a;g`$ と定義して $`\omega_a:F(a) \to Y \mbox{ for }a\in A`$ が再現します。

依存型理論の記法

依存型理論では、次のような、型に関する推論規則（の一例）が使われます。

$`
\xymatrix@R-1.8pc@C-2pc{
{}
&*{A:Type}
&
&*{a:A \vdash F(a):Type}
&
\\
{}\ar@{-}[rrrr]
&
&
&
&
\\
{}
&
&* {\prod_{a:A}F(a) : Type}
&
}
`$

ブログシステムとWebページの表示の都合（下の補足参照）から、上の図を次のような記法で書くことにします。

$`\require{color}%
\newcommand{\Keyword}[1]{ \textcolor{green}{ \bf #1} }%
\newcommand{\When}{\Keyword{when\:\:} }%
\newcommand{\And}{ \Keyword{\:\: and \:\:} }%
\newcommand{\Then}{ \Keyword{then\: } }%
\newcommand{\Holds}{ \Keyword{holds\:\:} }%
\newcommand{cat}[1]{ \mathcal{#1} }%
%
\When A:Type \And a: A \vdash F(a):Type \\
\Then \\
\Holds \prod_{a:A}F(a) : Type
`$

[補足]
数式のレンダリングに使っているMathJaxの\ruleコマンド、または「はてなブログ」システムがバグっているらしく、横棒をうまく引けないんです。\ruleの出現位置、ブラウザ種別、ディスプレイかプリントアウトかによって表示が変わってしまうという制御不可能な挙動を示すので、\ruleの使用は諦めました。

上の横棒の図は、XyJax（「はてなブログでもXyJaxが使える、のか？」参照）で描いています。横棒はXyJaxのグラフィックスです。なんとか描けますが、XyJaxのコードを書くのは面倒なんで、ちょっとやってられない。で、代替記法にします。
[/補足]

上の推論規則を圏論の言葉に翻訳しましょう。Type = |C| だったので、A:Type とは A∈|C| のことです。a:A |- F(a):Type は、a∈A に対して F(a)∈|C| だと言っているので、結局、Fはファミリー〈関手〉だと主張しています。よって、圏論の言葉／書き方なら以下のようになります。

$`
\When A\in |\cat{C}| \And F: J(A) \to \cat{C} \mbox{ in }{\bf CAT} \\
\Then \\
\Holds Lim_A(F) \in |\cat{C}|
`$

要するに、任意の対象Aと関手 F:J(A) → C に対して極限が存在するよ、ってことなので、Cの自己完備性を要請していることになります。

次に、「底面Fの錐があると、パイ型 ΠA(F) への射が構成できる」という事実ですが、これは圏論の言葉から依存型理論の言葉へと翻訳してみます。

先に描いた可換図式を眺めると（念の為、すぐ下に再掲）次のことが言えます。

$`
\When A \in |\cat{C}|
\And a\in A
\And \psi_a : X \to F(a) \mbox{ in }\cat{C}\\
\Then \\
\Holds f:X \to Lim_A(F) \mbox{ in }\cat{C}
`$

可換図式：

$`
\forall a\in A.\\
\begin{CD}
X @>{f}>> \Pi_A(F) \\
@V{\psi_a}VV @VV{\pi(F)_a}V \\
F(a) @= F(a)
\end{CD}\\
\mbox{commutes in }{\mathcal{C}}
`$

この書き方は、論理的に正確とはいい難いですが、前提である錐 ψ に対して、射 f が一意に決まることを表現しています。

Cはデカルト閉圏だと仮定していたので、射をカリー化することにより終対象1からの射〈データ | ポイント〉に置き換えることができます。カリー化のオペレータを右肩にキャップ（'∩'）で示すとして、次のように書けます。

$`
\When A \in |\cat{C}|
\And a\in A
\And (\psi_a)^\cap :{\bf 1} \to [X, F(a)] \mbox{ in }\cat{C}\\
\Then \\
\Holds f^\cap:{\bf 1} \to [X, Lim_A(F)] \mbox{ in }\cat{C}
`$

ここだけの一時的な記法ですが、g:1 → A in C を g:∈ A in C と書くことにします。また、指数対象〈関数対象〉[A, B] を A $`\multimap`$ B とも書くことにします。そうすると：

$`
\When A \in |\cat{C}|
\And a\in A
\And (\psi_a)^\cap :\in X \multimap F(a) \mbox{ in }\cat{C}\\
\Then \\
\Holds f^\cap :\in X \multimap Lim_A(F) \mbox{ in }\cat{C}
`$

型理論では、射とそのカリー化データが同一視され、'∈' も ':∈' もコロンで書かれます。そして、指数型〈関数型〉を矢印記号「→」で書きます。それで次のようになります。

$`
\When A : Type
\And a : A
\And \psi_a : X \to F(a) \\
\Then \\
\Holds f : X \to \Pi_A(F)
`$

X = 1 のときは次のように簡略化されます。

$`
\When A : Type
\And a : A
\And \psi_a : F(a) \\
\Then \\
\Holds f : \Pi_A(F)
`$

こうして翻訳してみると、圏論と型理論を隔てているのは主に記法の習慣だと分かります。記法の見た目は多少似てますが*4、同じ記号が意図するところがズレています。僕はそろそろ翻訳がめんどくさくなりましたが、「依存型理論 → 圏論」方向の翻訳を丁寧に記述すれば、依存型理論の圏論的意味論〈セマンティクス | モデル〉が出来上がります。

依存型と総称型

依存型は今述べたようなものだとして、「多相型」とか「総称型」とかいう言葉もありますが、これらは何でしょうか？ -- なんだかよく分かりません。定義が合意されてませんからね。「多相」は矢鱈に広い意味で使われ、もはやワイルドカード／マジックワードになっている気がします、今日は議論しません。「総称」は（僕の印象だと）「型パラメータを持つ」くらいかな、と。もしそうなら、総称型は型パラメータを持つ型です。

ここではとりあえず、型パラメータを持つ型が総称型だとして、Cのカインド〈部分圏〉DからCへの関手 T:D → C in CAT を総称型〈generic type | generics〉と呼びましょう*5。

C自身はCのカインド〈部分圏〉なので、T:C → C という自己関手も総称型です。C = Set のときのリスト関手 List:Set → Set はそのような総称型の例です。一方で、対象 A∈|C| は“型”ですが、Aをポイントする関手 {1} → C を考えると、通常の型も特殊な総称型となります。{1} は、単元集合と恒等射だけからなる自明部分圏です。

定義の上からは、総称型と依存型は全然違うものです。総称型 T:D → C の極限／余極限の存在は保証されないので、パイ型／シグマ型の構成は自由にできません。もし、総称型に対するパイ型／シグマ型類似物が欲しいなら、Cの対象としてではなくて、Cの外部にある存在物として構成することになります。それは（ある程度は）できますが、先に述べた依存型理論とは違うものになります。

しかし、総称型が依存型を使って表現可能な場合もあります。カインド〈部分圏〉がレイファイ可能なときです。D ⊆ C をC-カインドだとして、次の条件を満たすとき、Dはレイファイ可能〈reifiable〉だといいます。

  • 対象 A∈|C| が存在して、J(A) と D が圏同値。

これは、カインドDが型Aで置き換え可能だということです。型＝対象であるAは単なる集合なので、レイファイ可能なカインドDはかなり特殊なもので、“本質的に小さい亜群”と呼ばれる圏です。カインドDが型Aにレイファイ可能なら、総称型 T:D → C はファミリー F:J(A) → C で置き換え可能です。このファミリーに対してはパイ型／シグマ型が作れます。

レイファイ可能性の条件がきつすぎて、ほとんど利用できない感じがしますが、工夫すれば意外に使えるかも？ と思ってますが、確信がないのでこの話はここでやめます。

おおざっぱな総括としては； パイ型／シグマ型が自由に作れる状況設定で行うのが依存型理論、より一般的な総称型は、この状況設定に収まるわけではない、ということです。

*1:もとの記事の冒頭に断り書きとこの記事へのリンクを入れますが、本文は修正しません。そういう落とし穴があるよ、という教訓です（ほんとはめんどくさい）。

*2:矢印記号のオーバーロードによる混乱はかなり深刻な問題で、「矢印の苦悩」とでも呼びたくなります。

*3:集合の要素と、その要素をポイントする射を同一視しています。データは、要素またはポイントする射の意味です。

*4:多少似ているところがタチが悪いのです。a∈A と a:A は似てますが、完全に同じわけではありません。矢印記号もほぼ同じに見えて、実は違う意味です。

*5:複数の型パラメータを持つ型なら、T:D1×...×Dn → C in CAT となります。ここでは単一の型パラメータだけ考えることにします。