No polymorphic abstraction
# (function x -> x x) (function x -> x)
This expression has type 'a -> 'b but is here used with type 'a
# let x = function x -> x in x x
# sem1 (Appl(Fun(Id "x", Appl(Var(Id "x"),Var(Id "x"))),(Fun(Id "x",Var(Id "x")))) ) 0;;
- : eval = Forall ([], Notype), []
# sem1 (Let(Id "x",Fun(Id "x",Var(Id "x")),Appl(Var(Id "x"),Var(Id "x"))) ) 0;;
- : eval = Forall (["var2"], Mkarrow (Vvar "var2", Vvar "var2")), [...]
- universally quantifying the variable bound to the formal parameter in the lambda abstraction does not work
- with polymorphic abstraction the semantics of the following constructs should be equivalent (no need for let)
- let x = e1 in e2 and (function x -> e2) e1
- this is not the case as shown by the following example