Am Mittwoch 22 April 2009 23:30:35 schrieb Peter Verswyvelen:
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...
No, that works perfectly fine. *SafeHead> safeHead $ Cons 1 Nil 1 *SafeHead> safeHead $ Cons () Nil () You probably tried something like *SafeHead> safeHead $ silly 2 <interactive>:1:11: Couldn't match expected type `Safe' against inferred type `NotSafe' Expected type: MarkedList () Safe Inferred type: MarkedList () NotSafe In the second argument of `($)', namely `silly 2' In the expression: safeHead $ silly 2 ??? Well, *SafeHead> :t silly silly :: (Num t) => t -> MarkedList () NotSafe The case silly 0 = Nil makes silly have the return type MarkedList t NotSafe (for some unknown t). The other equations for silly fix t as (), but nothing can transform the NotSafe into Safe. Commenting out the first equation of silly yields *SafeHead> :t silly silly :: (Num t) => t -> MarkedList () z *SafeHead> safeHead $ silly 2 ()
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)