依赖挑战的数据类型提升答案

【问题标题】：Datatype promotion for dependently challenged依赖挑战的数据类型提升
【发布时间】：2012-01-25 21:45:37
【问题描述】：

阅读完 ghc 7.4。预发布说明和Giving Haskell a Promotion 论文，我仍然对您对提升类型的实际操作感到困惑。例如，GHC 手册给出了以下关于提升数据类型的示例：

data Nat = Ze | Su Nat

data List a = Nil | Cons a (List a)

data Pair a b = Pair a b

data Sum a b = L a | R b

这些作为种类有哪些用途？你能给出（代码）例子吗？

【问题讨论】：

这是个好问题。构建一个好的答案的一种方法可能是翻译您在“cabal install she”时获得的示例文件。我可以发布 SHE 代码，作为对读者的练习：这有用吗？我现在正在尝试安装 7.4，但我正在运行 Leopard，我担心结果会很糟糕。
@pigworker，我试着看一下 SHE 示例，我想我摸索了一些部分，但是一个简单的 SHE 示例，带有一些“傻瓜的 cmets”可能也不错。

标签： haskell types language-design dependent-type

【解决方案1】：

论文本身至少有两个例子：

“1. 简介”说：“例如，我们可能能够确保 [在编译时] 所谓的红黑树确实具有红黑属性”。

“2.1 提升数据类型”讨论了长度索引向量（即具有编译时“索引超出范围”错误的向量）。

您还可以查看此方向的早期工作，例如用于类型安全的异构列表和可扩展集合的 HList 库。 Oleg Kiselyov 有很多相关的作品。您还可以阅读有关使用依赖类型进行编程的作品。 http://www.seas.upenn.edu/~sweirich/ssgip/main.pdf 有 Agda 中类型级计算的介绍性示例，但这些也可以应用于 Haskell。

粗略地说，这个想法是head for 列表被赋予了更精确的类型。而不是

head :: List a -> a

是的

head :: NotEmptyList a -> a

后一个 head 函数比前一个更类型安全：它永远不能应用于空列表，因为它会导致编译器错误。

您需要类型级别的计算来表达类型，例如 NotEmptyList。具有函数依赖关系的类型类、GAGT 和（索引）类型族已经为 haskell 提供了类型级计算的弱形式。您刚才提到的工作在这个方向上做了进一步的阐述。

有关仅使用 Haskell98 类型类的实现，请参阅 http://www.haskell.org/haskellwiki/Non-empty_list。

【讨论】：

我很想看看红黑树的例子。
您能否扩展一下为什么需要 NotEmptyList 类型的类型级计算？至少您提到的 wiki 页面在类型级别上没有任何作用。

【解决方案2】：

Nat 可以是例如用于构造只有在长度相同时才能相加的数值向量，在编译时检查。

【讨论】：