Thanks to everybody. Now I have enough articles to ruin my spare time again :)<div><br><div class="gmail_quote">On Thu, Apr 23, 2009 at 4:20 PM, Martijn van Steenbergen <span dir="ltr">&lt;<a href="mailto:martijn@van.steenbergen.nl">martijn@van.steenbergen.nl</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">Hoi Peter,<div class="im"><br>
<br>
Peter Verswyvelen wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Sure I understand what a GADT is, but I&#39;m looking for practical examples, and the ones on the wiki seem to show what you *cannot* do with them...<br>
</blockquote>
<br></div>
I use GADTs for two things:<br>
<br>
<br>
1) Type witnesses for families of data types. An example from the MultiRec paper (by heart so it might differ slightly):<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
data AST :: * -&gt; * where<br>
  Expr :: AST Expr<br>
  Stmt :: AST Stmt<br>
</blockquote>
<br>
This allows for defining functions that work on all types in a family (simplified example):<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
hmapA :: Applicative a =&gt; (forall ix. s ix -&gt; r ix -&gt; a (r&#39; ix)) -&gt;<br>
  F s r ix -&gt; a (F s r&#39; ix)<br>
</blockquote>
<br>
Where s is the family (e.g. the AST defined above). While the function has to be polymorphic in ix, it is passed a value of type s ix which it can pattern match on to refine ix to a known type.<br>
<br>
<br>
2) Capturing polymorphic constrained values and manipulating them:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
class Functor p =&gt; Satisfy p where<br>
  -- | The type of the input symbols.<br>
  type Input p :: *<br>
<br>
  -- | Recognise a symbol matching a predicate.<br>
  satisfy :: (Input p -&gt; Bool) -&gt; p (Input p)<br>
<br>
type SatisfyA s a =<br>
  forall p. (Satisfy p, Alternative p, Input p ~ s) =&gt; p a<br>
</blockquote>
<br>
Then you can write:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
transform :: SatisfyA s A -&gt; SatisfyA s B<br>
</blockquote>
<br>
which can transform such a polymorphic value in any way you desire by instantiating it to an internal GADT &quot;P&quot; (see below), transforming it, then making it polymorphic again:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
data P :: * -&gt; * -&gt; * where<br>
  Satisfy :: (s -&gt; Bool) -&gt; P s s<br>
  Point :: a -&gt; P s a<br>
  Fmap :: (a -&gt; b) -&gt; P s a -&gt; P s b<br>
  Apply :: P s (a -&gt; b) -&gt; P s a -&gt; P s b<br>
  Empty :: Parser s a<br>
  Choice :: Parser s a -&gt; Parser s a -&gt; Parser s a<br>
<br>
instance Satisfy (P s) where ...<br>
instance Functor (P s) where ...<br>
instance Applicative (P s) where ...<br>
instance Alternative (P s) where ...<br>
</blockquote>
<br>
The neat thing about this is that if you write your parser polymorphically, you can then transform it *before* instantiating it to a specific parser library (e.g. Parsec, UUParser).<br>
<br>
Hope this helps,<br><font color="#888888">
<br>
Martijn.<br>
</font></blockquote></div><br></div>