(****************************************************************************** plc.fml Type checking and syntactic normalization for Polymorphic Lambda Calculus (PLC) in Fresh OCaml A.M.Pitts 2003-08-03 ******************************************************************************) type t;; (* some type *) type tyvar = t name;; (* type variables, a *) type ty = (* types, t *) Tyvar of tyvar (* a *) | Fun of ty * ty (* t1 -> t2 *) | All of <>ty;; (* All a. t *) type t;; (* some type *) type var = t name;; (* variables, x *) type expr = (* expressions, e *) Var of var (* x *) | Lam of ty * (<>expr) (* \x:t.e *) | App of expr * expr (* e1 e2 *) | Gen of <>expr (* \a.e *) | Spec of expr * ty;; (* e t *) type nf = (* normal forms *) L of ty * (<>nf) | G of <>nf | N of ne and ne = (* neutral forms *) V of var | A of ne * nf | S of ne * ty;; type tyenv = (* typing environments *) (var * ty)list;; exception Typ_error;; let ( |-> ) (a : tyvar) (t : ty) : ty -> ty = (* capture-avoiding substitution of types for type variables in types *) let rec sub (t' : ty) : ty = match t' with Tyvar b -> if a = b then t else Tyvar b | Fun(t1, t2) -> Fun(sub t1, sub t2) | All(<|a|>t1) -> All(<|a|>(sub t1)) (* note that a is automatically fresh for t, so we avoid "capture" in this case! *) in sub;; let rec typ (env : tyenv) (e : expr) : ty = (* type of an expression in a typing environment, if any *) match e with Var x -> (try List.assoc x env with Not_found -> raise Typ_error) | Lam(t, <|x|>e) -> Fun(t, typ ((x, t) :: env) e) | App(e1, e2) -> (match typ env e1 with Fun(t1, t2) -> if t1 = typ env e2 then t2 else raise Typ_error | _ -> raise Typ_error) | Gen(<|a|>e) -> All(<|a|>(typ env e)) (* note that a is automatically fresh for env, so the usual side-condition "a not a free type variable of env" is unnecessary! *) | Spec(e, t) -> (match typ env e with All(<|a|>t1) -> (a |-> t)t1 | _ -> raise Typ_error);; exception Apply_error;; exception Specialize_error;; let rec apply (n : nf) (n' : nf) : nf = (* apply a normal form to a normal form *) match n with L(t1, <>n1) -> sub_nf_nf n' x1 n1 | G _ -> raise Apply_error | N neu -> N(A(neu, n')) and specialize (n :nf) (t : ty) : nf = (* specialize a normal form at a type *) match n with L _ -> raise Specialize_error | G(<>n1) -> sub_ty_nf t a1 n1 | N neu -> N(S(neu, t)) and sub_nf_nf (n' : nf) (x : var) (n : nf) : nf = (* substitute a normal form for a variable in a normal form *) match n with L(t1, <>n1) -> L(t1, <>(sub_nf_nf n' x n1)) | G(<>n1) -> G(<>(sub_nf_nf n' x n1)) | N neu -> sub_nf_ne n' x neu and sub_nf_ne (n' : nf) (x : var) (neu : ne) : nf = (* substitute a normal form for a variable in a neutral form *) match neu with (V x1) as neu1 -> if x = x1 then n' else N(neu1) | A(neu1, n1) -> apply (sub_nf_ne n' x neu1) (sub_nf_nf n' x n1) | S(neu1, t1) -> specialize (sub_nf_ne n' x neu1) t1 and sub_ty_nf (t : ty) (a : tyvar) (n : nf) : nf = (* substitute a type for a type variable in a normal form *) match n with L(t1, <>n1) -> L((a |-> t)t1, <>(sub_ty_nf t a n1)) | G(<>n1) -> G(<>(sub_ty_nf t a n1)) | N neu -> sub_ty_ne t a neu and sub_ty_ne (t : ty) (a : tyvar) (neu : ne) : nf = (* substitute a type for a type variable in a neutral form *) match neu with (V x1) as neu1 -> N(neu1) | A(neu1, n1) -> apply (sub_ty_ne t a neu1) (sub_ty_nf t a n1) | S(neu1, t1) -> specialize (sub_ty_ne t a neu1) ((a |-> t)t1);; let rec eval (e : expr) : nf = (* evaluate an expression to beta-normal form (if any) *) match e with Var x1 -> N(V x1) | Lam(t1, <>e1) -> L(t1, <>(eval e1)) | App(e1, e2) -> apply (eval e1) (eval e2) | Gen(<>e1) -> G(<>(eval e1)) | Spec(e1, t1) -> specialize (eval e1) t1;; let rec reify_nf (n :nf) : expr = (* reify a normal form as an expression *) match n with L(t1, <>n1) -> Lam(t1, <>(reify_nf n1)) | G(<>n1) -> Gen(<>(reify_nf n1)) | N neu -> reify_ne neu and reify_ne (neu : ne) : expr = (* reify a neutral form as an expression *) match neu with V x1 -> Var x1 | A(neu1, n1) -> App(reify_ne neu1, reify_nf n1) | S(neu1, t1) -> Spec(reify_ne neu1, t1);; let normalize (env : tyenv) (e : expr) : expr * ty = (* normalize a well-typed expression *) let t = typ env e in (reify_nf(eval e), t);; let b_equiv (env : tyenv) (e: expr) (e' : expr) : bool = (* beta-equivalence of well-typed expressions *) ((typ env e) = (typ env e')) && ((eval e) = (eval e'));; (******************************************************************** Example: list processing in PLC *********************************************************************) let a, a' = (fresh : tyvar), (fresh : tyvar);; let a_list = (* All a'. a' -> (a -> a' -> a') -> a' *) All(<>( Fun(Tyvar a', Fun(Fun(Tyvar a, Fun(Tyvar a', Tyvar a')), Tyvar a'))));; let x, x', f, l = (fresh : var), (fresh : var), (fresh : var), (fresh : var);; let plc_nil = (* /\a. /\a'. \x' : a'. \f : a -> a' -> a'. x' *) Gen(<>(Gen(<>(Lam(Tyvar a', <>(Lam(Fun(Tyvar a, Fun(Tyvar a', Tyvar a')), <>(Var x'))))))));; typ [] plc_nil = All(<>a_list);; let plc_cons = (* /\a. \x : a. \l : a_list. /\a'. \x' : a'. \f : a -> a' -> a'. f x (l a' x' f) *) Gen(<>(Lam(Tyvar a, <>(Lam(a_list, <>(Gen(<>( Lam(Tyvar a', <>(Lam(Fun(Tyvar a, Fun(Tyvar a', Tyvar a')), <>(App(App(Var f, Var x), App(App(Spec(Var l, Tyvar a'), Var x'), Var f))))))))))))));; typ [] plc_cons = All(<>(Fun(Tyvar a, Fun(a_list, a_list))));; let plc_iter = (* /\a. /\a'. \x' : a'. \f : a -> a' -> a'. \l : a_list. l a' x' f *) Gen(<>(Gen(<>(Lam(Tyvar a', <>( Lam(Fun(Tyvar a, Fun(Tyvar a', Tyvar a')), <>(Lam(a_list, <>(App(App(Spec(Var l, Tyvar a'), Var x'), Var f)))))))))));; typ [] plc_iter = All(<>(All(<>(Fun(Tyvar a', Fun(Fun(Tyvar a, Fun(Tyvar a', Tyvar a')), Fun(a_list, Tyvar a')))))));; let tenv : tyenv = (* [ x' |-> a', f |-> a -> a' -> a' ] *) [(x', Tyvar a'); (f, Fun(Tyvar a, Fun(Tyvar a', Tyvar a')))];; let nil_lhs = (* plc_iter a a' x' f (plc_nil a) This should be beta-equal to x' *) App(App(App(Spec(Spec(plc_iter, Tyvar a), Tyvar a'), Var x'), Var f), Spec(plc_nil, Tyvar a));; typ tenv nil_lhs = Tyvar a';; b_equiv tenv nil_lhs (Var x');; let tenv' : tyenv = (* [ x |-> a, l |-> a_list, x' |-> a', f |-> a -> a' -> a' ] *) (x, Tyvar a) :: (l, a_list) :: tenv;; let cons_lhs = (* plc_iter a a' x' f (plc_cons a x l) *) App(App(App(Spec(Spec(plc_iter, Tyvar a), Tyvar a'), Var x'), Var f), App(App(Spec(plc_cons, Tyvar a), Var x), Var l));; typ tenv' cons_lhs = Tyvar a';; let cons_rhs = (* f x (plc_iter a a' x' f l) *) App(App(Var f, Var x), App(App(App(Spec(Spec(plc_iter, Tyvar a), Tyvar a'), Var x'), Var f), Var l));; typ tenv' cons_rhs = Tyvar a';; (* true! *) b_equiv tenv' cons_lhs cons_rhs;; (* true! *) (********************************************************************* end of plc.ml *********************************************************************)