Implementation in ML (1)
Straightforward Implementation Fails to Type-Check, Because ? and ? are Dependent Functions
Solution: Represent a Type ? by a Pair of Functions (??, ??) [Yang 98] [Rhiger 99]
datatype 'a typ = RR of ('a -> exp) * (exp -> 'a)
(* reify : 'a typ -> 'a -> exp *)
fun reify (RR(f, _)) v = f v
(* reflect : 'a typ -> exp -> 'a *)
fun reflect (RR(_, f)) e = f e