７．７ 型定理(Type Theory)
型定理という言葉に戸惑う人も多いことと思う。日本語版のウィキペディアで型理論を検索するとあまりにも短い記述にがっかりするだろう。得られる情報も余りない。しかし、さすがに英語版の方には詳しく書いてある。その記述の中に、圏論との関係についての記述がある。その中で、ジョン・ベル(John Lane Bell)が「圏は、ある種の型定理と見なすことができる」と書いていると紹介されている。その紹介に続いて、対象を型に変更すれば、圏は型定理になるとも書かれている。
対象を型に変えるという表現はどこかで見たような気がしないだろうか。そう、圏論をHaskellに変えるときに使っていた表現だ。なんてことはない。圏論の定理を型定理で解釈したほうが分かりやすい場合があることも経験的にわかっている。そこで、今回は、指数対象で成り立っている定理のいくつかについて、型定理での解釈を試みよう。
例を説明する前にこれまでの復習をしておこう。
\(A \Rightarrow B\)は、ドメイン\(A\)からコドメイン\(B\)への余すところのない、また、重複することのない射の集まり(集合)であった。そして、射の集まりは圏論では対象と見なすことができるので、これに特別な名前を与えて、写像対象と呼んだ。
\(A\)が\(m\)個の要素、\(B\)が\(n\)個の要素から成り立っているとき、射の総数は\(n^m\)である。
射の総数の表し方に似せて、写像対象\(A \Rightarrow B\)を\(B^A\)と書くことにする。\(B^A\)は指数対象と呼ばれる。指数対象が射の集まりであることに注意すると、二つの指数対象\(B^A\)と\(D^C\)が与えられた時、それぞれを構成している射の総数が同じである時、二つの指数対象には1対1の関係が成り立つ。この時、二つの指数対象は同型写像(Isomorphism)が成り立つという意味において同値であるといい、\(B^A = D^C\)と記述することとする。
また、Haskellでは対象は型(タイプ)として表される。指数対象\(B^A\)は型となるが、\(A\)も\(B\)も共に型である。Haskellでは型は小文字で記述されるので、\(a\),\(b\)と記述される。これは型変数とも呼ばれる。指数対象は射の集まりなので、Haskellでは型シグネチャで記述され、\(B^A\)は\(a \rightarrow b\)となる。
二つの指数対象\(B^A\)と\(D^C\)が同値の時、それぞれの型シグネチャは1対1に対応するので、
\begin{eqnarray}
a \rightarrow b \sim c \rightarrow d
\end{eqnarray}
と記述することにする。
それでは例を示すことにしよう。
1) \(A^{B+C}=A^B \times A^C\)
圏論では\(A^{B+C}=A^B \times A^C\)が成り立つ。これを、型定理、即ち、Haskellで解釈してみよう。
\(B+C\)は型定理では\(Either \ b \ c\)である。左辺\(A^{B+C}\)は\(B+C\)を入力とし\(A\)を出力とする射の集まりなので、型定理では\(Either \ b \ c \rightarrow a\)となる。
\(A\)と\(B\)のデカルト積、即ち、\(A \times B\)は型定理では\((a,b)\)である。右辺\(A^B \times A^C\)は二つの射の集まり\(A^B\)と\(A^C\)のデカルト積なので、型定理では\((b \rightarrow a, c \rightarrow a)\)となる。
従って、\(A^{B+C}=(A^B \times A^C)\)は型定理では
\begin{eqnarray}
Either \ b \ c \rightarrow a \sim (b \rightarrow a, c \rightarrow a)
\end{eqnarray}
といっている。
2) \(A^{B^C}=A^{B \times C}\)
左辺\(A^{B^C}\)は、\(C\)という入力から、(\(B\)を入力とし\(A\)を出力とする)射を出力とするような射の集まりなので、型定理では\(c \rightarrow (b \rightarrow a)\)となる。
右辺\(A^{B \times C}\)は、\(B \times C\)という入力から、\(A\)を出力とする射の集まりなので、型定理では\((b,c) \rightarrow a\)となる。
従って、\(A^{B^C}=A^{B \times C}\)は型定理では
\begin{eqnarray}
c \rightarrow (b \rightarrow a) \sim (b,c) \rightarrow a
\end{eqnarray}
となる。これは変数を増やすアンカリー化と変数を減らすカリー化である。
3) \((A \times B)^C=A^C \times B^C\)
左辺\((A \times B)^C\)は、\(C\)という入力から、デカルト積\(A \times B\)を出力とする射の集まりなので、型定理では\(c \rightarrow (a,b)\)となる。
右辺\(A^C \times B^C\)は、\(C\)という入力から\(A\)を出力とする射と\(C\)という入力から\(B\)を出力とする射の集まりのデカルト積なので、型定理では\((c \rightarrow a, c \rightarrow b)\)となる。
従って、\((A \times B)^C=A^C \times B^C\)は型定理では
\begin{eqnarray}
c \rightarrow (a,b) \sim (c \rightarrow a, c \rightarrow b)
\end{eqnarray}
となる。
前回説明したものについても、もう一度、挙げておこう。
4) \(A^0=1\)
左辺\(A^0\)は、\(0\)という入力から\(1\)を出力とする射の集まりである。型定理では、\(0\)は\(Void\)なので、左辺は\(Void \rightarrow a\)となる。
右辺は\(1\)である。型定理では、\(1\)はユニット\(()\)なので、右辺は\(()\)となる。
従って、\(A^0=1\)は型定理では
\begin{eqnarray}
Void \rightarrow a \sim ()
\end{eqnarray}
となる。これは、それぞれの集まりが1であることから、この関係が成り立つことが分かる。
5) \(A^1=A\)
左辺\(A^1\)は、\(1\)という入力から積\(A\)を出力とする射の集まりなので、型定理では\(() \rightarrow a\)となる。
右辺は\(A\)である。型定理では\(a\)となる。
従って、\(A^1=A\)は型定理では
\begin{eqnarray}
() \rightarrow a \sim a
\end{eqnarray}
となる。これは、それぞれの集まりが\(A\)の要素数であることから、この関係が成り立つことが分かる。
6) \(1^A=1\)
左辺\(1^A\)は、\(A\)という入力から積\(1\)を出力とする射の集まりなので、型定理では\(a \rightarrow ()\)となる。これは、終対象への写像であり、写像の総数は1である。
右辺は\(1\)である。型定理では\(()\)となる。
従って、\(1^A=1\)は型定理では
\begin{eqnarray}
a \rightarrow () \sim ()
\end{eqnarray}
となる。これは、それぞれの集まりが\(1\)であることから、この関係が成り立つことが分かる。
最後に型定理とプログラミングの関係を説明した本を紹介しておこう。Benjamin C. PierceのTypes and Programming Languagesがよいと思う(日本語訳も出ているようだ)。彼は、コンピュータ科学の人たちに向けて圏論の本も書いている。
また、最近のホットな話題はホモトピータイプ定理(Hotomopy Type Theory)である。型の概念をさらに抽象化した数学の一分野で、いずれは、コンピュータ科学に大きな影響を及ぼすだろうと期待している。
