Add Cornell inference code and lecture material

references/Infer/Makefile

+# Infer makefile
+#
+# targets are:
+#
+# all -- rebuild the project (default)
+# clean -- remove all objects and executables
+
+SOURCES = ast.ml Parser/parser.mli Parser/parser.ml Parser/lexer.ml unify.ml infer.ml repl.ml
+
+.PHONY: all
+all: Parser/parser.mli Parser/parser.ml Parser/lexer.ml infer.exe
+
+.PHONY: clean
+clean:
+	rm -f infer.exe
+	rm -f Parser/parser.ml Parser/parser.mli Parser/lexer.ml
+	for X in . Parser; do \
+	  for Y in cmo cmi output; do \
+        rm -f $$X/*.$$Y; \
+      done; \
+    done
+
+infer.exe: $(SOURCES)
+	ocamlc -o infer.exe -g -I Parser str.cma $(SOURCES)
+
+Parser/parser.mli Parser/parser.ml: Parser/parser.mly ast.ml
+	ocamlyacc -v Parser/parser.mly
+
+Parser/lexer.ml: Parser/lexer.mll Parser/parser.ml
+	ocamllex Parser/lexer.mll

references/Infer/Parser/lexer.mll

+{
+open Parser
+exception Eof
+}
+
+let alphabetic = ['a'-'z' 'A'-'Z']
+let alphanumeric = ['a'-'z' 'A'-'Z' '0'-'9']*
+rule token = parse
+  | [' ' '\t']  { token lexbuf } (* skip blanks *)
+  | ['\n'] { EOL }
+  | "fun"  { FUN }
+  | alphabetic alphanumeric as id { VAR id }
+  | '('    { LPAREN }
+  | ')'    { RPAREN }
+  | "->"   { IMP }
+  | eof    { EOL }

references/Infer/Parser/parser.ml

+type token =
+  | VAR of (string)
+  | LPAREN
+  | RPAREN
+  | IMP
+  | EOL
+  | FUN
+  | APP
+
+open Parsing;;
+# 2 "Parser/parser.mly"
+open Ast
+# 14 "Parser/parser.ml"
+let yytransl_const = [|
+  258 (* LPAREN *);
+  259 (* RPAREN *);
+  260 (* IMP *);
+  261 (* EOL *);
+  262 (* FUN *);
+  263 (* APP *);
+    0|]
+
+let yytransl_block = [|
+  257 (* VAR *);
+    0|]
+
+let yylhs = "\255\255\
+\001\000\002\000\002\000\002\000\002\000\000\000"
+
+let yylen = "\002\000\
+\002\000\001\000\004\000\003\000\002\000\002\000"
+
+let yydefred = "\000\000\
+\000\000\000\000\002\000\000\000\000\000\006\000\000\000\000\000\
+\000\000\001\000\005\000\004\000\000\000\000\000"
+
+let yydgoto = "\002\000\
+\006\000\011\000"
+
+let yysindex = "\003\000\
+\013\255\000\000\000\000\013\255\006\255\000\000\000\255\007\255\
+\012\255\000\000\000\000\000\000\013\255\020\255"
+
+let yyrindex = "\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\015\255"
+
+let yygindex = "\000\000\
+\000\000\255\255"
+
+let yytablesize = 22
+let yytable = "\007\000\
+\003\000\004\000\008\000\001\000\010\000\005\000\009\000\003\000\
+\004\000\012\000\000\000\014\000\005\000\003\000\004\000\013\000\
+\000\000\003\000\005\000\003\000\003\000\004\000"
+
+let yycheck = "\001\000\
+\001\001\002\001\004\000\001\000\005\001\006\001\001\001\001\001\
+\002\001\003\001\255\255\013\000\006\001\001\001\002\001\004\001\
+\255\255\003\001\006\001\005\001\001\001\002\001"
+
+let yynames_const = "\
+  LPAREN\000\
+  RPAREN\000\
+  IMP\000\
+  EOL\000\
+  FUN\000\
+  APP\000\
+  "
+
+let yynames_block = "\
+  VAR\000\
+  "
+
+let yyact = [|
+  (fun _ -> failwith "parser")
+; (fun __caml_parser_env ->
+    let _1 = (Parsing.peek_val __caml_parser_env 1 : 'expr) in
+    Obj.repr(
+# 22 "Parser/parser.mly"
+                       ( _1 )
+# 83 "Parser/parser.ml"
+               : Ast.expr))
+; (fun __caml_parser_env ->
+    let _1 = (Parsing.peek_val __caml_parser_env 0 : string) in
+    Obj.repr(
+# 26 "Parser/parser.mly"
+                        ( Var _1 )
+# 90 "Parser/parser.ml"
+               : 'expr))
+; (fun __caml_parser_env ->
+    let _2 = (Parsing.peek_val __caml_parser_env 2 : string) in
+    let _4 = (Parsing.peek_val __caml_parser_env 0 : 'expr) in
+    Obj.repr(
+# 27 "Parser/parser.mly"
+                               ( Fun (_2, _4) )
+# 98 "Parser/parser.ml"
+               : 'expr))
+; (fun __caml_parser_env ->
+    let _2 = (Parsing.peek_val __caml_parser_env 1 : 'expr) in
+    Obj.repr(
+# 28 "Parser/parser.mly"
+                        ( _2 )
+# 105 "Parser/parser.ml"
+               : 'expr))
+; (fun __caml_parser_env ->
+    let _1 = (Parsing.peek_val __caml_parser_env 1 : 'expr) in
+    let _2 = (Parsing.peek_val __caml_parser_env 0 : 'expr) in
+    Obj.repr(
+# 29 "Parser/parser.mly"
+                        ( App (_1, _2) )
+# 113 "Parser/parser.ml"
+               : 'expr))
+(* Entry main *)
+; (fun __caml_parser_env -> raise (Parsing.YYexit (Parsing.peek_val __caml_parser_env 0)))
+|]
+let yytables =
+  { Parsing.actions=yyact;
+    Parsing.transl_const=yytransl_const;
+    Parsing.transl_block=yytransl_block;
+    Parsing.lhs=yylhs;
+    Parsing.len=yylen;
+    Parsing.defred=yydefred;
+    Parsing.dgoto=yydgoto;
+    Parsing.sindex=yysindex;
+    Parsing.rindex=yyrindex;
+    Parsing.gindex=yygindex;
+    Parsing.tablesize=yytablesize;
+    Parsing.table=yytable;
+    Parsing.check=yycheck;
+    Parsing.error_function=parse_error;
+    Parsing.names_const=yynames_const;
+    Parsing.names_block=yynames_block }
+let main (lexfun : Lexing.lexbuf -> token) (lexbuf : Lexing.lexbuf) =
+   (Parsing.yyparse yytables 1 lexfun lexbuf : Ast.expr)

references/Infer/Parser/parser.mli

+type token =
+  | VAR of (string)
+  | LPAREN
+  | RPAREN
+  | IMP
+  | EOL
+  | FUN
+  | APP
+
+val main :
+  (Lexing.lexbuf  -> token) -> Lexing.lexbuf -> Ast.expr

references/Infer/Parser/parser.mly

+%{
+open Ast
+%}
+
+%token <string> VAR
+%token LPAREN RPAREN
+%token IMP
+%token EOL
+%token FUN
+%token APP
+
+%nonassoc FUN
+%nonassoc VAR LPAREN
+%left APP
+
+%start main  /* entry point */
+%type <Ast.expr> main
+
+%%
+
+main:
+  expr EOL             { $1 }
+;
+
+expr:
+  | VAR                 { Var $1 }
+  | FUN VAR IMP expr %prec FUN { Fun ($2, $4) }
+  | LPAREN expr RPAREN  { $2 }
+  | expr expr %prec APP { App ($1, $2) }
+;
+

