haskell - 学习 GADT 的材料

Question

我开始在 Haskell Wiki 中阅读有关 GADT 的内容，但对理解它感到不太自在。您是否会为 Haskell 初学者推荐特定的书籍章节或解释 GADT 的博客文章？

score 16 · Accepted Answer

16

Apfelmus为 GADT 制作了视频教程，这可能会有所帮助。

于 2010-10-26T05:22:29.220 回答

score 6 · Accepted Answer

我喜欢GHC 手册中的示例。这很简单，它说明了一些关键点：

GADT 让您可以使用 Haskell 的类型系统对您正在实现的语言（“对象语言”）的类型系统进行建模
这允许 Haskell 的静态检查断言你的“编译器通过”或者什么不是类型保留。采用对象语言术语的函数可以假设这些术语是良好类型的。需要返回对象语言术语的函数才能生成类型良好的术语。
匹配 GADT 构造函数的模式会导致类型细化。 eval总体上具有类型Term a -> a，但右侧eval (Lit i)具有类型Int，因为左侧构造函数具有类型Term Int。
Haskell 系统不关心你给你的 GADT 构造函数什么类型。我们可以很容易地让每个构造函数data Term a给出一个类型的结果Term a，或者Term Bool，并且data定义仍然会通过。但是我们不能写eval :: Term a -> a。您选择 GADT“标签类型”来为您的问题建模，以便您想要编写的有用函数是类型良好的。

score 1 · Accepted Answer

Haskell wiki 的GADTs for dummy是我见过的最好的解释。

我（我怀疑其他人）在大多数介绍中遇到的问题是，它们在语法方面显示了 GADT 的示例，在您理解 GADT 之前，这些示例是不明显的。这使得构建所有内容的最简单示例特别难以完全理解——您可以猜测许多模式在做什么，但理解每个语句的确切作用是具有挑战性的。

“for dummies”帖子剖析并构建了语法的含义，并解释了它自己的基本示例，这使其成为一个更有用的起点。我强烈推荐它。

score 1 · Accepted Answer

其他链接：

4 回答 4