针对依赖性挑战的数据类型升级

Question

通过ghc 7.4阅读.预发行说明和给予Haskell一份推广文章,我仍然对你实际使用推广类型做了什么感到困惑.例如,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为列表提供了更精确的类型.代替

head :: List a -> a

它是

head :: NotEmptyList a -> a

后一个head函数比fomer更安全:它永远不能应用于空列表,因为它会导致编译器错误.

您需要类型级计算来表达NotEmptyList等类型.具有功能依赖性的类型类,GAGT和(索引)类型族已经为haskell提供了弱类型的类型级计算.你提到的工作只是在这方面进一步阐述.

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

Answer 2

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