[解決済み] 依存型タイピングとは？

質問

依存型付けについて教えてください。 Haskell, Cayenne, Epigramなどの関数型言語の経験がほとんどないので、簡単な言葉であればあるほどありがたいです!

どのように解決するのですか？

考えてみてください。まともなプログラミング言語であれば、関数を書くことができ、例えば

def f(arg) = result

ここで f は値をとります。 arg を受け取り、値を計算する。 result . これは値から値への関数である。

さて、言語によってはポリモーフィック（別名ジェネリック）な値を定義することができます。

def empty<T> = new List<T>()

ここで empty は型を取ります。 T を受け取り、値を計算する。これは型から値への関数である。

通常、汎用的な型定義も可能です。

type Matrix<T> = List<List<T>>

この定義は型を受け取り、型を返します。これは、型から型への関数と見なすことができます。

普通の言語が提供するものはここまでです。4番目の可能性、すなわち値から型への関数を定義することもできる言語を依存型言語と呼ぶ。言い換えれば、値に対する型定義のパラメータ化です。

type BoundedInt(n) = {i:Int | i<=n}

いくつかの主流の言語では、混同しないように、このような偽の形式をとっています。例えば、C++では、テンプレートはパラメータとして値を取ることができますが、適用されるときにはコンパイル時の定数でなければなりません。真に依存型言語ではそうではない。例えば、上の型をこんな風に使うことができる。

def min(i : Int, j : Int) : BoundedInt(j) =
  if i < j then i else j

ここでは、関数の結果型 が依存します。 は実際の引数値 j に依存するため、このような用語が使われています。