More Examples

• We can use constructs of ML (but cannot residualize them)

- reify (E-->E-->E)

(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);

> val it =

Abs ("x3",Abs ("x4",

App (Var "x3",Var "x4"))) : exp

Previous slide

Next slide

Back to first slide

View graphic version