什么是依赖类型？

有人可以向我解释依赖类型吗？我对 Haskell、Cayenne、Epigram 或其他函数式语言缺乏经验，因此您可以使用的术语越简单，我就越感激！

考虑一下：在所有像样的编程语言中，您都可以编写函数，例如

def f(arg) = result

Here, f取一个值arg并计算一个值result。它是一个从值到值的函数。

现在，某些语言允许您定义多态（也称为通用）值：

def empty<T> = new List<T>()

Here, empty需要一个类型T并计算一个值。它是一个从类型到值的函数。

通常，您还可以有泛型类型定义：

type Matrix<T> = List<List<T>>

该定义接受一个类型并返回一个类型。它可以被视为从类型到类型的函数。

普通语言提供的功能就这么多。如果一种语言还提供第四种可能性，即定义从值到类型的函数，则该语言被称为依赖类型。或者换句话说，通过值参数化类型定义：

type BoundedInt(n) = {i:Int | i<=n}

一些主流语言有一些虚假的形式，不要混淆。例如。在 C++ 中，模板可以将值作为参数，但应用时它们必须是编译时常量。在真正依赖类型的语言中并非如此。例如，我可以像这样使用上面的类型：

def min(i : Int, j : Int) : BoundedInt(j) =
  if i < j then i else j

这里，函数的结果类型depends关于实际参数值j，因此有了术语。