リスト、タプル、タグ付きデータ、関数、依存関数 - 檜山正幸のキマイラ飼育記 (はてなBlog)

$\newcommand{\Iff}{\Leftrightarrow } \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\id}{\mathrm{id} } \newcommand{\Id}{\mathrm{Id} } \require{color} \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\For}{\Keyword{For } }% \newcommand{\Where}{\Keyword{Where } }% \newcommand{\Let}{\Keyword{Let } }% \newcommand{\Then}{\Keyword{Then } }%$ 「依存型とΣ-Δ-Π随伴、そしてカン拡張」の冒頭にて：

「依存積型」と「依存和型」に関しては、もうサンザンだよー、あったく...[snip]...
ふんとに「依存ナントカ型」って紛らわしいよねぇ。それで、「依存ナントカ型」と言うのはやめます。...[snip]...
今後は見たままのパイ型／シグマ型を使おうと思います。

依存型の紛らわしさに、僕はもうほんとにウンザリなんだけど、今後はトラブルが起きないように整理しておきます。

内容：

はじめに
成分、インデックス
直積型、直和型、指数型＝関数型
直積型とタプル／リスト
直和型とタグ付きデータ
リスト型
型ファミリーとシグマ型
パイ型
まとめ

はじめに

依存型に関して、圏論的な解釈を試みた記事に次があります。

今回の記事は、内容的に過去記事と重複がありますが、過去記事を参照せずに読めると思います。また、あまり圏論は使わないようにしています。とはいえ、次の用語と記法は使っています。

「圏」「対象」「射」の定義くらいは知っていたほうがいいでしょう。
${\bf Set}$ は集合圏（集合と写像の圏）です。出てくる圏はこの圏だけです。
$|{\bf Set}|$ は集合圏の対象類で、すべての集合からなる類です。
${\bf Set}(A, B)$ は集合圏のホムセットですが、実体は関数〈写像〉の集合です。

今回強調したいことは、呼び名がインフレーション〈膨張・増大〉を起こしているだけで、依存型に関わる概念が少数であることです。次の4つを知っていれば十分です。

シグマ型
シグマ型のインスタンス＝タグ付きデータ
パイ型
パイ型のインスタンス＝タプル

成分、インデックス

ナニカを並べたり配置したりしたデータにおける“ナニカ”をなんと呼ぶか？

成分〈component〉
要素〈element〉
項目〈item〉
エントリー〈entry〉
フィールド値〈field value〉
属性値〈attribute value〉
カラム値〈column value〉
プロパティ値〈property value〉
スロット値〈slot value〉
もっとあるかも

ハァー、ここで既にウンザリ。これらに本質的な違いはなくて、要するに関数値のことです。「関数値」とは区別したいという感情や文脈を完全に無視するのもナンナンデ、「成分」だけは使うことにします。

複合データ（ナニカを並べたり配置したりしたデータ） $d$ の成分を取り出す構文（書き方）は：

$d_i$
$d^i$
$d.\!i$
$d[i]$
$d(i)$
$d\,i$
もっとあるかも

ここに出てくる $i$ の呼び名も色々ありますが、一律に「インデックス」で済ませます。インデックスは要するに関数に対する引数のことです。

複合データ＝関数
インデックス＝関数への引数
成分＝関数値

直積型、直和型、指数型＝関数型

型とは、集合または集合に構造が載ったもの（順序集合とかモノイドとか）のことです。より一般には、適当な圏 $\cat{C}$ の対象を「型」とも呼びます。つまり、型＝対象。ここでは、圏 $\cat{C}$ として集合圏 ${\bf Set}$ を取るので、型＝集合です。

「積型」、「和型」だと曖昧多義語でトラブルになるので、直積型〈direct product type〉、直和型〈direct sum type〉を使います。集合圏を背景にしているなら型＝集合なので、直積型＝直積集合、直和型＝直和集合。さすがにこれは誤解されないでしょう。

型（＝集合） $A, B$ に対して $B^A$ と書かれる型（＝集合）を指数型〈exponential type〉と呼ぶことにします。これも大丈夫だよな、と思ったら、Wikipediaの exponential type は複素解析の話だった。けど、function type へのリンクもありました。指数型〈exponential type〉＝ 関数型〈function type〉です。

次のような書き方もあります。（「関数」と「写像〈map〉」は同義語です。）

$\quad B^A = [A, B] = \mrm{Map}(A, B) = {\bf Set}(A, B)$

