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

[Peter Verswyvelen]

Yeah that's what I also thought. I tried it first in GHCi, and I got a type
error. I tried it again, and it works now. I must have forgotten to reload
the file or something, cause I made the wrong conclusion. Duh, mea culpa.
On Wed, Apr 22, 2009 at 11:48 PM, Luke Palmer <lrpalmer at gmail.com> wrote:

> 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
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090423/9a7cdaa6/attachment.htm