Work on the F type-checker.

demos/system-F-type/F.cppo.ml

 open AlphaLib
 open Abstraction
-#include "AlphaLibMacros.cppo.ml"
 
 (* In this demo, only type variables are handled via AlphaLib. Term variables
    are represented as strings. *)
 
+(* Type variables. *)
+
+type tyvar =
+  Atom.t
+
 (* Types. *)
 
 type ('fn, 'bn) typ =
@@ -16,19 +20,19 @@ type ('fn, 'bn) typ =
 
 (* Term variables. *)
 
-and var = (string[@opaque])
+and tevar = (string[@opaque])
 
 (* Terms. *)
 
 and ('fn, 'bn) term =
-  | TeVar of var
-  | TeAbs of var * ('fn, 'bn) typ * ('fn, 'bn) term
+  | TeVar of tevar
+  | TeAbs of tevar * ('fn, 'bn) typ * ('fn, 'bn) term
   | TeApp of ('fn, 'bn) term * ('fn, 'bn) term
-  | TeLet of var * ('fn, 'bn) term * ('fn, 'bn) term
+  | TeLet of tevar * ('fn, 'bn) term * ('fn, 'bn) term
   | TeTyAbs of ('bn, ('fn, 'bn) term) abstraction
   | TeTyApp of ('fn, 'bn) term * ('fn, 'bn) typ
   | TePair of ('fn, 'bn) term * ('fn, 'bn) term
-  | Teroj of int * ('fn, 'bn) term
+  | TeProj of int * ('fn, 'bn) term
 
 (* Visitor generation. *)
 
@@ -51,7 +55,7 @@ and ('fn, 'bn) term =
 
   ]
 
-(* Operations based on visitors. *)
+(* Type abbreviations. *)
 
 type raw_typ =
   (string, string) typ
@@ -63,6 +67,10 @@ type raw_term =
 type nominal_term =
   (Atom.t, Atom.t) term
 
+(* Operations based on visitors. *)
+
+#include "AlphaLibMacros.cppo.ml"
+
 __FA
 FA(typ)
 FA(term)

demos/system-F-type/FTypeChecker.ml

