, Sep 21, 2012 at 8:34 AM, Florian Lorenzen
florian.loren...@tu-berlin.de
mailto:florian.loren...@tu-berlin.de wrote:
Hello cafe,
I have the following GADT definitions capturing the simply typed
lambda calculus with de Bruijn indices for variables and
explicitly annotated types
) (TmInt 5))
have the type I expected:
test2 :: Term ctx (TyArrow 'TyInt 'TyInt)
Thank you and 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
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
) = 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.loren...@tu-berlin.de
WWW:http
- Maybe (Term a) tcIf (If c e1 e2) = do c'
- tc c e1' - tc e1 e2' - tc e2 return (TIf c' e1' e2')
Cheers, Pedro
On Fri, Sep 14, 2012 at 11:45 AM, Florian Lorenzen
florian.loren...@tu-berlin.de
mailto:florian.loren...@tu-berlin.de wrote:
Hello cafe,
I have a question wrt. to GADTs
in GHC Haskell.
I very much appreciate any hints and explanations on this.
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
that it is well typed.
May I conclude that the (GHC) Haskell type system is not powerful
enough to type such a typecheck function?
Best regards,
Florian
On 09/14/2012 02:01 PM, Sean Leather wrote:
On Fri, Sep 14, 2012 at 12:45 PM, Florian Lorenzen wrote:
I'd like to transform a value
