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.
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
