On Wed, Apr 22, 2009 at 2:30 PM, Peter Verswyvelen
I was reading the explanation of GADTs on the wiki , and but can't make any sense of the examples. Sure I understand what a GADT is, but I'm looking for practical examples, and the ones on the wiki seem to show what you *cannot* do with them... For example, the article gives an alternative approach to the safeHead function (see code below) But now that does not work either, since Cons x y never evaluates to MarkedList x Safe, so safeHead (Cons 1 Nil) will give a type error... Am I missing something or is this wikibook just confusing? Does anybody have good links to examples of GADTs?
Thrists, or type directed lists. You can find them in the darcs source code (darcs doesn't use Gabor's terminology): http://darcs.net/src/Darcs/Ordered.hs And an explanation of how darcs uses them: http://blog.codersbase.com/2009/03/25/type-correct-changes-a-safe-approach-t... And Gabor's explanation of how to use Thrists them: http://www.opendylan.org/~gabor/Thrist-draft-2007-07-16.pdf If you flip to the appendices of my thesis I do have a brief intro to GADTs as well as a listing of some operations we defined for our GADT based lists, and the slides from my defense talk have an example or two. You can get pdfs of both from the blog link above. If you're already familiar with type classes, you'll want to try to figure out how GADTs are similar and different to type classes. For example, a type class is an open set of types that share an interface (the functions in the type class), but once it is defined that interface is (mostly) closed. You can only add things on top of the interface instead of extending it directly. On the other hand, each data constructor of the GADT behaves similarly to a type in a type class. Except, in the GADT case, the set of types (really data constructors) is closed and the interface they share (functions on your GADT) is open. Another interesting aspect of GADTs is the way in which they allow you to combine existentially quantified types with phantom types along side our usual type variables. Keeping in mind the similarity between type classes, you might notice that specifying the relationship between type variables in a GADT data constructor is similar to using multiparameter type classes and functional dependencies. If you're already familiar with the type hackery that people accomplish with type classes then you should also recognize the power of GADTs. Some benefits of GADTs over type class hackery include, GADT type checking is decidable and at run-time GHC doesn't have to pass dictionaries AFAIK like it does with type classes. I hope that helps, Jason