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"><<a href="mailto:martijn@van.steenbergen.nl">martijn@van.steenbergen.nl</a>></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'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 :: * -> * 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 => (forall ix. s ix -> r ix -> a (r' ix)) -><br>
F s r ix -> a (F s r' 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 => 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 -> Bool) -> p (Input p)<br>
<br>
type SatisfyA s a =<br>
forall p. (Satisfy p, Alternative p, Input p ~ s) => 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 -> 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 "P" (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 :: * -> * -> * where<br>
Satisfy :: (s -> Bool) -> P s s<br>
Point :: a -> P s a<br>
Fmap :: (a -> b) -> P s a -> P s b<br>
Apply :: P s (a -> b) -> P s a -> P s b<br>
Empty :: Parser s a<br>
Choice :: Parser s a -> Parser s a -> 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>