references/Infer/ast.ml

+(*********************************************************************
+ * Abstract syntax trees for lambda expressions and type expressions *
+ *********************************************************************)
+
+type id = string
+
+(* lambda expressions *)
+type expr =
+  | Fun of id * expr
+  | App of expr * expr
+  | Var of id
+
+(* type expressions *)
+type typ =
+  | TVar of id
+  | Arrow of typ * typ
+
+(* annotated expressions *)
+type aexpr =
+  | AFun of id * aexpr * typ
+  | AApp of aexpr * aexpr * typ
+  | AVar of id * typ
+
+let rec to_string (e : expr) : string =
+  match e with
+    | Var x -> x
+    | Fun (x, e) -> Printf.sprintf "fun %s -> %s" x (to_string e)
+    | App (Fun _ as e1, e2) -> Printf.sprintf "%s %s" (protect e1) (protect e2)
+    | App (e1, e2) -> Printf.sprintf "%s %s" (to_string e1) (protect e2)
+
+and protect (e : expr) : string =
+  match e with
+    | Var x -> x
+    | _ -> Printf.sprintf "(%s)" (to_string e)
+
+let rec type_to_string (e : typ) : string =
+  match e with
+    | TVar x -> "'" ^ x
+    | Arrow (Arrow (u, v) as s, t) -> Printf.sprintf "(%s) -> %s" (type_to_string s) (type_to_string t)
+    | Arrow (s, t) -> Printf.sprintf "%s -> %s" (type_to_string s) (type_to_string t)
+
+let rec aexpr_to_string (e : aexpr) : string =
+  match e with
+    | AVar (x, a) -> Printf.sprintf "(%s:%s)" x (type_to_string a)
+    | AApp (e1, e2, a) -> Printf.sprintf "((%s %s):%s)" (aexpr_to_string e1) (aexpr_to_string e2) (type_to_string a)
+    | AFun (x, e, a) -> Printf.sprintf "((Fun %s -> %s):%s)" x (aexpr_to_string e) (type_to_string a)

references/Infer/infer.ml

