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

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