Являются ли дженерики параметризуемыми значениями такими же, как и зависимые типы?

Question

Я читал на зависимых типах, и у меня есть один вопрос, чтобы убедиться, что я не что-то недопонимаю. Wikipedia page on dependent types:

В информатике и логике зависимый тип - это тип, определение которого зависит от значения. «Пара целых чисел» - это тип. «Пара целых чисел, где вторая больше первой» является зависимым типом из-за зависимости от значения.

---

Предположим, что у меня есть язык, где я могу представлять собой число в диапазоне:

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++ имел полные зависимые типы, вы не могли бы даже вызвать конструктор без какой-либо проверки (статический или динамический).