プログラミング言語だと、指数型（＝関数型）を $A \to B,\, A \Rightarrow B$ などと書きます。これは、射のプロファイル記述（域・余域の指定）と紛らわしいので僕は使いません。多くのプログラミング言語では、指数型（＝関数型）とプロファイルの記法を意図的に混同しています。そのへんのことは「Haskellの二重コロン「::」とバインド記号「>>=」の説明」参照。

一般的には型＝対象なので、指数型＝指数対象ということになります。 $\cat{C}$ がデカルト閉圏なら $\cat{C}$ 内の指数対象を考えることができます。nLab項目 exponential object 参照。

直積型とタプル／リスト

型（＝集合） $A, B$ に対してその直積型は $A\times B$ です。型（＝集合） $A, B, C$ に対してその直積型は $A\times B \times C$ です。が、次の2つの直積型は同じではありません。

$(A\times B) \times C$
$A\times (B \times C)$

同じではないけど同型なので、通常は同一視しています。同一視のための対応は：

$\quad ( (a, b), c ) \leftrightarrow (a, (b, c) )$

直積型のインスタンス〈要素〉をタプル〈tuple〉と呼びます。（ニュアンスは違うにしろ）タプルの同義語が山ほどあります。でも、「タプル」だけを使うことにします。

タプルの成分がすべて同じ型のときリストといいます。成分の型が $A$ で長さ（成分の個数）が $n$ であるリストの型は $A^n$ です。この記法は次のような意味です。

$\quad A^n = A\times A \times \cdots \times A$

しかし、 $A^n$ を指数型（＝関数型）と解釈することもできます（後述）。

タプルもリストも直積型〈直積集合〉のインスタンス〈要素〉ですが、リストはすべての成分が同一の型になっています。

直和型とタグ付きデータ

直積型に比べて、直和型は馴染みがない人が多いようです。型（＝集合） $A, B$ に対する直和型 $A + B$ は次のように定義します。

$\quad A + B := (\{1\}\times A ) \cup (\{2\} \times B)$

ここで注目すべきポイントは：

$\quad (\{1\}\times A ) \cap (\{2\} \times B)= \emptyset$

$A + B$ は、共通部分がない2つの部分から構成され、片一方は $A$ と同型で、もう一方は $B$ と同型です。もともと $A, B$ に共通部分があっても、別コピーを作って引き剥がされます。例えば：

$\quad A + A := (\{1\}\times A ) \cup (\{2\} \times A)\\ \Where\\ \quad (\{1\}\times A ) \cap (\{2\} \times A)= \emptyset$

直和型 $A + B$ のインスタンス〈要素〉は、 $(1, a)\:\text{where }a\in A$ または $(2, b)\:\text{where }b\in B$ の形です。第一成分をタグ〈tag〉と呼びます。 $(1, a),\, (2, b)$ はタプルですが、直和型のインスタンスであることを強調するときはタグ付きデータ〈tagged data〉といいます。

タグの集合として $\{1, 2\}$ を使いましたが、2元集合ならなんでもかまいません。例えば、

$\quad A + B := (\{\text{"foo"}\}\times A ) \cup (\{\text{"bar"}\} \times B)$

実用性はないけど自然なタグは集合それ自身です。

$\quad A + B := (\{A\}\times A ) \cup (\{B\} \times B)$

タグ付きデータを、見てすぐそれと分かるように書く記法は幾つかあります。僕は $a@1$ または $@1\; a$ のようなアットマークを使う記法を使っています。例えば、ユーザーIDとしてニックネーム〈ハンドル〉か通し番号のどちらでもいい場合、ユーザーIDのデータ型は次のようになるでしょう。

$\quad \mrm{UserID} := (\{\text{"name"}\} \times \mrm{String}) \cup (\{\text{"num"}\} \times {\bf N})$

ユーザーID型のインスタンスは $\text{"m-hiyama"}@\text{"name"}$ とか $1253@\text{"num"}$ とかになります。ストリングのダブルクォートを省略していいなら $\text{m-hiyama}@\text{name}$ または $1253@\text{num}$ です。

当然ながら、直和型、タグ、タグ付きデータに対する（ニュアンスは違うにしろ）同義語はありますが、同義語を列挙するのはやめます。ウンザリするだけのことなので。

リスト型

成分の型が $A$ であるリストの型は、リストの長さごとに $A^0, A^1, A^2, \cdots$ のように書けます。ここで、 $A^0$ は空リストだけからなる単元集合で、 $A^1 \cong A$ です（ $A^1 = A$ と思ってもかまいません）。

