[Haskell-cafe] Regular Expressions without GADTs

[Ross Paterson]

On Wed, Oct 19, 2005 at 03:17:41PM +0100, Conor McBride wrote:
> I was just about to send, when up popped Ross's program, which does give 
> me a datatype, including just enough extra stuff to support functoriality.
> 
> >>data RegExp tok a
> >>	= Zero
> >>	| One a
> >>	| Check (tok -> a) (tok -> Bool)
> >>	| Plus (RegExp tok a) (RegExp tok a)
> >>	| forall b. Mult (RegExp tok (b -> a)) (RegExp tok b)
> >>	| forall e. Star ([e] -> a) (RegExp tok e)
> 
> This combines several dodges rather neatly. You can see the traces of 
> the translation from GADT to nested-datatype-with-equations, but instead 
> of saying forall e. Star (Eq [e] a) (RegExp tok e), Ross has kept just 
> the half of the iso he needs in order to extract the parsed value. 

The direction I've kept is the one that matters if everything is
covariant, because

	forall a. F a -> T (G a)
	~=
	forall a, b. (G a -> b) -> F a -> T b

if F, G and T are functors.  So we can translate

	data T :: * -> * where
		C :: F a -> T (G a)
to
	data T b
		= forall a. C (G a -> b) (F a)

and the mechanical translation of your GADT is

data RegExp tok a
	= Zero (Empty -> a) Empty
	| One (() -> a) ()
	| Check (tok -> a) (tok -> Bool) (RegExp tok a)
	| forall b c. Plus (Either b c -> a) (RegExp tok b) (RegExp tok c)
	| forall b c. Mult ((b, c) -> a) (RegExp tok b) (RegExp tok c)
	| forall e. Star ([e] -> a) (RegExp tok e)

A little simplification (ignoring lifted types here and there) yields
the version I gave.

And of course we're no longer assuming that the function is half of an iso.

> Throwing away the other half more-or-less allows him to hide the 
> head-glueing functions inside the grammar of the regular expressions. In 
> effect, Map has been distributed through the syntax.