[Haskell-cafe] GADT on the wiki: I'm lost
lrpalmer at gmail.com
Wed Apr 22 17:48:40 EDT 2009
On Wed, Apr 22, 2009 at 3:30 PM, Peter Verswyvelen <bugfact at gmail.com>wrote:
> I was reading the explanation of GADTs on the wiki<http://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 at haskell.org
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe