<div class="gmail_quote">On Wed, Apr 22, 2009 at 3:30 PM, Peter Verswyvelen <span dir="ltr"><<a href="mailto:bugfact@gmail.com">bugfact@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
I was reading the explanation of <a href="http://en.wikibooks.org/wiki/Haskell/GADT" target="_blank">GADTs on the wiki</a> , and but can't make any sense of the examples.<div><br></div><div>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...</div>
<div><br></div><div>For example, the article gives an alternative approach to the safeHead function (see code below)</div><div><br></div><div>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...</div>
</blockquote><div><br></div><div><span class="Apple-style-span" style="font-family: -webkit-sans-serif; font-size: 18px; line-height: 27px; "><pre style="padding-top: 1em; padding-right: 1em; padding-bottom: 1em; padding-left: 1em; border-top-width: 1px; border-right-width: 1px; border-bottom-width: 1px; border-left-width: 1px; border-top-style: dashed; border-right-style: dashed; border-bottom-style: dashed; border-left-style: dashed; border-top-color: rgb(47, 111, 171); border-right-color: rgb(47, 111, 171); border-bottom-color: rgb(47, 111, 171); border-left-color: rgb(47, 111, 171); color: black; background-color: rgb(249, 249, 249); line-height: 1.1em; ">
<span style="font-size: small; ">Cons :: t -> MarkedList t y -> MarkedList t z</span></pre></span></div><div> </div><div>Note the different variables y and z. Cons 42 y has type MarkedList Int a, for any type a, including Safe, NotSafe, and ElephantBanana.</div>
<div><br></div><div><br></div><div><br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;"><div></div>
<div><br></div><div>Am I missing something or is this wikibook just confusing?</div><div><br></div><div>Does anybody have good links to examples of GADTs? </div><div><br></div><div>Yampa surely seems a good example, but it's a bit too advanced. </div>
<div><br></div><div><span style="font-family:-webkit-sans-serif;font-size:18px;line-height:27px"><pre style="padding-top:1em;padding-right:1em;padding-bottom:1em;padding-left:1em;border-top-width:1px;border-right-width:1px;border-bottom-width:1px;border-left-width:1px;border-top-style:dashed;border-right-style:dashed;border-bottom-style:dashed;border-left-style:dashed;border-top-color:rgb(47, 111, 171);border-right-color:rgb(47, 111, 171);border-bottom-color:rgb(47, 111, 171);border-left-color:rgb(47, 111, 171);color:black;background-color:rgb(249, 249, 249);line-height:1.1em">
<span style="font-size:small">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)</span></pre></span></div>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br>