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

[Peter Verswyvelen]

Thanks to everybody. Now I have enough articles to ruin my spare time again
:)
On Thu, Apr 23, 2009 at 4:20 PM, Martijn van Steenbergen <
martijn at van.steenbergen.nl> wrote:

> Hoi Peter,
>
> Peter Verswyvelen wrote:
>
>> 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...
>>
>
> I use GADTs for two things:
>
>
> 1) Type witnesses for families of data types. An example from the MultiRec
> paper (by heart so it might differ slightly):
>
>  data AST :: * -> * where
>>  Expr :: AST Expr
>>  Stmt :: AST Stmt
>>
>
> This allows for defining functions that work on all types in a family
> (simplified example):
>
>  hmapA :: Applicative a => (forall ix. s ix -> r ix -> a (r' ix)) ->
>>  F s r ix -> a (F s r' ix)
>>
>
> 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.
>
>
> 2) Capturing polymorphic constrained values and manipulating them:
>
>  class Functor p => Satisfy p where
>>  -- | The type of the input symbols.
>>  type Input p :: *
>>
>>  -- | Recognise a symbol matching a predicate.
>>  satisfy :: (Input p -> Bool) -> p (Input p)
>>
>> type SatisfyA s a =
>>  forall p. (Satisfy p, Alternative p, Input p ~ s) => p a
>>
>
> Then you can write:
>
>  transform :: SatisfyA s A -> SatisfyA s B
>>
>
> 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:
>
>  data P :: * -> * -> * where
>>  Satisfy :: (s -> Bool) -> P s s
>>  Point :: a -> P s a
>>  Fmap :: (a -> b) -> P s a -> P s b
>>  Apply :: P s (a -> b) -> P s a -> P s b
>>  Empty :: Parser s a
>>  Choice :: Parser s a -> Parser s a -> Parser s a
>>
>> instance Satisfy (P s) where ...
>> instance Functor (P s) where ...
>> instance Applicative (P s) where ...
>> instance Alternative (P s) where ...
>>
>
> 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).
>
> Hope this helps,
>
> Martijn.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090423/07dd2d4d/attachment.htm