types - 依赖类型

Question

关闭。这个问题需要更多focused .它目前不接受答案。












想改善这个问题吗？更新问题，使其仅关注一个问题 editing this post .

5年前关闭。




Improve this 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 type 就是我们所说的类型族:对于每个值 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。