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