有人可以解释依赖打字给我吗？我在Haskell，Cayenne，Epigram或其他功能语言中没有什么经验，所以更简单的术语你可以使用，更多我会欣赏它！
考虑这一点：在所有可行的编程语言中，您可以编写函数，例如。
原文链接：https://www.f2er.com/javaschema/282582.htmldef 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，因此是术语。
