[Haskell-cafe] GADT on the wiki: I'm lost

[Jason Dagit]

On Wed, Apr 22, 2009 at 2:30 PM, Peter Verswyvelen <bugfact at gmail.com> wrote:
> 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-to-version-control-implementation/
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