More Examples
We can use constructs of ML (but cannot residualize them)
(fn x => fn y => if 3+5ɟ then x else y);
> val it = Abs ("x1",Abs ("x2",Var "x2")) : exp
We may specify a non-principal type (but get a redundant result)
- reify ((E-->E)-->(E-->E)) (fn x => x);
App (Var "x3",Var "x4"))) : exp