依存型入力とは何ですか？

Question

誰かが私に従属しているタイピングを説明できますか？私はHaskell、Cayenne、Epigram、またはその他の関数型言語での経験はほとんどないので、使用できる用語が簡単であればあるほど、私はそれを高く評価します！

Answer 1

これを考慮してください：すべてのまともなプログラミング言語では、関数を書くことができます。ここ

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、これの用語にを依存しています。

Answer 2

ブックタイプを引用し、プログラミング言語（30.5）：この本の

多くは抽象化にさまざまな種類の メカニズムを正式に関係してきました。単純に型付けされたラムダ計算では、 は、用語を取り、 サブタイトルを抽象化して、後で によって異なる用語にそれを適用することができる関数を生成する演算を形式化しました。システムFでは、 という用語を使用して型を抽象化し、さまざまな型に適用することによってインスタンス化できる用語 を生成すると考えました。 では、 レベルアップという単純な型指定のメカニズムを再現しました。型を取り、サブタイプを抽象化して 型演算子を取得しました。これは後で 異なる型に適用することでインスタンス化できます。 抽象化のこれらのすべての形式を考える便利な方法は、他の 式によって索引付けされた式のファミリの観点からです。通常のラムダ抽象化λx:T1.t2は、 という用語のファミリであり、用語の意味はsです。[x -> s]t1同様に、タイプ抽象度 λX::K1.t2は、タイプによって索引付けされる用語ファミリーであり、タイプ・オペレーター は、タイプ別に索引付けされるタイプのファミリーです。種類このリストを見てみると

によってインデックス付けタイプの種類

λX::K1.T2家族でインデックス化用語の観点

λX::K1.t2家族でインデックス化用語の

• λx:T1.t2家族、 1つの可能性があることは明らかです まだ考慮されていません。この 形式の抽象化も、依存型のルックアックの下で広範に研究されている。

Answer 3

あなたはC++、それが動機の例を提供するのは簡単です知ってしまった場合：あなたがかもしれない（我々は

typedef std::map<int,int> IIMap; 
IIMap foo; 
IIMap bar; 

その一部のコンテナ型と2つのインスタンスを持っていると言うと、このコードフラグメントを考えてみましょう

をfooが空ではないと仮定します）。

IIMap::iterator i = foo.begin(); 
bar.erase(i); 

これは明らかなガベージであり（おそらくデータ構造が壊れています"iterator into foo"と "iterator into bar"は意味的に完全に互換性がないにもかかわらず同じタイプのIIMap::iteratorであるため、型チェックが正しく行われます。

foo.iterator i = foo.begin(); 
bar.erase(i); // ERROR: bar.iterator argument expected 

：

問題がイテレータ型がコンテナにコンテナタイプではなく、実際には、単に依存してはならないオブジェクト、すなわち、それは「非静的メンバのタイプを」あるべきということです

このような特徴は、用語（foo）に依存する型（foo.iterator）を表現する能力は、厳密に型定義が意味するものです。

この機能がよく見えない理由は、ワームの大きな蓋を開くためです。突然、コンパイル時に2つのタイプが同じかどうかをチェックすると、 2つの式が同等であることを証明する（実行時に常に同じ値を返す）。その結果、ウィキペディアのlist of dependently typed languagesとそのlist of theorem proversを比較すると、疑わしい類似点に気付くことがあります。 ;-)

Answer 4

のより大きなセットは、コンパイル時間で削除することができます。これが機能fで次の仕様を考慮して説明するために：

機能fは、入力としてのみでも整数を取る必要があります。あなたはこのような何かかもしれない依存型なし

：ここ

def f(n: Integer) := { 
    if n mod 2 != 0 then 
    throw RuntimeException 
    else 
    // do something with n 
} 

コンパイラがnかどうかを検出することができない、つまり、次の式はokです、コンパイラの観点からも、確かにある：

f(1) // compiles OK despite being a logic error! 

このプログラムは実行時に実行時に例外をスローします。つまり、プログラムに論理エラーがあります。

さて、依存型がはるかに表現力もすることができますし、このような何かを書くことができますでしょう：

def f(n: {n: Integer | n mod 2 == 0}) := { 
    // do something with n 
} 

ここnは依存タイプ{n: Integer | n mod 2 == 0}です。

nは、各整数は、コンパイラがコンパイル時に検出します。この場合 2.

で割り切れるような整数の集合のメンバーであるように、それは大声で、これを読み出すために役立つかもしれません奇数をfに渡したロジックエラーで、最初にプログラムが実行されないようにします。

f(1) // compiler error