有人可以解释依赖打字给我吗?我在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,因此是术语。