GADTs in the wild

Roman Cheplyaka roma at
Tue Aug 14 23:22:44 CEST 2012

* Simon Peyton-Jones <simonpj at> [2012-08-14 11:32:19+0000]
> This message is to invite you to send me your favourite example of
> using a GADT to get the job done.  Ideally I'd like to use examples
> that are (a) realistic, drawn from practice (b) compelling and (c)
> easy to present without a lot of background.  Most academic papers
> only have rather limited examples, usually eval :: Term t -> t, but I
> know that GADTs are widely used in practice.
> Any ideas from your experience, satisfying (a-c)?  If so, and you can
> spare the time, do send me a short write-up. Copy the list, so that we
> can all benefit.

Here's how you can encode regular expressions as a GADT:

data RE s a where
    Eps :: RE s ()
    Sym :: (s -> Bool) -> RE s s
    Alt :: RE s a -> RE s b -> RE s (Either a b)
    Seq :: RE s a -> RE s b -> RE s (a, b)
    Rep :: RE s a -> RE s [a]

If you add one more constructor, Fmap :: (a -> b) -> RE s a -> RE s b,
RE will become Functor and Applicative (and half-Alternative).

This is a simplified extract from the regex-applicative library:

Roman I. Cheplyaka ::

More information about the Glasgow-haskell-users mailing list