plc.ml(******************************************************************************

  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 <<tyvar>>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 * (<<var>>expr) (* \x:t.e *)
  | App of expr * expr        (* e1 e2 *)
  | Gen of <<tyvar>>expr      (* \a.e *)
  | Spec of expr * ty;;       (* e t *)

type nf =                     (* normal forms *)
    L of ty * (<<var>>nf)
  | G of <<tyvar>>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, <<x1>>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(<<a1>>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, <<x1>>n1) -> L(t1, <<x1>>(sub_nf_nf n' x n1))
    | G(<<a1>>n1) -> G(<<a1>>(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, <<x1>>n1) -> L((a |-> t)t1, <<x1>>(sub_ty_nf t a n1))
    | G(<<a1>>n1) -> G(<<a1>>(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, <<x1>>e1) -> L(t1, <<x1>>(eval e1))
    | App(e1, e2) -> apply (eval e1) (eval e2)
    | Gen(<<a1>>e1) -> G(<<a1>>(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, <<x1>>n1) -> Lam(t1, <<x1>>(reify_nf n1))
    | G(<<a1>>n1) -> Gen(<<a1>>(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(<<a'>>(
    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(<<a>>(Gen(<<a'>>(Lam(Tyvar a', 
  <<x'>>(Lam(Fun(Tyvar a, Fun(Tyvar a', Tyvar a')), 
  <<f>>(Var x'))))))));;

typ [] plc_nil = All(<<a>>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(<<a>>(Lam(Tyvar a, <<x>>(Lam(a_list, <<l>>(Gen(<<a'>>(
    Lam(Tyvar a', <<x'>>(Lam(Fun(Tyvar a, Fun(Tyvar a', Tyvar a')),
    <<f>>(App(App(Var f, Var x), App(App(Spec(Var l, Tyvar a'), 
    Var x'), Var f))))))))))))));;

typ [] plc_cons = All(<<a>>(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(<<a>>(Gen(<<a'>>(Lam(Tyvar a', <<x'>>(
    Lam(Fun(Tyvar a, Fun(Tyvar a', Tyvar a')), <<f>>(Lam(a_list,
    <<l>>(App(App(Spec(Var l, Tyvar a'), Var x'), Var f)))))))))));;

typ [] plc_iter = 
    All(<<a>>(All(<<a'>>(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
*********************************************************************)