```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
*********************************************************************)

```

This document was generated using caml2html