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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
