(* This is an implementation of typed-directed normalization by evaluation for the simply-typed lambda-calculus, as described by Pitts in volume 53 of JACM, 2006. *) (* ----------------------------------------------------------------------- *) (* Simple types. *) type typ = | Iota | Arrow of typ * typ (* ----------------------------------------------------------------------- *) (* Since the algorithm is type-directed, we must, at runtime, manipulate lambda-terms that contain type information. It turns out that assuming that every occurrence of a variable is decorated with a type is enough. In a more standard representation of typed lambda-terms, every lambda abstraction would be decorated with the type of the bound variable, while occurrences of variables would be undecorated. This standard representation can easily be converted to the representation used here -- see the end of this file. We cannot, at the moment, statically establish and maintain the invariant that the types carried within our lambda-terms are consistent. For this reason, there are a couple of occurrences of [fail] in the code. *) type term = | TVar of atom * typ | TApp of term * term | TLam of < atom * inner term > (* ----------------------------------------------------------------------- *) (* Normal and atomic terms. *) type normal = | NLam of < atom * inner normal > | NAtomic of atomic type atomic = | AVar of atom | AApp of atomic * normal (* ----------------------------------------------------------------------- *) (* Denotations. *) (* In Pitts' treatment, denotations at a function type are just (finitely supported) functions from denotations to denotations. Since this language does not (yet?) support higher-order functions, we take a more syntactic view and defunctionalize the code. It turns out that we need two kinds of functions, which correspond to suspended calls to the denotation and reflection functions, respectively. *) type denotation = | DIota of normal | DLam of < env: environment * x: atom * inner t: term > where free(x) # bound(env) (* so the order of bindings does not matter *) | DReflectedArrow of typ * typ * atomic type environment binds = | ENil | ECons of x: atom * outer denotation * env: environment where free(x) # bound(env) (* so the order of bindings does not matter *) (* ----------------------------------------------------------------------- *) (* Applying an environment to a variable. In the case where the variable turns out not to belong to the domain of the environment, the variable is reflected. This conforms with Pitts' definition of the initial environment. *) fun denot_variable accepts env (* env *), x (* atom *), typ (* typ *) produces d (* denotation *) where free(d) <= outer(env) U (free(x) \ bound(env)) = case env of | ENil -> reflect (typ, AVar (x)) | ECons (y, d, env) -> if x == y then d else denot_variable (env, x, typ) end end (* ----------------------------------------------------------------------- *) (* Converting a term to a denotation. *) fun denot_term accepts env (* env *), t (* term *) produces d (* denotation *) where free(d) <= outer(env) U (free(t) \ bound(env)) = case t of | TVar (x, typ) -> denot_variable (env, x, typ) | TApp (t1, t2) -> apply_denotation (denot_term (env, t1), denot_term (env, t2)) | TLam (x, t) -> DLam (env, x, t) end (* ----------------------------------------------------------------------- *) (* Reification and reflection. *) fun reify accepts typ (* typ *), d (* denotation *) produces n (* normal *) = case typ, d of | Iota, DIota (n) -> n | Iota, _ -> fail | Arrow (typ1, typ2), _ -> fresh x in NLam (x, reify (typ2, apply_denotation (d, reflect (typ1, (AVar (x)))))) end fun reflect accepts typ (* typ *), a (* atomic *) produces d (* denotation *) = case typ of | Iota -> DIota (NAtomic (a)) | Arrow (typ1, typ2) -> DReflectedArrow (typ1, typ2, a) end (* ----------------------------------------------------------------------- *) (* Interpreting a denotation at a function type, that is, converting it into a function of denotations to denotations. *) fun apply_denotation accepts d1 (* denotation *), d2 (* denotation *) produces d (* denotation *) = case d1 of | DIota (_) -> fail | DLam (env, x, t) -> denot_term (ECons (x, d2, env), t) | DReflectedArrow (typ1, typ2, a) -> reflect (typ2, AApp (a, reify (typ1, d2))) end (* ----------------------------------------------------------------------- *) (* Normalization. *) fun norm accepts typ (* typ *), t (* term *) produces n (* normal *) = reify (typ, denot_term (ENil, t)) (* ----------------------------------------------------------------------- *) (* As announced above, one can also start with a standard representation of typed terms and convert it to the representation used above. *) (* Here is the standard representation of terms. *) type standard_term = | ATVar of atom | ATApp of standard_term * standard_term | ATLam of < atom * inner typ * inner standard_term > (* ----------------------------------------------------------------------- *) (* Converting a standard term to a term in our format requires a type environment that provides the types of the free variables. *) type type_environment binds = | TENil | TECons of x: atom * inner typ * tenv: type_environment where free(x) # bound(tenv) (* so the order of bindings does not matter *) (* ----------------------------------------------------------------------- *) (* Conversion. *) fun convert accepts tenv (* type_environment *), st (* standard_term *) where free(st) <= bound(tenv) produces t (* term *) = case st of | ATVar (x) -> case tenv of | TENil -> absurd | TECons (y, typ, tenv) -> if x == y then TVar (x, typ) else convert (tenv, st) end end | ATApp (st1, st2) -> TApp (convert (tenv, st1), convert (tenv, st2)) | ATLam (x, typ, st) -> TLam (x, convert (TECons (x, typ, tenv), st)) end (* ----------------------------------------------------------------------- *) (* Conversion and normalization, composed. *) fun norm_st accepts tenv (* tenv *), typ (* typ *), st (* standard_term *) where free(st) <= bound(tenv) produces n (* normal *) = norm (typ, convert (tenv, st))