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

[Martijn van Steenbergen]

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.