Material for Learning GADT

I started reading about GADT in Haskell Wiki but didn't feel quite comf开发者_Python百科ortable understanding it. Do you recommend a specific book chapter or a blog post explaining GADT for a Haskell beginner?

---

Apfelmus has made video tutorial for GADTs which might be helpful.

---

I like the example in the GHC manual. It's simple, and it illustrates some key points:

• GADTs let you use Haskell's type system to model the type system of a language you're implementing (the "object language")

• This allows Haskell's static checking to assert that your "compiler passes" or what-not are type preserving. Functions taking object-language terms can assume those terms are well-typed. Functions returning object-language terms are required to produce well-typed terms.

• Pattern matching a GADT constructor causes type refinement. eval has type Term a -> a overall, but the right-hand side for eval (Lit i) has type Int, because the left-hand constructor had type Term Int.

• The Haskell system doesn't care what types you give your GADT constructors. We could just as easily make every constructor in data Term a give a result of type Term a, or Term Bool, and the data definition would still go through. But we wouldn't be able to write eval :: Term a -> a. You choose the GADT "tag types" to model your problem, so that the useful functions you want to write are well-typed.

---

Other links:

• http://www.haskell.org/haskellwiki/Generalised_algebraic_datatype
• http://www.comlab.ox.ac.uk/people/ralf.hinze/talks/FOP.pdf

---

The Haskell wiki's GADTs for dummies is the best explanation I have seen.

The problem I (and I suspect others) have with most introductions is that they show examples of GADTs in terms of syntax which is non-obvious until you understand GADTs. This makes the simplest examples on which everything is built especially hard to fully understand—you can guess at what many of the patterns are doing, but understanding the exact role of every statement is challenging.

The "for dummies" post dissects and builds up the meaning of the syntax along the way to explaining its own basic examples, which makes it a far more useful starting point. I highly recommend it.