haskell - 依赖挑战的数据类型提升

Question

阅读完 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

这些有什么样的用途？你能给出(代码)例子吗？

Answer 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 提供了类型级计算的弱形式。你提到的工作只是在这个方向上进一步阐述。

见 http://www.haskell.org/haskellwiki/Non-empty_list对于仅使用 Haskell98 类型类的实现。