Re: [Haskell-cafe] Transforming a ADT to a GADT

-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Thanks Erik. This made the issue clear to me. Best regards, Florian On 09/14/2012 03:22 PM, Erik Hesselink wrote:

On Fri, Sep 14, 2012 at 2:27 PM, Erik Hesselink wrote:

...

In general, I think you have to work inside an existential. So you hide the type of the parsed Term inside an existential. If you want to apply functions to this Term, you unpack, call the function, and repack.

Maybe I should expand what I mean by this. Let's say you have:

data SomeTerm where SomeTerm :: Term a -> SomeTerm

Your typecheck function goes:

typecheck :: Exp -> SomeTerm

and you want to apply:

transform :: Term t -> Term t

You should do something like:

f (SomeTerm t) = SomeTerm (transform t)

Or, more generally:

onSomeTerm :: (forall t. Term t -> Term t) -> SomeTerm -> SomeTerm onSomeTerm f (SomeTerm t) = SomeTerm (f t)

Erik

- -- Florian Lorenzen Technische Universität Berlin Fakultät IV - Elektrotechnik und Informatik Übersetzerbau und Programmiersprachen Sekr. TEL12-2, Ernst-Reuter-Platz 7, D-10587 Berlin Tel.: +49 (30) 314-24618 E-Mail: florian.lorenzen@tu-berlin.de WWW: http://www.user.tu-berlin.de/florenz/ -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.11 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://www.enigmail.net/ iEYEARECAAYFAlBW2bgACgkQvjzICpVvX7Zr3QCfbIqkX9WqM69NLyk98aqyNcYe RrUAniGndhj9OTl9XIoUBC/hoBI1lwML =hReY -----END PGP SIGNATURE-----