+open AlphaLib
+open F
+
+(* -------------------------------------------------------------------------- *)
+
+(* Type environments. *)
+
+module TermVar =
+  String
+
+module TermVarMap =
+  Map.Make(TermVar)
+
+type env = {
+  tevars: nominal_typ TermVarMap.t;
+  tyvars: Atom.Set.t
+}
+
+let empty : env =
+  { tevars = TermVarMap.empty; tyvars = Atom.Set.empty }
+
+exception UnboundTermVariable of tevar
+
+let lookup (env : env) (x : tevar) : nominal_typ =
+  try
+    (* The free type variables of this type cannot be captured; see below. *)
+    TermVarMap.find x env.tevars
+  with Not_found ->
+    raise (UnboundTermVariable x)
+
+let extend_with_tevar (env : env) (x : tevar) (ty : nominal_typ) : env =
+  (* We maintain the invariant that the free type variables in the codomain
+     of [env.tevars] form a subset of [env.tyvars]. *)
+  assert (Atom.Set.subset (fa_typ ty) env.tyvars);
+  { env with tevars = TermVarMap.add x ty env.tevars }
+
+let extend_with_tyvar (env : env) (a : tyvar) : env =
+  (* We assume that type variables are globally unique in the term that we are
+     type-checking. Thus, the \Lambda-bound name [a] cannot be in the domain
+     of the environment (i.e., it cannot have been previously bound). Therefore,
+     by the above invariant, it cannot be in the codomain of the environment
+     either. This implies that it is safe to look up a type in the environment. *)
+  assert (not (Atom.Set.mem a env.tyvars));
+  { env with tyvars = Atom.Set.add a env.tyvars }
+
+(* -------------------------------------------------------------------------- *)
+
+(* Destructors. *)
+
+let unfold ty =
+  assert (wf_typ ty);
+  match ty with
+  | TyMu (a, body) ->
+      (* No shadowing within [ty] implies [a # ba(body)]. *)
+      assert (not (Atom.Set.mem a (ba_typ body)));
+      (* The free names of [ty] are free in [body] too.
+         Strong well-formedness for [body] yields [fa(body) # ba(body)].
+         Therefore, we have [fa(ty) # ba(body)]. *)
+      assert (Atom.Set.disjoint (fa_typ ty) (ba_typ body));
+      (* By the above, the bound names of [body] are disjoint with the
+         domain and codomain of the substitution [ty/a]. *)
+      subst_typ_typ1 ty a body
+  | _ ->
+      assert false
+
+exception NotAnArrow of nominal_typ
+
+let rec as_arrow ty : nominal_typ * nominal_typ =
+  match ty with
+  | TyArrow (ty1, ty2) ->
+      ty1, ty2
+  | TyMu _ ->
+      as_arrow (unfold ty)
+  | _ ->
+      raise (NotAnArrow ty)
+
+exception NotAProduct of nominal_typ
+
+let rec as_product ty : nominal_typ * nominal_typ =
+  match ty with
+  | TyProduct (ty1, ty2) ->
+      ty1, ty2
+  | TyMu _ ->
+      as_product (unfold ty)
+  | _ ->
+      raise (NotAProduct ty)
+
+exception NotAForall of nominal_typ
+
+let rec as_forall ty : tyvar * nominal_typ =
+  match ty with
+  | TyForall (a, ty) ->
+      a, ty
+  | TyMu _ ->
+      as_forall (unfold ty)
+  | _ ->
+      raise (NotAForall ty)
+
+(* -------------------------------------------------------------------------- *)
+
+(* An equality test. *)
+
+(* TEMPORARY should unfold recursive types on the fly *)
+
+exception TypeMismatch of nominal_typ * nominal_typ
+
+let (--) ty1 ty2 =
+  if not (equiv_typ ty1 ty2) then
+    raise (TypeMismatch (ty1, ty2))
+
+(* -------------------------------------------------------------------------- *)
+
+(* The type-checker. *)
+
+let rec typeof env (t : nominal_term) : nominal_typ =
+  match t with
+  | TeVar x ->
+      lookup env x
+  | TeAbs (x, ty1, t) ->
+      let ty2 = typeof (extend_with_tevar env x ty1) t in
+      TyArrow (ty1, ty2)
+  | TeApp (t, u) ->
+      let ty1, ty2 = as_arrow (typeof env t) in
+      typeof env u -- ty1;
+      ty2
+  | TeLet (x, t, u) ->
+      let env = extend_with_tevar env x (typeof env t) in
+      typeof env u
+  | TeTyAbs (a, t) ->
+      TyForall (a, typeof (extend_with_tyvar env a) t)
+  | TeTyApp (t, ty2) ->
+      let a, ty1 = as_forall (typeof env t) in
+      (* We need ba(ty1) # [ty2/a] for this substitution to be safe. *)
+      (* We have ba(ty1) # a because the type a.ty1 is well-formed. Weak uniqueness,
+         also known as no-shadowing, suffices. *)
+      assert (not (Atom.Set.mem a (ba_typ ty1))); (* TEMPORARY problem: ba is too strong *)
+      (* We have ba(ty1) # fa(ty2) because fa(ty2) is a subset of dom(env), that is,
+         env.tyvars, and typeof has the postcondition ba(\result) # env.tyvars. *)
+      subst_typ_typ1 ty2 a ty1
+  | TePair (t1, t2) ->
+      TyProduct (typeof env t1, typeof env t2)
+  | TeProj (i, t) ->
+      assert (i = 1 || i = 2);
+      let ty1, ty2 = as_product (typeof env t) in
+      if i = 1 then ty1 else ty2
+
+let typeof =
+  typeof empty

demos/system-F-type/Main.ml

-module T = F
+module T = FTypeChecker