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.