Script started on Thu Jun 7 10:58:10 2007 feral-prairie-dog:~/bydate/2007/06/07 sundresh$ clear;ocaml  Objective Caml version 3.08.4 # ^[[B    #use "tc.ml";; type expr = IntConst of int | BoolConst of bool type type_expr = Int | Bool # IntConst 7;; - : expr = IntConst 7 # Bool;; - : type_expr = Bool # #use "tc.ml";; type expr = IntConst of int | BoolConst of bool type type_expr = Int | Bool val type_of : 'a -> expr -> type_expr = # type_of [] (IntConst 7);; - : type_expr = Int # $ #use "tc.ml";; type var_name = string type expr = IntConst of int | BoolConst of bool | Var of var_name type type_expr = Int | Bool type type_env = (string * type_expr) list exception TypeError File "tc.ml", line 14, characters 41-47: Unbound value lookup # #use "tc.ml";; type var_name = string type expr = IntConst of int | BoolConst of bool | Var of var_name type type_expr = Int | Bool type type_env = (string * type_expr) list exception TypeError val lookup : ('a * 'b) list -> 'a -> 'b = val type_of : (var_name * type_expr) list -> expr -> type_expr = # type_of ( [] (Var "x"] );; Exception: TypeError. # type_of [" ("x y", Int), ("x", Bool)] (Var "x");; # type_of [("y", Int), ("x", Bool)] (Var "x");; This expression has type (string * type_expr) * (string * type_expr) but is here used with type var_name * type_expr Type string * type_expr is not compatible with type var_name = string # type_of [("y", Int); ("x", Bool)] (Var "x");; - : type_expr = Bool # #use "tc.ml";; type var_name = string type expr = IntConst of int | BoolConst of bool | Var of var_name | Add of (expr * expr) type type_expr = Int | Bool type type_env = (string * type_expr) list exception TypeError val lookup : ('a * 'b) list -> 'a -> 'b = val type_of : (var_name * type_expr) list -> expr -> type_expr = # ;  ;; # ;; Syntax error # type_of [] (Add (IntConst 1) , Int     IntConst 2222222222222222222222                     ));; - : type_expr = Int # type_of [] (Add (IntConst                (Var "x", Int)] (Add (                     "x", i Int)] (Add (Var "x", Add (IntConst 1, A IntConst 3)));; - : type_expr = Int # #use "tc.ml";; type var_name = string type expr = IntConst of int | BoolConst of bool | Var of var_name | Add of (expr * expr) | Equals of (expr * expr) type type_expr = Int | Bool type type_env = (string * type_expr) list exception TypeError val lookup : ('a * 'b) list -> 'a -> 'b = val type_of : (var_name * type_expr) list -> expr -> type_expr = # ;; # ;; Syntax error # type_of [] (e Euq  quals (BoolConst true, BoolConst false));; - : type_expr = Bool # type_of [] (Equals (IntConst 7, BoolConst false));; Exception: TypeError. # #use "tc.ml";; File "tc.ml", line 11, characters 0-4: Syntax error # #use "tc.ml";; type var_name = string type expr = IntConst of int | BoolConst of bool | Var of var_name | Add of (expr * expr) | Equals of (expr * expr) | Apply of (expr * expr) type type_expr = Int | Bool | Fun of (type_expr * type_expr) type type_env = (string * type_expr) list exception TypeError val lookup : ('a * 'b) list -> 'a -> 'b = File "tc.ml", line 28, characters 25-39: Warning: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: (Bool|Int) val type_of : (var_name * type_expr) list -> expr -> type_expr = # #use "tc.ml";; File "tc.ml", line 29, characters 21-24: Syntax error # #use "tc.ml";; type var_name = string type expr = IntConst of int | BoolConst of bool | Var of var_name | Add of (expr * expr) | Equals of (expr * expr) | Apply of (expr * expr) type type_expr = Int | Bool | Fun of (type_expr * type_expr) type type_env = (string * type_expr) list exception TypeError val lookup : ('a * 'b) list -> 'a -> 'b = val type_of : (var_name * type_expr) list -> expr -> type_expr = # ;; # ;; Syntax error # #use "tc.ml";; type var_name = string type type_expr = Int | Bool | Fun of (type_expr * type_expr) type expr = IntConst of int | BoolConst of bool | Var of var_name | Add of (expr * expr) | Equals of (expr * expr) | Apply of (expr * expr) | Lambda of (var_name * type_expr * expr) type type_env = (string * type_expr) list exception TypeError val lookup : ('a * 'b) list -> 'a -> 'b = File "tc.ml", line 36, characters 3-20: This pattern matches values of type expr but is here used to match values of type type_expr # #use "tc.ml";; type var_name = string type type_expr = Int | Bool | Fun of (type_expr * type_expr) type expr = IntConst of int | BoolConst of bool | Var of var_name | Add of (expr * expr) | Equals of (expr * expr) | Apply of (expr * expr) | Lambda of (var_name * type_expr * expr) type type_env = (string * type_expr) list exception TypeError val lookup : ('a * 'b) list -> 'a -> 'b = val type_of : (var_name * type_expr) list -> expr -> type_expr = # ;; # ;; Syntax error # type_of [] (Apply (Lm ambda ("x", Int, "x  Var "x"), IntConst 7));; - : type_expr = Int # type_of [] (Apply (Lambda ("x", Int, Var "x"), BoolConst 7)  true));; Exception: TypeError. # #use "tc.ml";; type var_name = string type type_expr = Int | Bool | Fun of (type_expr * type_expr) type expr = IntConst of int | BoolConst of bool | Var of var_name | Add of (expr * expr) | Equals of (expr * expr) | Apply of (expr * expr) | Lambda of (var_name * type_expr * expr) | LetRec of (var_name * type_expr * expr * expr) type type_env = (string * type_expr) list exception TypeError val lookup : ('a * 'b) list -> 'a -> 'b = val type_of : (var_name * type_expr) list -> expr -> type_expr = # ;  ;; # ;; Syntax error # type_of [] (LetRec ("x", Int, IntConst 7, Var "x"));; - : type_expr = Int # #use "t poly.M ml";; File "poly.ml", line 6, characters 31-32: Syntax error # #use "poly.ml";; File "poly.ml", line 6, characters 31-32: Syntax error # # use   u u  use "poly.ml";; type var_name = string type type_var = string type type_expr = Int | Bool | Fun of (type_expr * type_expr) | TV of type_var type type_schema = TypeSchema of (type_var list * type_expr) type expr = IntConst of int | BoolConst of bool | Var of var_name | Add of (expr * expr) | Equals of (expr * expr) | Apply of (expr * expr) | Lambda of (var_name * type_expr * expr) | LetRec of (var_name * type_expr * expr * expr) type type_env = (string * type_schema) list exception TypeError val fv : type_expr -> type_var list = val lookup : ('a * 'b) list -> 'a -> 'b = File "poly.ml", line 48, characters 62-69: This expression has type var_name * type_expr but is here used with type var_name * type_schema # #use "poly.ml";; type var_name = string type type_var = string type type_expr = Int | Bool | Fun of (type_expr * type_expr) | TV of type_var type type_schema = TypeSchema of (type_var list * type_expr) type expr = IntConst of int | BoolConst of bool | Var of var_name | Add of (expr * expr) | Equals of (expr * expr) | Apply of (expr * expr) | Lambda of (var_name * type_expr * expr) | LetRec of (var_name * type_expr * expr * expr) type type_env = (string * type_schema) list exception TypeError val fv : type_expr -> type_var list = val lookup : ('a * 'b) list -> 'a -> 'b = File "poly.ml", line 30, characters 1-940: Warning: this pattern-matching is not exhaustive. Here is an example of a value that is not matched: LetRec _ val type_of : (var_name * type_schema) list -> expr -> type_schema = # #use "poly.ml";; type var_name = string type type_var = string type type_expr = Int | Bool | Fun of (type_expr * type_expr) | TV of type_var type type_schema = TypeSchema of (type_var list * type_expr) type expr = IntConst of int | BoolConst of bool | Var of var_name | Add of (expr * expr) | Equals of (expr * expr) | Apply of (expr * expr) | Lambda of (var_name * type_expr * expr) | LetRec of (var_name * type_expr * expr * expr) type type_env = (string * type_schema) list exception TypeError val fv : type_expr -> type_var list = val lookup : ('a * 'b) list -> 'a -> 'b = val type_of : (var_name * type_schema) list -> expr -> type_schema = # type_of [] (Fun   Lambda ("x", "a", Var 'a  "a"));; # type_of [] (Lambda ("x", "a", Var "a"));; This expression has type var_name * string * expr but is here used with type var_name * type_expr * expr # type_fo  of [] (Lambda ("x", TV ' "a", Var 'a"   "a"));; Exception: TypeError. # typeof []   "x"     (x "x", TV "    TypeSchema ([], TV "a"))] Var     (Var "a"                                                type_of [] (Lambda ("x", TV "a", Var "a"));;      x"));; - : type_schema = TypeSchema (["a"], Fun (TV "a", TV "a")) # type_of [] (Lambda ("x", TV "a",         (Fun (TV "A a", TV  TV "b")), Var     Var "x"));; - : type_schema = TypeSchema (["a"; "b"], Fun (Fun (TV "a", TV "b"), Fun (TV "a", TV "b"))) # typeo _of [] (Lambda ("x"  , Fun     ( Fun (TV "a", TV "b"), Lambda ("y", TV 'a"   "a", Apply(Var "x", Var "y"))));; Exception: TypeError. # Lambda       ty   type_of [] "x  ("x", Fun (TV "a", TV "b"))] Lambda ("y", TV "a", Apply(Var "x", Var "y"))                                   ;; ;; ))));; ;; ^CInterrupted. # type_of [("x", Fun (TV "a", TV "b"))] (Lambda ("y", TV "a", A Apply (Var "x", Var "y")));; # type_of [("x", Fun (TV "a", TV "b"))] (Lambda ("y", TV "a", Apply (Var "x", Var "y")));; This expression has type var_name * type_expr but is here used with type var_name * type_schema # type_of [("x", TypeSchema ([],    ], Fun (TV "a", TV "b")))] (Lambda ("y", TV "a", Apply (Var "x", Var "y")));; Exception: TypeError. # ^D feral-prairie-dog:~/bydate/2007/06/07 sundresh$ exit Script done on Thu Jun 7 12:46:40 2007