functional-programming - 什么是依赖类型？

Question

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

score 137 · Accepted Answer

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

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

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

score 38 · Accepted Answer

从属类型可以在编译时消除更大的逻辑错误集。为了说明这一点，请考虑以下关于 function 的规范：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路径依赖类型的说明性示例，说明我们如何尝试实现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

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

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

我们说类型 n.IsEven.type取决于值 n，因此术语依赖类型。

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

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

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

或者换句话说

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

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

这是完整的实现供参考，它使用基于文字的单例类型、类型级别的整数的Peano实现、匹配类型和依赖函数类型，但是有关此 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

斯卡斯蒂

score 27 · Accepted Answer

如果您碰巧了解 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即使它们在语义上完全不兼容。

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

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

这样的特性，即表达依赖于术语 (foo) 的类型 (foo.iterator) 的能力，正是依赖类型的含义。

你不经常看到这个特性的原因是因为它打开了一大堆蠕虫：你突然陷入这样一种情况，在编译时检查两种类型是否相同，你最终不得不证明两个表达式是等价的（在运行时总是会产生相同的值）。因此，如果您将维基百科的依赖类型语言列表与其定理证明者列表进行比较，您可能会注意到可疑的相似性。;-)

score 4 · Accepted Answer

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

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

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

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

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

查看此列表，很明显有一种可能性我们尚未考虑：按术语索引的类型族。在依赖类型的标题下，这种抽象形式也得到了广泛的研究。

functional-programming - 什么是依赖类型？

4 回答 4

Related

Reference