Ross Paterson ross at soi.city.ac.uk
Wed Oct 19 11:32:08 EDT 2005

```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
> 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)

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.

```