依存型

依存型  とは、計算機科学と論理学において、値に依存する型のことである。数学の型理論の表現形式と計算機科学における型システムの特徴を併せ持つ。直観主義型理論においては、全称量化子や存在量化子のような論理学における量化子をエンコードするために依存型が用いられている。ATS 、Agda、Idris、Epigramなどのいくつかの関数型プログラミング言語では、依存型を使った非常に表現力の強い型によって、バグを防止している。

依存型の中でも、依存関数と依存ペアは特によく使われている。依存関数の戻り値の型は、引数の型だけではなく引数の//値//に応じて変化する。例えば、整数"n"を引数に取る依存関数は長さ"n"の配列を返すことができる。  依存ペアでは、2番目の型が1番目の値に応じて変化する。依存ペアを使うと、2番目の値が1番目の値よりも大きいような整数の対をエンコードすることができる。

依存型を入れた型システムは、より複雑になる。プログラム中に出現する2つの依存型が等しいかどうかを判定するとき、プログラムの一部を実行する必要があるかもしれない。特に、依存型に任意の式を含めることが許される場合、型の同値性判定は任意に与えられた2個のプログラムが同じ結果をもたらすかどうかを判定する問題を含んでしまう。したがって、この場合は型検査は決定不能となってしまう。

1. 歴史
-----

依存型は、プログラミングと論理学のつながりを深めるために作られた。

1934年にハスケル・カリーは、当時考えられていた数学的なプログラミング言語で使われていた型が、命題論理の公理系と同じパターンに従っていることを発見した。さらに、命題論理の証明それぞれに対して、プログラミング言語における関数が対応していることもわかった。カリーの挙げた例の一つは、単純型付きラムダ計算と直観主義論理の対応である。

述語論理は命題論理に量化子を加えたものである。ハワードとド・ブラウンは型付きラムダ計算に依存関数のための型と依存ペアのための型を加えることで、述語論理に対応するプログラミング言語を作り出した。



2. 形式的な定義
---------

非常に大雑把に説明すると、依存型は添字づけられた集合の族によって与えられると考えることができる。より形式的には、をに属する型としたときに、型のなす族を考えることができる。すなわち、に属する値それぞれについて、型が割り当てられているのである。終域が引数に応じて変化する関数は依存関数と呼ばれ、このような関数のための型は依存型、依存積型、あるいはΠ型と呼ばれる。この例では、依存積型は

あるいは

と表記される。

もし//B//が定数関数であるなら、依存積型は通常の関数型となる。つまり、は型判定において関数型と等しい。

Π型という名前は、依存積型が型の直積と見なせるという考え方に由来している。依存積型は全称量化のモデルとして理解することもできる。

例えば、実数の個の対をと表記するとき、は、自然数//n//を受け取り//n//個の実数の対を返す関数の型である。通常の関数空間は、依存積型で戻り値の型が実際には引数に依存しない特別な場合としてあらわれる。//例えば//、は自然数から実数への関数の型であり、単純型付きラムダ計算ではと表記される。

型多相な関数は依存関数の重要な例である。多相関数は、型を与えられると、その型を含む型を持つ値として振る舞う。例えば、恒等関数、すなわち任意の型//A//に対しを受け取り//a//をそのまま返す関数、の型は、

と書くことができる。

3. 依存ペア型
--------

依存積型の双対は、依存ペア型、依存和型、あるいはΣ型と呼ばれる型である。これは余積や直和、非交和などのアナロジーである。依存和型は存在量化のモデルとして理解することもできる。依存和型は

と表記される。

依存和型は、2番目の型が1番目の値に応じて変化するペアの型を表している。したがって、もし

ならば、であり、である。//B//が定数関数のときは、依存和型は直積型、すなわち通常の直積と一致する。

3.1. 存在量化としての例
--------------

を、型上で述語を量化した依存和型とする。このとき、が成立するが存在することと、が非空であることが同値である。例えば、//a//が//b//以下であることと、自然数//n//と//a//+//n//=//b//の証明の組が存在することが同値である。

4. ラムダ・キューブ
-----------

ヘンク・バレンドレクト  はいくつかの型システムを3つの軸にそって分類するラムダ・キューブを発明した。立方体の形をした図の8個の頂点それぞれが型システムに対応している。単純型付きラムダ計算が最も表現力が低い頂点に配置され、Calculus of constructions が最も表現力が高い頂点に配置されている。立方体の3個の軸はそれぞれ単純型付きラムダ計算に対する3種類の異なる拡張を意味している。それぞれ、依存型の追加、型多相性の追加、高階のカインド ) を持つ型コンストラクタ  の追加、である。ラムダ・キューブは純粋型システム によってさらに一般化される。

ラムダ・キューブにおける依存型と多相型は、どちらも依存積型の特別な場合と見なせるが、値に関する量化をする場合は依存型、型や型コンストラクタに関する量化をする場合は多相型と呼び、区別される。ラムダ・キューブにおけるカインドを, 超カインドをと表記する。このとき、依存型とは、およびを用いて構成される、という型のことである。一方、多相型は、およびを用いて構成される、という型のことである。例えば、であることを用いてと書いたものは、型に関する量化をしている多相型となる。

4.1. 一階の依存型理論
-------------

一階の依存型を持つ型システムは、単純型付きラムダ計算の関数型を依存積型に一般化することで得られる。これは論理学におけるLogical Framework LF に対応する。

4.2. 二階の依存型理論
-------------

二階の依存型を持つ型システムは、に型コンストラクタ上での量化を許容することで得られる。この型システムでは、依存積演算子は単純型付きラムダ計算の演算子とSystem Fの束縛子の両方の役割を果たす。

4.3. 高階の依存型付き多相ラムダ計算
--------------------

高階の型システムはを、ラムダ・キューブの4つ全てのラムダ抽象の形式に拡張することで得られる。すなわち、項から項への関数、型から項への関数、項から型への関数、そして型から型への関数である。この型システムはCalculus of constructionsに対応する。Calculus of constructionsをさらに拡張するとCalculus of inductive constructions  が得られる。これは、Coqが用いている型システムである。

5. プログラミング言語と論理学の両立
-------------------

カリー＝ハワード同型対応により、どんなに複雑な数学的な性質も型によって表現できる。もしユーザーが、型が//非空//である  ことの構成的な証明を与えることができれば、コンパイラは証明の正当性を検査し、証明の構成を追うことにより、実際にその値を計算できる実行可能なプログラムコードを出力することができる。このように証明を検査できるという性質により、依存型を持つプログラミング言語は定理証明支援系と近い関係にある。コードを生成できるという視点からは、機械的に検証された数学の証明からプログラムコードを直接導出することができるため、形式手法によるプログラム検証や証明つきコードへのアプローチが考えられる。

6. 脚注
-----

7. 関連項目
-------

型理論
直観主義型理論
型付きラムダ計算
型システム