什么是依赖打字？

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

如果您碰巧了解C++,那么很容易提供一个激励性的例子:

假设我们有一些容器类型和两个实例

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

并考虑这个代码片段(你可以假设foo是非空的):

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

这显然是垃圾(并且可能破坏数据结构),但是它会进行类型检查,因为"迭代器变成foo"和"迭代器变成条形"是相同的类型IIMap::iterator,即使它们在语义上完全不兼容.

问题是迭代器类型不应该只依赖于容器类型,而应该依赖于容器对象,即它应该是"非静态成员类型":

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

这样的特征,表达依赖于术语(foo)的类型(foo.iterator)的能力正是依赖类型的意思.

你不经常看到这个功能的原因是因为它打开了一大堆蠕虫:你突然遇到这样的情况:在编译时检查两种类型是否相同,你最终必须证明两个表达式是等价的(在运行时总是会产生相同的值).因此,如果您将维基百科的依赖类型语言列表与其定理证明列表进行比较,您可能会发现可疑的相似性.;-)

Answer 3

依赖类型允许在编译时消除更大的逻辑错误集.为了说明这一点,请考虑以下功能规范: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

Answer 4

引用书籍类型和编程语言(30.5):

本书的大部分内容都与形式化各种抽象机制有关.在简单类型化的lambda演算中,我们形式化了一个术语并抽象出一个子项的操作,产生了一个函数,以后可以通过将其应用于不同的术语来实例化.在System中F,我们考虑了使用术语和抽象出类型的操作,产生了一个可以通过将其应用于各种类型来实例化的术语.在中??,我们概括了简单类型lambda-calculus"一级向上"的机制,它采用一种类型并抽象出一个子表达式来获得一个类型操作符,以后可以通过将其应用于不同类型来实例化.考虑所有这些抽象形式的一种便捷方式是表达式系列,由其他表达式索引.普通的lambda抽象?x:T1.t2是一个由术语[x -> s]t1索引的术语族s.类似地,类型抽象 ?X::K1.t2是由类型索引的一族术语,类型操作符是由类型索引的类型族.

• ?x:T1.t2 按术语索引的术语系列

• ?X::K1.t2 按类型索引的术语系列

• ?X::K1.T2 按类型索引的类型族

看一下这个清单,很明显我们还没有考虑过一种可能性:按术语索引的类型系列.在依赖类型的标题下,这种抽象形式也得到了广泛的研究.