+(******************************************
+ * Type inference for simple lambda terms *
+ ******************************************)
+
+open Ast
+
+let code = ref (Char.code 'a')
+
+let reset_type_vars() = code := Char.code 'a'
+
+let next_type_var() : typ =
+  let c = !code in
+  if c > Char.code 'z' then failwith "too many type variables";
+  incr code;
+  TVar (String.make 1 (Char.chr c))
+
+let type_of (ae : aexpr) : typ =
+  match ae with
+    AVar (_, a) -> a
+  | AFun (_, _, a) -> a
+  | AApp (_, _, a) -> a
+  
+(* annotate all subexpressions with types *)
+(* bv = stack of bound variables for which current expression is in scope *)
+(* fv = hashtable of known free variables *)
+let annotate (e : expr) : aexpr =
+  let (h : (id, typ) Hashtbl.t) = Hashtbl.create 16 in
+  let rec annotate' (e : expr) (bv : (id * typ) list) : aexpr =
+    match e with
+      Var x ->
+        (* bound variable? *)
+        (try let a = List.assoc x bv in AVar (x, a)
+        (* known free variable? *)
+        with Not_found -> try let a = Hashtbl.find h x in AVar (x, a)
+        (* unknown free variable *)
+        with Not_found -> let a = next_type_var() in Hashtbl.add h x a; AVar (x, a))
+    | Fun (x, e) ->
+        (* assign a new type to x *)
+        let a = next_type_var() in
+        let ae = annotate' e ((x, a) :: bv) in
+        AFun (x, ae, Arrow (a, type_of ae))
+    | App (e1, e2) ->
+        AApp (annotate' e1 bv, annotate' e2 bv, next_type_var())
+  in annotate' e []
+
+(* collect constraints for unification *)
+let rec collect (aexprs : aexpr list) (u : (typ * typ) list) : (typ * typ) list =
+  match aexprs with
+    [] -> u
+  | AVar (_, _) :: r -> collect r u
+  | AFun (_, ae, _) :: r -> collect (ae :: r) u
+  | AApp (ae1, ae2, a) :: r ->
+      let (f, b) = (type_of ae1, type_of ae2) in
+      collect (ae1 :: ae2 :: r) ((f, Arrow (b, a)) :: u)
+
+(* collect the constraints and perform unification *)
+let infer (e : expr) : typ =
+  reset_type_vars();
+  let ae = annotate e in
+  let cl = collect [ae] [] in
+  let s = Unify.unify cl in
+  Unify.apply s (type_of ae)

references/Infer/repl.ml

+(*****************************
+ * Main read-eval-print loop *
+ *****************************)
+
+let parse (s : string) : Ast.expr =
+  Parser.main Lexer.token (Lexing.from_string s)
+  
+let i = "fun x -> x"
+let s = "fun x -> fun y -> fun z -> x z (y z)"
+let k = "fun x -> fun y -> x"
+let o = "fun f -> fun g -> fun x -> f (g x)"
+let y = "fun f -> (fun x -> f x x) (fun y -> f y y)"
+  
+let rec repl () =
+  print_string "? ";
+  let input = read_line() in
+  if input = "" then () else
+  try
+    let e = parse input in
+    let t = Infer.infer e in
+    Printf.printf "%s : %s\n" (Ast.to_string e) (Ast.type_to_string t);
+    repl ()
+  with Failure msg -> print_endline msg; repl ()
+  | _ -> print_endline "Error"; repl ()
+  
+let _ = repl()

references/Infer/unify.ml

+(*****************************
+* Unification of type terms *
+*****************************)
+
+open Ast
+
+(* invariant for substitutions: no id on a lhs occurs in any term earlier  *)
+(* in the list                                                             *)
+type substitution = (id * typ) list
+
+(* check if a variable occurs in a term *)
+let rec occurs (x : id) (t : typ) : bool =
+  match t with
+  | TVar y -> x = y
+  | Arrow (u, v) -> occurs x u || occurs x v
+
+(* substitute term s for all occurrences of var x in term t *)
+let rec subst (s : typ) (x : id) (t : typ) : typ =
+  match t with
+  | TVar y -> if x = y then s else t
+  | Arrow (u, v) -> Arrow (subst s x u, subst s x v)
+
+(* apply a substitution to t right to left *)
+let apply (s : substitution) (t : typ) : typ =
+  List.fold_right (fun (x, e) -> subst e x) s t
+
+(* unify one pair *)
+let rec unify_one (s : typ) (t : typ) : substitution =
+  match (s, t) with
+  | (TVar x, TVar y) -> if x = y then [] else [(x, t)]
+  | (Arrow (x, y), Arrow (u, v)) -> unify [(x, u); (y, v)]
+  | ((TVar x, (Arrow (u, v) as z)) | ((Arrow (u, v) as z), TVar x)) ->
+      if occurs x z
+      then failwith "not unifiable: circularity"
+      else [(x, z)]
+
+(* unify a list of pairs *)
+and unify (s : (typ * typ) list) : substitution =
+  match s with
+  | [] -> []
+  | (x, y) :: t ->
+      let t2 = unify t in
+      let t1 = unify_one (apply t2 x) (apply t2 y) in
+      t1 @ t2
+