什么是依赖类型？

有人能给我解释一下依赖性输入吗？我在哈斯克尔、卡宴、埃皮格拉姆或其他函数式语言方面没有什么经验，所以你能使用的术语越简单，我就会越欣赏它！

21092 次浏览
小开

引用《类型与编程语言》一书(30.5) :

这本书的大部分内容都与形式化抽象有关 各种各样的机制。在简单类型的 lambda 微积分中，我们 形式化了取一个术语并抽象出一个术语的操作 子项，产生一个函数，以后可以通过 在 SystemF中，我们考虑了 operation of taking a term and abstracting out a type, yielding a term that can be instantiated by applying it to various types. Inλω, we 概括了简单类型的 lambda 微积分“ one”的机制 升级,”获取一个类型并抽象出一个子表达式以获取 a type operator that can later be instantiated by applying it to 一种方便的方式来思考所有这些形式的 abstraction is in terms of families of expressions, indexed by other 一个普通的匿名函数 ABc0 术语 [x -> s]t1被术语 s索引。类似地，类型抽象 λX::K1.t2是由类型索引的一系列术语和一个类型运算符 是由类型索引的类型族。

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

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

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

看看这个列表，很明显有一种可能性 我们还没有考虑: 按术语索引的类型族 抽象的形式也被广泛研究 依附类型的规则。

小开
最佳答案

考虑一下: 在所有像样的编程语言中，您都可以编写函数，例如。

def f(arg) = result

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

现在，有些语言允许您定义多态(又名泛型)值:

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

Here, empty takes a type T and computes a value. It is a function from types to values.

Usually, you can also have generic type definitions:

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，因此是术语。

小开

如果你碰巧知道 C + + ，很容易举出一个激励人心的例子:

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

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

and consider this code fragment (you may assume foo is non-empty):

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

Such a feature, the ability to express a type (foo.iterator) which depends on a term (foo), is exactly what dependent typing means.

你之所以不经常看到这个特性，是因为它打开了一个巨大的蠕虫罐头: 你突然发现，在编译时，为了检查两个类型是否相同，你不得不证明两个表达式是等价的(在运行时总是产生相同的值)。因此，如果你比较维基百科的 依赖类型语言列表和 定理证明列表定理证明列表，你可能会注意到一个可疑的相似之处。;-)

小开

依赖类型使较大的 logic errors集在 编译时被消除。为了说明这一点，考虑以下关于函数 f的规范:

函数 f必须只接受 甚至整数作为输入。

如果没有依赖类型，你可能会这样做:

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

这里，编译器无法检测 n是否确实是偶数，也就是说，从编译器的角度来看，以下表达式是 OK 的:

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

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

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

我们说 类型 n.IsEven.type依赖于 value n，因此术语 受养人类别。

As a further example let us define a dependently typed function where the return type will depend on the value argument.

使用 Scala 3工具，考虑下面的 异质性列表，它保持每个元素的精确类型(而不是推导出一个公共的最小上界)

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

The objective is that indexing should not lose any compile-time type information, for example, after indexing the third element the compiler should know it is exactly a 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 of type Int, the return type is Elem[L, idx.type]

where again we note how the return type depends on the value idx.

这里有一个完整的实现作为参考，它使用了类型级别的整数的 literal-based singleton types、 皮诺实现、 匹配类型和 dependent functions types，但是这个特定于 Scala 的实现如何工作的确切细节对于这个答案来说并不重要，它只是试图说明两个关于依赖类型的关键概念

  1. 类型可以依赖于值
  2. 它允许在编译时消除更广泛的错误集
// 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

小开

我会尽量提供一个直奔主题的答案。

A dependent type is the label used to indicate that the output's type (i.e. the type of the co-domain) depends on the actual input value/argument passed to the (dependent) function. e.g. F:forall a:A, Y(A) means the input type of F is A and that depending on the specific value of a the 输出类型输出类型 will be Y(a). So the output type depends on the input argument.

对于一个普通函数，我们通常写 f: A -> B，这意味着函数 f，任何 A类型的输入(非正式的 \forall a \in A或 a:A)返回一些 B类型的元素(非正式的 some a \in B或 b:A)。这是一个“正常”函数类型。但是，依赖类型表示(依赖)函数 F的输出类型取决于参数。类似地，输出类型也是通过参数的值进行索引的(即“依赖”)。例如，我喜欢的符号(没有其他人使用 afaik)是 F: a:A -> Y(a)或者常用的符号 f0。这些表示法只是说 F接受 A中的一些元素 f2(即类型为 A) ，并返回类型为 f6的一些元素 f5(或者如果你喜欢索引集更多地使用 f7)。它仅仅意味着 F的输出类型根据输入值 f2到 F的不同而变化。

一个常见的例子是函数 F: forall n:Nat, Vector n，它显式地指定返回/输出的数组的大小。所以如果你调用 F(a)，那么输出类型为 Vector n，这意味着它只能返回一个大小为 n的矢量，表示为 F(a):Y(a)。正如您可以猜到的那样，如果您总是以某种方式保证这种返回类型得到尊重，那么就会使得出现绑定错误变得更加困难(这对安全性有好处)。

事实上，我很喜欢维基百科关于产品类型的文章部分，并且认为它非常全面。如果它的一些部分没有意义的小部分问我在这里，我很高兴澄清在评论部分 https://en.wikipedia.org/wiki/Dependent_type#Formal_definition。希望以后能更详细地解释这篇文章的内容——特别是产品类型的含义以及它与笛卡尔产品的关系。

小开

如果表达式的类型依赖于某个值，则称其为依赖类型。

以 C + + 为例，表达式“ int”是整数类型，它的类型不依赖于任何东西，总是 一样。让我们定义另一个类型“ int (x)”，其中 x 是一个数字。让我们将 int (x)类型的用途定义为 帮助我们得到一个只有“ x”位数的整数。因此，int (x)的类型取决于 x 的值，其中 x 的值 可以在运行时确定。例如，我们可以有一个包含一个表达式“ int (x)”的语句，其中 of x is passed as an argument to the function. What we are saying is that, for example, int(2) and int(3) are of different data types, i.e. how they behave 在计算过程中是不同的。


提交答案