[Haskell-cafe] Transforming a ADT to a GADT

[Florian Lorenzen]

-----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
> <hesselink at gmail.com> 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 at 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-----