Martijn van Steenbergen martijn at van.steenbergen.nl
Thu Apr 23 10:20:46 EDT 2009

```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 ...