功能编程 – 什么是依赖打字？

有人可以解释依赖打字给我吗？我在Haskell，Cayenne，Epigram或其他功能语言中没有什么经验，所以更简单的术语你可以使用，更多我会欣赏它！

考虑这一点：在所有可行的编程语言中，您可以编写函数，例如。

def f(arg) = result

这里，f取值arg并计算值结果。它是一个从值到值的函数。

现在，一些语言允许您定义多态(也称为通用)值：

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

这里，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

编辑：这里，函数的结果类型取决于实际的参数值j，因此是术语。