Implementation in ML (2)
(* E : exp typ *)
val E = RR(fn v => v, fn e => e)
(* --> : 'a typ * 'b typ -> ('a -> 'b) typ *)
infixr -->
fun (dom --> codom) =
RR(fn v =>
let val x = gensym ()
in Abs(x, reify codom (v (reflect dom (Var(x)))))
end,
fn e =>
fn x => reflect codom (App(e, reify dom x)))
Previous slide
Next slide
Back to first slide
View graphic version