泛型是否由与依赖类型相同的值参数化？

Question

我一直在阅读依赖类型，我有一个问题要确保我没有误解什么。 Wikipedia page on dependent types 以此开头：

In computer science and logic, a dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value.

假设我有一种语言可以表示一个范围内的数字：

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, 4> 将产生 Int<3, 14>.

类型的结果

在这样的类型系统中，我们也可以有有序的对，例如：

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

以此类推

这与依赖类型有什么不同吗？如果是，怎么做？

Answer 1

这是依赖类型的一种有限形式，其中类型可以依赖于值，但这些值必须在编译时可用。

在完全依赖类型的语言中，例如 Idris, types can also depend on runtime values—in order to construct such a value, you need a 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++ 有完全依赖的类型，你甚至不能 在没有某种形式的检查（静态或动态）的情况下调用 构造函数。

泛型是否由与依赖类型相同的值参数化？

Are generics parameterized by values the same as dependent types?

language-agnostic

generics

dependent-type