リストは実は関数です。そのことを説明するために、自然数 $n$ 対して、 $\bar{n} := \{1, 2, \cdots, n\}$ とします。特別な場合は：

$\bar{0} = \{\} = \emptyset$
$\bar{1} = \{ 1 \}$
$\bar{2} = \{ 1, 2 \}$

リスト $a$ があるときに、その第 $i$ 成分は $a_i$ と書きますが、 $a(i)$ と書いても同じことです。次は同値です。

$a$ は、成分の型が $A$ で、長さが $n$ のリストである。
$a$ は、余域が $A$ で、域が $\bar{n}$ の関数である。

型〈集合〉のあいだの同型として書けば：

$\quad A^n \cong A^{\bar{n}}$

上記の同型の右辺は指数型（＝関数型）です。

$\quad A^{\bar{n}} = \mrm{Map}(\bar{n}, A) = {\bf Set}(\bar{n}, A)$

成分の型が $A$ で、長さが $n$ のリストの型を $\mrm{List}_n(A)$ と書きます。つまり：

$\quad \mrm{List}_n(A) := A^{\bar{n}} = \mrm{Map}(\bar{n}, A)$

長さを固定したリストの型は実は指数型（＝関数型）だったのです。関数型の要素を“関数”と呼ぶ（当たり前！）ので、リストは関数です。

すべての長さのリストを寄せ集めると、長さを固定しないリストの型ができます。それを $\mrm{List}(A)$ と書きます。

$\quad \mrm{List}(A) \\ := \mrm{List}_0(A)\cup \mrm{List}_1(A)\cup \mrm{List}_2(A)\cup \cdots\\ = \bigcup_{n\in {\bf N}}\mrm{List}_n(A)\\ = \bigcup_{n\in {\bf N}}\mrm{Map}(\bar{n}, A)$

$n\ne m$ ならば $\mrm{List}_n(A) \cap \mrm{List}_m(A) = \emptyset$ なので、タグ付きデータにする必要はないのですが、リストの長さをタグにすると次のようになります。

$\quad \mrm{List}(A) \\ := (\{0\}\times \mrm{List}_0(A)) \cup (\{1\} \times \mrm{List}_1(A))\cup (\{2\} \times \mrm{List}_2(A)) \cup \cdots\\ = \bigcup_{n\in {\bf N}} (\{n\}\times \mrm{List}_n(A))\\ = \sum_{n\in {\bf N}} \mrm{List}( A)$

$\sum$ は無限直和の場合も使える記号です。もちろん、有限直和に使ってもかまいません。例えば：

$\quad \sum_{i\in \{1, 2, 3\}} X_i = X_1 + X_2 + X_3$

もともと共通部分がないときでもタグを付けるのはバカバカしいのはそのとおりです。そこで次の約束をしましょう。

もともと共通部分がない集合たちに対して、 $\sum$ は $\bigcup$ と同じ意味で使ってよい。
共通部分がある集合たちに対しては、適当にタグを付けた直和を $\sum$ で表す。

このようなご都合主義的約束をしても大丈夫なのは、結果として出来上がる型〈集合〉が同型になるからです。同型な型〈集合〉を神経質に区別する必要はありません。

[追記]リスト型の定義にまつわる問題が次の記事にあります。

集合論と圏論がズレるとき：空リスト問題

[/追記]

型ファミリーとシグマ型

集合 $X$ 上で定義されて値が集合である関数を、

$X$ でインデックス付けられた集合族〈X-indexed family of sets〉

と呼びます。長いので「集合族」と省略します。集合＝型だったので「型族」、ですがなんか語感が悪いので「型ファミリー〈type family〉」とします。型ファミリーも関数なので：

型ファミリーの成分＝集合値関数の関数値である集合（成分＝関数値）
型ファミリーのインデックス ＝集合値関数の引数（インデックス＝引数）
型ファミリーのインデックス集合 ＝集合値関数の域

型ファミリー〈集合値関数〉のインデックス集合〈関数の域〉は何でもいいので、特に $\bar{n}$ に取ると、型ファミリー $F:\bar{n} \to |{\bf Set}|$ ができます。ところで、域（インデックス集合）が $\bar{n}$ である関数をリストと呼んでいたので、これは型〈集合〉のリストです。つまり、型のリストは型ファミリーの特別なものです。

