[Haskell-cafe] GADT on the wiki: I'm lost
Daniel Fischer
daniel.is.fischer at web.de
Wed Apr 22 18:18:42 EDT 2009
Am Mittwoch 22 April 2009 23:30:35 schrieb Peter Verswyvelen:
> 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...
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)
More information about the Haskell-Cafe
mailing list