ジェネリックは、依存型と同じ値でパラメータ化されていますか？

Question

私は依存型について読んできました。何かを誤解していないことを確認するための質問が1つあります。これでWikipedia page on dependent types開始：コンピュータ科学とロジックで

、依存の型は、その定義値に依存タイプです。 「整数の対」はタイプです。 「第2の値が第1より大きい整数の対」は、値に依存するため依存型です。

---

私は範囲の数を表すことができる言語があるとします。例えば

struct Int<Min, Max> 

を、タイプInt<0, 10>は0包括と10との間の排他的整数を表します。ボーナスとして

、私は一般的な分散を導入するとします。たとえば

struct Int<in Min, out Max> 

を、そのようInt<3, 10>やInt<0, 8>ようなタイプのインスタンスは、タイプInt<0, 10>の変数に割り当てることができます。だから

Int<Min1 + Min2, Max1 + Max2> operator+(Int<Min1, Max1> op1, Int<Min2, Max2> op2); 

Int<0, 10>とを追加するタイプInt<3, 14>の結果を生成します：

今、このタイプの加算演算は次のようにシグネチャを持つことができます。そのようなタイプのシステムでは

、我々はまた、のようなペア、注文している可能性：ように

struct OrderedPair<Min, Mid, Max> 
{ 
    Int<Min, Mid> SmallerNumber; 
    Int<Mid, Max> LargerNumber; 
} 

をと。

---

これは従属型とは異なりますか？もしそうなら、どうですか？

Answer 1

これは、タイプが値に依存することができる限定されたタイプの依存型ですが、これらの値はコンパイル時に使用可能でなければなりません。

Idrisのような完全に依存する型付き言語では、型はランタイム値にも依存する可能性があります。そのような値を構成するには、その値に型が入る範囲がproofである必要があります。証拠を得るための一つの方法は、簡単なテスト（擬似コード）である：

m = user_input(); 
n = user_input(); 

// Type error: n is not guaranteed to be in range. 
x = Int<0, m>(n); 

if (n >= 0 && n <= m) { 
    // Accepted: proofs of n >= 0 and n <= m in scope. 
    x = Int<0, m>(n); 
} 

ですから、C++（例えば）で、あなたの例を実装するが、Int<Min, Max>を構築すると、コンストラクタで動的なチェックを必要とすることができます。 C++に完全な依存型があった場合は、というコンストラクタを何らかの形式のチェック（静的または動的）なしで呼び出すことさえできませんでした。