依赖类型

Question

不久前，我遇到了编程语言 Idris，它的“独特卖点”似乎是依赖类型。有人能解释一下依赖类型是什么以及它们正在解决什么样的问题吗？

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 类型注释确保了向量长度的保存。这些是非常简单的示例，说明依赖类型如何帮助构建软件确保正确。

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