* Simon Peyton-Jones
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/Applic... -- Roman I. Cheplyaka :: http://ro-che.info/