[Haskell-cafe] GADT on the wiki: I'm lost
Martijn van Steenbergen
martijn at van.steenbergen.nl
Thu Apr 23 10:20:46 EDT 2009
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
> 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,
More information about the Haskell-Cafe