GADTs in the wild

[Roman Cheplyaka]

* Simon Peyton-Jones <simonpj at microsoft.com> [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:
https://github.com/feuerbach/regex-applicative/blob/master/Text/Regex/Applicative/Types.hs#L58

-- 
Roman I. Cheplyaka :: http://ro-che.info/