什么是依赖类型？答案

【问题标题】：What is dependent typing?什么是依赖类型？
【发布时间】：2012-03-09 11:17:04
【问题描述】：

有人可以向我解释依赖类型吗？我在 Haskell、Cayenne、Epigram 或其他函数式语言方面的经验很少，所以您使用的术语越简单，我就会越感激！

【问题讨论】：

嗯，文章开头是 lambda 立方体，对我来说听起来像是某种羊肉。然后继续讨论 λΠ2 系统，由于我不会说外星人，所以我跳过了那部分。然后我读到了关于归纳构造的微积分，顺便说一下，这似乎与微积分、热传递或构造无关。给个语言对照表后，文章就结束了，比到页面时更迷茫了。
@Nick 这是维基百科的普遍问题。几年前我看到了你的评论，从那以后我就记住了。我现在正在为它添加书签。

标签： functional-programming dependent-type

【解决方案1】：

考虑一下：在所有体面的编程语言中，您都可以编写函数，例如

def f(arg) = result

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

现在，一些语言允许您定义多态（又名泛型）值：

def empty<T> = new List<T>()

这里，empty 采用类型 T 并计算一个值。它是一个从类型到值的函数。

通常，您也可以有泛型类型定义：

type Matrix<T> = List<List<T>>

这个定义接受一个类型并返回一个类型。可以看成是一个从类型到类型的函数。

普通语言所能提供的就这么多。如果一种语言还提供第 4 种可能性，即定义从值到类型的函数，则该语言称为依赖类型。或者换句话说，通过值参数化类型定义：

type BoundedInt(n) = {i:Int | i<=n}

一些主流语言有一些虚假的形式，不要混淆。例如。在 C++ 中，模板可以将值作为参数，但在应用时它们必须是编译时常量。在真正依赖类型的语言中并非如此。例如，我可以像这样使用上面的类型：

def min(i : Int, j : Int) : BoundedInt(j) =
  if i < j then i else j

这里，函数的结果类型取决于实际参数值j，因此是术语。

【讨论】：

BoundedInt 示例实际上不是细化类型吗？这“非常接近”，但并不完全是那种“依赖类型”，例如 Idris 在关于 dep.typing 的教程中首先提到的那种。
@Noein，细化类型确实是依赖类型的一种简单形式。
我可以看到它是一种很好的方式，让程序员知道我必须小于 j。但是为什么它与仅仅检查“if i>j {throw error}”相比真的有那么大的不同呢？这种类型不能在编译时检查，所以它做同样的事情，我只是不确定有什么优势。
@mczarnek，这些类型在编译时被检查。否则它们就不是类型。

【解决方案2】：

依赖类型可以在编译时消除更多的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

这是一个使用 Scala path-dependent types 的说明性示例，说明我们如何尝试实现满足此类要求的函数 f：

case class Integer(v: Int) {
  object IsEven { require(v % 2 == 0) }
  object IsOdd { require(v % 2 != 0) }
}

def f(n: Integer)(implicit proof: n.IsEven.type) =  { 
  // do something with n safe in the knowledge it is even
}

val `42` = Integer(42)
implicit val proof42IsEven = `42`.IsEven

val `1` = Integer(1)
implicit val proof1IsOdd = `1`.IsOdd

f(`42`) // OK
f(`1`)  // compile-time error

关键是注意值n如何出现在值proof的类型中，即n.IsEven.type：

def f(n: Integer)(implicit proof: n.IsEven.type)
      ^                           ^
      |                           |
    value                       value

我们说 type n.IsEven.type 取决于 value n 因此术语 dependent-types。

作为另一个示例，让我们定义一个 dependently typed function，其中返回类型将取决于 value 参数。

使用 Scala 3 工具，请考虑以下 heterogeneous list，它维护其每个元素的精确类型（而不是推导出常见的最小上限）

val hlist: (Int, List[Int], String)  = 42 *: List(42) *: "foo" *: Tuple()

目标是索引不应该丢失任何编译时类型信息，例如，在索引第三个元素之后，编译器应该知道它正是String

val i: Int = index(hlist)(0)           // type Int depends on value 0
val l: List[Int] = index(hlist)(1)     // type List[Int] depends on value 1 
val s: String = index(hlist)(2)        // type String depends on value 2

这是依赖类型函数index的签名

type DTF = [L <: Tuple] => L => (idx: Int) => Elem[L, idx.type] 
                                  |                     |        
                                 value           return type depends on value

或者换句话说

对于L 类型的所有异构列表，以及所有（值）索引 idx 类型为Int，返回类型为Elem[L, idx.type]

我们再次注意到返回类型如何取决于值idx。

这里是完整的实现供参考，它利用了literal-based singleton types、Peano 在类型级别的整数实现、match types 和dependent functions types，但是关于这个 Scala 特定实现的确切细节对于这个答案来说，作品并不重要，这只是试图说明关于依赖类型的两个关键概念

类型可以依赖于值
允许在编译时消除更广泛的错误

// Bring in scope Peano numbers which are integers lifted to type-level
import compiletime.ops.int._

// Match type which reduces to the exact type of an HList element at index IDX
type Elem[L <: Tuple, IDX <: Int] = L match {
  case head *: tail =>
    IDX match {
      case 0 => head
      case S[nextIdx] => Elem[tail, nextIdx]
    }
}

// type of dependently typed function index
type DTF = [L <: Tuple] => L => (idx: Int) => Elem[L, idx.type] 

// implementation of DTF index
val index: DTF = [L <: Tuple] => (hlist: L) => (idx: Int) => {
  hlist.productElement(idx).asInstanceOf[Elem[L, idx.type]]
}

给定依赖类型 DFT 编译器现在能够在编译时捕获以下错误

val a: String = (42 :: "foo" :: Nil)(0).asInstanceOf[String] // run-time error
val b: String = index(42 *: "foo" *: Tuple())(0)             // compile-time error

scastie

【讨论】：

如何处理随机值？比如f(random())会导致编译错误吗？
将f 应用于某个表达式将要求编译器（无论是否有您的帮助）提供该表达式始终是偶数，并且对于random() 不存在这样的证明（因为它实际上可能是奇怪的），因此f(random()) 将无法编译。
-1。此处显示的代码说明了细化类型，它与依赖类型相关但不完全相同。事实上，细化类型的表现力不如依赖类型。
@Xwtek 感谢您的反馈。请参阅编辑后的答案，希望现在提供Pi types in Scala 的示例。
@MarioGalic：但是语言中依赖类型（甚至细化类型）的存在是否不需要在编译时评估许多表达式，否则这些表达式会在运行时进行评估，从而显着增加编译时间？

【解决方案3】：

如果您碰巧了解 C++，很容易提供一个激励示例：

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

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

并考虑这个代码片段（你可以假设 foo 是非空的）：

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

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

问题在于迭代器类型不应该仅仅依赖于容器type，而是实际上依赖于容器object，即它应该是一个“非静态成员类型”：

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 进行比较，您可能会注意到一个可疑的相似性。 ;-)

【讨论】：

【解决方案4】：

引用 Types and Programming Languages (30.5) 一书：

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

λx:T1.t2 由术语索引的术语族

λX::K1.t2 按类型索引的术语族

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

看看这个列表，很明显有一种可能性我们还没有考虑：按术语索引的类型族。这抽象形式也得到了广泛的研究，在依赖类型的量规。

【讨论】：