On Wed, Apr 22, 2009 at 3:30 PM, Peter Verswyvelen wrote:

I was reading the explanation of GADTs on the wikihttp://en.wikibooks.org/wiki/Haskell/GADT , 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...

Cons :: t -> MarkedList t y -> MarkedList t z Note the different variables y and z. Cons 42 y has type MarkedList Int a, for any type a, including Safe, NotSafe, and ElephantBanana.

Am I missing something or is this wikibook just confusing?

Does anybody have good links to examples of GADTs?

Yampa surely seems a good example, but it's a bit too advanced.

data NotSafe data Safe

data MarkedList :: * -> * -> * where Nil :: MarkedList t NotSafe Cons :: t -> MarkedList t y -> MarkedList t z

safeHead :: MarkedList x Safe -> x safeHead (Cons x _) = x

silly 0 = Nil silly 1 = Cons () Nil silly n = Cons () $ silly (n-1)

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Wed, Apr 22, 2009 at 2:30 PM, Peter Verswyvelen 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-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

Hoi Peter, Peter Verswyvelen wrote:

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...

I use GADTs for two things: 1) Type witnesses for families of data types. An example from the MultiRec paper (by heart so it might differ slightly):

data AST :: * -> * where Expr :: AST Expr Stmt :: AST Stmt

This allows for defining functions that work on all types in a family (simplified example):

hmapA :: Applicative a => (forall ix. s ix -> r ix -> a (r' ix)) -> F s r ix -> a (F s r' ix)

Where s is the family (e.g. the AST defined above). While the function has to be polymorphic in ix, it is passed a value of type s ix which it can pattern match on to refine ix to a known type. 2) Capturing polymorphic constrained values and manipulating them:

class Functor p => Satisfy p where -- | The type of the input symbols. type Input p :: *

-- | Recognise a symbol matching a predicate. satisfy :: (Input p -> Bool) -> p (Input p)

type SatisfyA s a = forall p. (Satisfy p, Alternative p, Input p ~ s) => p a

Then you can write:

transform :: SatisfyA s A -> SatisfyA s B

which can transform such a polymorphic value in any way you desire by instantiating it to an internal GADT "P" (see below), transforming it, then making it polymorphic again:

data P :: * -> * -> * where Satisfy :: (s -> Bool) -> P s s Point :: a -> P s a Fmap :: (a -> b) -> P s a -> P s b Apply :: P s (a -> b) -> P s a -> P s b Empty :: Parser s a Choice :: Parser s a -> Parser s a -> Parser s a

instance Satisfy (P s) where ... instance Functor (P s) where ... instance Applicative (P s) where ... instance Alternative (P s) where ...

The neat thing about this is that if you write your parser polymorphically, you can then transform it *before* instantiating it to a specific parser library (e.g. Parsec, UUParser). Hope this helps, Martijn.