什么是依赖型打字？

Question

有人可以解释依赖打字给我吗？我在Haskell，Cayenne，Epigram或其他函数式语言方面没有经验，所以您可以使用的术语越简单，我越会感激它！

Answer 1

想一想：在所有正常的编程语言中，您都可以编写函数，例如

def f(arg) = result 

这里，f取值arg并计算值result。它是从值到值的函数。

现在，一些语言允许你定义多态（又名通用）值：

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，这样的术语。

Answer 2

竞标书的类型和编程语言（30.5）：

本书很多一直关注正式抽象不同种类的 机制。在简单类型的lambda演算中，我们 将抽取一个术语和抽象出一个 子项的操作形式化，产生一个函数，稍后可以通过 将其应用于不同的术语。在系统F中，我们考虑了 采取一个术语并抽象出一种类型的操作，产生一个术语 ，可以通过将其应用于各种类型来实例化该术语。在λω中，我们 概括了简单类型的lambda演算“一级 级别”的机制，采用一种类型并抽象出一个子表达式，以获得一个类型运算符，该运算符稍后可以通过将其应用于不同类型来实例化。所有这些抽象形式的简便思维方式都是根据表达式的家族来表达的，其他 表达式。普通拉姆达抽象λx:T1.t2是 术语[x -> s]t1的系列，其由术语s索引。类似地，类型抽象 λX::K1.t2是按类型索引的术语族，并且类型操作符 是按类型索引的类型族。

• λx:T1.t2家庭方面的通过方面

• λX::K1.t2家庭条件的按种类

• λX::K1.T2通过类型

看着这个列表索引类型的家庭收录索引，很显然，我们有一种可能性是 还没有考虑到：按条款索引的类型家族。这种抽象的形式也被广泛研究，依赖于依赖类型的 。

Answer 3

如果你碰巧知道C++可以很容易地提供一个激励例如：

比方说，我们有一些容器类型和两个实例及其

typedef std::map<int,int> IIMap; 
IIMap foo; 
IIMap bar; 

，并考虑下面的代码片段（您可能假设foo是非空的）：

IIMap::iterator i = foo.begin(); 
bar.erase(i); 

这是明显的垃圾（可能会破坏数据结构s），但它会进行类型检查，因为“iterator into foo”和“iterator into bar”是相同的类型，即使它们在语义上完全不兼容。

问题是一个迭代器类型不应该仅仅依赖于容器类型，但其实在容器上对象，也就是说，它应该是一个“非静态成员类型”：

foo.iterator i = foo.begin(); 
bar.erase(i); // ERROR: bar.iterator argument expected 

这样一个特性，即表达一个依赖于词（foo）的类型（foo.iterator）的能力，正是依赖类型意味着的。

你不经常看到这个功能的原因是因为它打开了一大堆蠕虫：你在编译时检查两种类型是否相同的情况下突然终止证明两个表达式是等价的（在运行时总会产生相同的值）。因此，如果您将维基百科的list of dependently typed languages与其list of theorem provers进行比较，您可能会注意到可疑的相似性。 ;-)

Answer 4

相关类型使logic errors的较大集合能够在编译时间被消除。为了说明这一点考虑功能f以下规范：

功能f必须采取只甚至整数作为输入。

没有相关的类型，你可以做这样的事情：

def f(n: Integer) := { 
    if n mod 2 != 0 then 
    throw RuntimeException 
    else 
    // do something with n 
} 

在这里，编译器不能如果n检测确实是偶数，也就是说，从编译器的角度来看，有以下公式确定：

f(1) // compiles OK despite being a logic error! 

该程序会运行，然后在运行时抛出异常，也就是说，您的程序有逻辑错误。

现在，依赖类型让你成为更富于表现力，并能使你写这样的事情：

def f(n: {n: Integer | n mod 2 == 0}) := { 
    // do something with n 
} 

这里n依赖型{n: Integer | n mod 2 == 0}的。它可以帮助阅读了这一点，大声

n是一个整数集的成员，使得每个整数整除 2.

在这种情况下，编译器会检测到在编译时一个逻辑错误，你已经通过一个奇数到f，并且会阻止程序首先被执行：

f(1) // compiler error