什么是依赖打字？
有人可以解释依赖打字给我吗？ 我在Haskell，Cayenne，Epigram或其他函数式语言方面经验不多，所以您可以使用的术语越简单，我越会感激！
考虑到这一点：在所有体面的编程语言，你可以编写函数，例如
def f(arg) = result 这里， f取值为arg并计算值result 。 这是一个从价值到价值的function。
现在，一些语言允许你定义多态（又名通用）值：
def empty<T> = new List<T>()
这里， empty取一个typesT并计算一个值。 这是一个从types到值的函数。
通常，你也可以有通用的types定义：
type Matrix<T> = List<List<T>>
这个定义需要一个types，并返回一个types。 它可以被看作是从types到types的函数。
对于普通语言提供的东西太多了。 如果一种语言也提供了第四种可能性，那么称它为依赖types，即定义从值到types的函数。 换句话说，通过一个值参数化一个types定义：
type BoundedInt(n) = {i:Int | i<=n}
一些主stream的语言有一些这样的假的forms是不会混淆的。 例如，在C ++中，模板可以将值作为参数，但是在应用时它们必须是编译时常量。 不是一个真正的依赖型语言。 例如，我可以像这样使用上面的types：
def min(i : Int, j : Int) : BoundedInt(j) = if i < j then i else j
编辑：这里，函数的结果types取决于实际的参数值j ，因此是术语。
如果你碰巧知道C ++，很容易提供一个激励的例子：
假设我们有一些容器types和两个实例
typedef std::map<int,int> IIMap; IIMap foo; IIMap bar;
并考虑这个代码片段（你可以假设foo是非空的）：
IIMap::iterator i = foo.begin(); bar.erase(i);
这是显而易见的垃圾（可能会破坏数据结构），但它会types检查就好了，因为“迭代器到foo”和“迭代器到吧”是相同的types， IIMap::iterator ，即使它们完全不兼容语义。
问题是一个迭代器types不应该仅仅取决于容器types，而是实际上取决于容器对象 ，即它应该是一个“非静态成员types”：
foo.iterator i = foo.begin(); bar.erase(i); // ERROR: bar.iterator argument expected
这样一个特征，即expression一个依赖于一个词（foo）的types（foo.iterator）的能力正是依赖types意味着什么的。
你不经常看到这个特性的原因是因为它打开了一大堆蠕虫：你在编译时检查两种types是否相同的情况下，最终会出现两个expression式是等价的（在运行时总会产生相同的值）。 因此，如果您将维基百科的依赖types语言 列表与定理certificate列表进行比较，您可能会注意到可疑的相似性。 😉
引用“书本types和编程语言”（30.5）：
这本书的大部分内容都涉及forms化各种抽象机制。 在简单types的lambda演算中，我们将抽取一个术语和抽象出一个子项的操作forms化，产生一个函数，稍后可以通过将其应用于不同的术语来实例化该函数。 在系统
F，我们考虑了抽取一个types的术语和抽象types的操作，产生一个可以通过将其应用于各种types来实例化的术语。 在λω，我们概括了简单types的lambda演算“上一层”的机制，取一个types并抽象出一个子expression式，以获得一个types运算符，稍后可以通过将其应用于不同types来实例化。 所有这些抽象forms的一种便利的思维方式就是用其他expression方式进行索引的expression系列。 一个普通的lambda抽象λx:T1.t2是由项s指数化的一个项[x -> s]t1。 类似地，types抽象λX::K1.t2是由types索引的一系列术语，并且types操作符是按types索引的types族。
λx:T1.t2系列术语索引
λX::K1.t2系列由types索引的术语
λX::K1.T2types索引的types看这个清单，显然有一种可能性，我们还没有考虑到：按条款索引的types的家庭。 这种抽象forms也在依赖types的标题下被广泛研究。
相关types使编译时可以消除更多的逻辑错误 。 为了说明这一点，请考虑函数f的以下规范：
函数
f只能用偶数作为input。
没有依赖types，你可能会这样做：
def f(n: Integer) := { if n mod 2 != 0 then throw RuntimeException else // do something with n }
这里编译器无法检测到n是否确实是偶数，也就是说，从编译器的angular度来看下面的expression式是可以的：
f(1) // compiles OK despite being a logic error!
这个程序会运行，然后在运行时抛出exception，也就是说，你的程序有一个逻辑错误。
现在，依赖types使您能够更加富有performance力，并使您能够编写如下所示的内容：
def f(n: {n: Integer | n mod 2 == 0}) := { // do something with n }
这里n是依赖types{n: Integer | n mod 2 == 0} {n: Integer | n mod 2 == 0} 。 这可能有助于大声读出这个
n是一组整数的成员，每个整数可以被2整除。
在这种情况下，编译器会在编译时检测到一个逻辑错误，在那里你传递了一个奇数给f并且会阻止程序首先被执行：
f(1) // compiler error
