[Haskell-cafe] Transforming a ADT to a GADT

[Florian Lorenzen]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Thanks Oleg for this elaboration. I'm now happy with the solution
involving an existential. I first did not realize that I still could
apply functions of type `Term t -> Term t` as soon as I open the package.

On 09/15/2012 01:02 PM, oleg at okmij.org wrote:
> Florian Lorenzen wrote: Chances are that you wanted the following
> 
> typecheck :: {e:Exp} -> Result e where Result e has the type (Just 
> (Term t)) (with some t dependent on e) if e is typeable, and 
> Nothing otherwise. But this is a dependent function type
> (Pi-type). No wonder we have to go through contortions like
> Template Haskell to emulate dependent types in Haskell. Haskell was
> not designed to be a dependently-typed language.
Yes, this is what I was looking for. I know, Haskell is not
dependently typed. But since many dependently typed idioms (like
printf) can already be expressed using the GHC Haskell type system, I
was wondering if this one was also possible.

Best regards,

Florian

- -- 
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/

iEYEARECAAYFAlBW2YIACgkQvjzICpVvX7alFwCgkS5Gq2CfJqxX5ZV2TJQslSDn
a9IAoJCj3HY5J8kU5T1HcCJGDFbUaLrc
=G/Zf
-----END PGP SIGNATURE-----