Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Implementation in ML (2)

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