依赖类型

Question

不久前我遇到了编程语言 Idris，它 "unique selling point" 似乎是依赖类型。有人可以解释什么是依赖类型以及它们正在解决什么样的问题吗？

Answer 1

好吧，依赖类型允许表达在编译时检查的数据类型不变量。依赖类型的典型示例是长度索引列表，也称为向量。向量的 Idris 定义是：

data Vec (A : Type) : Nat -> Type where
   Nil  : Vec A 0
   Cons : A -> Vec A n -> Vec A (S n)

其中类型 Nat 对应 Peano 表示法中的自然数：

data Nat = Z | S Nat

请注意，Vec A 类型就是我们所说的类型族：对于每个值 n : Nat，我们都有一个类型 Vec A n，包含长度为 n 的向量。

在其类型中具有长度允许一些列表函数通过构造是正确的。一个简单的例子是安全列表头函数：

head : Vec a (S n) -> a
head (x :: xs) = x

因为我们要求只将非空向量传递给 head 函数 - 注意索引 S n 需要非零值 - Idris 编译器保证 head 永远不会应用于空列表.

另一个例子是向量的串联，确保其结果的长度等于其参数长度的总和：

(++) : Vec a n -> Vec a m -> Vec a (n + m)
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

请注意，连接长度属性由连接函数类型保证。其他应用是证明向量上的传统映射函数保持其长度：

map : (a -> b) -> Vec a n -> Vec b n 
map f [] = []
map f (x :: xs) = f x :: map f xs

同样，向量长度保存由 map 类型注释确保。这些是依赖类型如何帮助构建软件确保正确性的非常简单的示例。

可以在 The Power of Pi 中找到更有说服力的依赖类型编程（使用 Agda 编程语言）的示例。我没有这样做过，但我相信本文的所有示例都可以毫无困难地移植到 Idris。

Dependent types