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.