依存するタイピングとは何ですか？

StackOverflow https://stackoverflow.com/questions/9338709

質問

誰かが私に依存的なタイピングを説明できますか？ 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, 、したがって、用語。

他のヒント

C ++を知っている場合は、やる気のある例を簡単に提供できます。

コンテナタイプとその2つのインスタンスがあるとしましょう

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

そして、このコードフラグメントを考慮してください（Fooが空でないと仮定することができます）：

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

これは明らかなゴミです（おそらくデータ構造を破損します）が、「foo」と「iterator into bar」が同じタイプであるため、タイプチェックされます。 IIMap::iterator, 、もしそれらが完全に互換性がないにもかかわらず。

問題は、iteratorタイプがコンテナだけに依存してはならないということです タイプ しかし、実際にはコンテナに 物体, 、つまり、それは「非静的なメンバータイプ」であるべきです：

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

このような機能、用語（foo）に依存するタイプ（foo.iterator）を表現する機能は、まさに依存するタイピングの意味です。

この機能をよく見ない理由は、ワームの大きな缶が開かれるためです。コンパイル時に2つのタイプが同じかどうかを確認するために、2つの式を証明する必要がある状況に突然なります。同等です（実行時に常に同じ値が生成されます）。その結果、Wikipediaのものを比較する場合 依存してタイプされた言語のリスト それで 定理プロバーのリスト 疑わしい類似点に気付くかもしれません。 ;-)

従属タイプは、より大きなセットを有効にします ロジックエラー で排除される 時間をまとめます. 。これを説明するには、関数に関する次の仕様を考慮してください f:

関数 f 取る必要があります 平 入力としての整数。

依存型がなければ、このようなことをするかもしれません：

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

ここでは、コンパイラがIFを検出できません n 確かに、つまり、コンパイラーの観点からは、次の式は問題ありません。

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

以下は、Scalaを使用した例です パス依存型 機能の実装を試みる方法の f そのような要件を満たす：

case class Integer(v: Int) {
  object IsEven { require(v % 2 == 0) }
  object IsOdd { require(v % 2 != 0) }
}

def f(n: Integer)(implicit proof: n.IsEven.type) =  { 
  // do something with n safe in the knowledge it is even
}

val `42` = Integer(42)
implicit val proof42IsEven = `42`.IsEven

val `1` = Integer(1)
implicit val proof1IsOdd = `1`.IsOdd

f(`42`) // OK
f(`1`)  // compile-time error

重要なのは、価値に気付くことです n 値のタイプで表示されます proof すなわち n.IsEven.type:

def f(n: Integer)(implicit proof: n.IsEven.type)
      ^                           ^
      |                           |
    value                       value

私達は言う タイプ n.IsEven.type に依存します 価値 n したがって、用語 依存型タイプ.

本の種類とプログラミング言語の引用（30.5）：

この本の多くは、さまざまな種類の抽象化メカニズムの形式化に関係しています。単にタイプされたLambda-Calculusでは、用語を取得してサブタームを抽象化するという操作を正式にし、それを異なる用語に適用することで後でインスタンス化できる関数を生成しました。システム内F, 、用語を取得してタイプを抽象化する操作を検討し、さまざまなタイプに適用することでインスタンス化できる用語を生成します。のλω, 、単にタイプされたラムダカルクルスの「1レベルアップ」のメカニズムを再現し、タイプを取り、サブエグエクスペレーションを抽象化して、異なるタイプに適用することで後でインスタンス化できるタイプ演算子を取得しました。これらすべての形式の抽象化を考えるのは、他の表現によって索引付けされた表現の家族の観点からです。通常のラムダ抽象化 λx:T1.t2 用語の家族です [x -> s]t1 用語でインデックス化されています s. 。同様に、タイプの抽象化 λX::K1.t2 タイプごとに索引付けされた用語ファミリーであり、タイプ演算子はタイプごとにインデックス化されたタイプのファミリーです。

  • λx:T1.t2 条件で索引付けされた用語の家族

  • λX::K1.t2 タイプごとに索引付けされた用語ファミリー

  • λX::K1.T2 タイプごとにインデックス付けされたタイプのファミリー

このリストを見ると、私たちがまだ考慮していない可能性が1つあることは明らかです。条件で索引付けされたタイプの家族です。この形式の抽象化は、従属タイプのルーブリックの下で広範囲に研究されています。

ライセンス： CC-BY-SA と 帰属
所属していません StackOverflow
scroll top