例えば、型ファミリー $F:\{1, 2, 3\} \to |{\bf Set}|$ は、長さ3の型のリストです。

$\For F:\{1, 2, 3\} \to |{\bf Set}|\\ \Let A := F(1)\\ \Let B := F(2)\\ \Let C := F(3)\\ \Then F = (A, B, C)$

番号の集合 $\bar{n}$ とは限らない任意の集合 $X$ でインデックス付けられた型ファミリー $F:X \to |{\bf Set}|$ に対して（無限かも知れない）直和型を定義できます。インデックス集合（関数の域） $X$ をタグの集合に使います。

$\quad \sum_{x\in X} F(x) := \bigcup_{x\in X} (\{x\}\times F(x))$

次のように定義することもできます。

$\quad \sum_{x\in X} F(x) := \{ (t, v) \in X \times \bigcup_{x\in X}F(x) \mid v \in F(t) \}$

この定義に従うと：

$\quad (t, v)\in \sum_{x\in X} F(x) \Iff t\in X \land v\in F(t)$

（無限かも知れない）直和型のインスタンス〈要素〉は、タグ $t$ と値 $v$ のペアで、値 $v$ が型ファミリーの成分 $F(t)$ に所属するものです。

（無限かも知れない）直和型の別名がシグマ型〈sigma type〉です。ここで、「依存ナントカ」という用語を使うとまたトラブルになるので、使う言葉は次のものに限定します。

型ファミリー
直和型（ただし、インデックス集合が無限も許す）
シグマ型＝直和型（ただし、インデックス集合が無限も許す）
タグ付きデータ＝シグマ型のインスタンス

パイ型

$F:X \to |{\bf Set}|$ が型ファミリーのとき、成分達 $F(x)$ をすべて足し合わせた型〈集合〉が（型ファミリーの）シグマ型でした。成分達 $F(x)$ をすべて掛け合わせた型〈集合〉が（型ファミリーの）パイ型〈pi type〉です。

簡単な例 $F:\{1, 2, 3\} \to |{\bf Set}|$ で説明します。先に説明した $F = (A, B, C)$ という書き方を使います。ファミリーは関数であり、番号集合からの関数はリストです。だから、番号集合を域〈インデックス集合〉とする型ファミリーは型のリストです。

成分が有限個である型ファミリーの場合は、そのパイ型は次のように定義してかまいません。

$\quad \prod_{i\in \{1, 2, 3\} } F(i) \\ = \prod_{i\in \{1, 2, 3\} } (F(1), F(2), F(3)) \\ = \prod_{i\in \{1, 2, 3\} } (A, B, C) \\ := A \times B \times C$

インデックス集合が無限になっても通用するように少し形を変えます。

$\quad \prod_{i\in \{1, 2, 3\} } F(i)\\ = \prod_{i\in \{1, 2, 3\} } (F(1), F(2), F(3))\\ = \prod_{i\in \{1, 2, 3\} } (A, B, C)\\ := \{ f\in \mrm{Map}(\{1, 2, 3\}, A\cup B\cup C) \mid f(1)\in A \land f(2)\in B \land f(3) \in C \}$

パイ型の要素は関数 $f:\{1, 2, 3\} \to A\cup B\cup C$ です。しかし、任意の関数を許すわけではなくて、条件を満たすものに絞ります。この条件を満たす関数 $f = (f(1), f(2), f(3))$ は $A\times B \times C$ の要素、つまりタプルと同一視できます。パイ型はタプルの型だと言えます。

$f$ に対する条件は次のようにも書けます。

$\quad \forall j\in \{1, 2, 3\}.\, f(j)\in F(j)$

これを使うと、型ファミリーのインデックス集合が無限の場合でもパイ型の定義が書けます。

$\quad \prod_{x\in X } F(x) := \{ f\in \mrm{Map}(X, \bigcup_{x\in X}F(x) ) \mid \forall t\in X.\, f(t)\in F(t) \}$

こうして定義されるパイ型のインスタンスはサイズが無限かも知れないタプルです。タプルがリストと違うのは、インデックス〈引数〉ごとに値を取る集合が異なるかも知れない点です。

「リスト＝関数」はいいとしても、「タプル＝関数」は言いすぎかも知れません。そこで、タプル＝ 依存関数〈dependent function〉とも呼びます。「依存」という言葉を含めると何かトラブルが起きそうで僕は懲りているから（「羹に懲りて膾を吹く」）、「依存」は使いたくないけど、用語「依存関数」は許すとしましょう。