依赖类型

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 Atype是我们所谓的类型族：对于每个值，n : Nat我们都有一个类型Vec A n为length的向量n。

具有长度的类型可以使某些列表功能在构造上是正确的。一个简单的例子是安全列表头函数：

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

由于我们要求仅将非空向量传递给head函数-请注意索引S n要求非零值-Idris编译器保证不会将head应用于空列表。

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

(++) : 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。