(*
Simple Hindley-Milner type checker for pure lambda-calculus with let
Explanation of the efficient generalization -- Remy algorithm
The sound and even more efficient generalization with levels computed
on demand,2 and the incremental occurs check and generalization.
*)
(* The language: lambda-calculus with let *)
type varname = string
type exp =
| Var of varname (* variable *)
| App of exp * exp (* application: e1 e2 *)
| Lam of varname * exp (* abstraction: fun x -> e *)
| Let of varname * exp * exp (* let x = e in e2 *)
;;
let rec show_exp = function
| Var v -> print_string v
| App (e1, e2) -> show_exp e1; print_string "("; show_exp e2; print_string ")"
| Lam (x, e) -> print_string "λ"; print_string x; print_string "."; show_exp e
| Let (x, e, b) -> print_string "let "; print_string x; print_string " = "; show_exp e; print_string " in "; show_exp b
;;
(* The types to infer *)
(* Types without quantified variables are simple types;
those containing quantified variables are type schemas.
A quantified variable is a TVar whose level is generic_level.
Since quantifiers are always on the outside in the HM system,
they are implied and not explicitly represented.
Unlike sound_eager.ml, all types, not only type variables,
have levels. Normally, the level of a composite type is
an upper bound on the levels of its components.
If a type belongs to a region n, all its subcomponents should be alive when
the region n is still alive.
However, levels are determined incrementally. Therefore,
Composite types have two levels: level_old is always
an upper bound for the levels of the components;
level_new is equal or less than level_old. If
level_new is less than level_old, the type is being promoted
to a higher region. The type needed to be traversed and
all of its components adjusted so their levels do not
exceed level_new. Generalization will perform such an
adjustment of levels for some types.
During type traversals, level_new may have the value
marked_level to signify that the type is being traversed.
Encountering a type at the marked_level during the traversals
means that we detect a cycle, created during unification
without the occurs check.
*)
type level = int
let generic_level = 100000000 (* as in OCaml typing/btype.ml *)
let marked_level = -1 (* for marking a node, to check*)
(* for cycles *)
type typ =
| TVar of tv ref
| TArrow of typ * typ * levels
and tv = Unbound of string * level | Link of typ
and levels = {mutable level_old : level; mutable level_new : level}
;;
let rec show_type: typ -> unit = function
| TVar r -> show_tvar (!r)
| TArrow (a, b, l) -> print_string "("; show_type a; print_string "->"; show_type b; print_string ")"
and show_tvar: tv -> unit = function
| Unbound (v, l) -> print_string v
| Link (v) -> show_type v
;;
(* Chase the links of bound variables, returning either
a free variable or a constructed type.
OCaml's typing/btype.ml has the same function with the same name.
Unlike OCaml, we do path compression.
*)
let rec repr : typ -> typ = function
| TVar ({contents = Link t} as tvr) ->
let t = repr t in
tvr := Link t; t
| t -> t
;;
(* get the level of a normalized type, which is not a bound TVar *)
let get_level : typ -> level = function
| TVar {contents = Unbound (_,l)} -> l
| TArrow (_,_,ls) -> ls.level_new
| _ -> assert false
;;
let gensym_counter = ref 0
let reset_gensym : unit -> unit =
fun () -> gensym_counter := 0
;;
let gensym : unit -> string = fun () ->
let n = !gensym_counter in
let () = incr gensym_counter in
if n < 26 then String.make 1 (Char.chr (Char.code 'a' + n))
else "t" ^ string_of_int n
;;
(* Determining the |let|-nesting level during the type-checking,
or just the _level_.
Each top-level expression to type-check is implicitly wrapped into a let.
So, the numbering starts with 1.
*)
let current_level = ref 1
let reset_level () = current_level := 1
let reset_type_variables () = (* name from OCaml's typing/typetext.ml *)
reset_gensym ();
reset_level ()
(* Increase level *)
let enter_level () =
incr current_level
(* Restore level *)
let leave_level () =
decr current_level
(* Make a fresh type variable and an arrow type *)
let newvar : unit -> typ =
fun () -> TVar (ref (Unbound (gensym (),!current_level)))
;;
let new_arrow : typ -> typ -> typ = fun ty1 ty2 ->
TArrow(ty1,ty2,{level_new = !current_level; level_old = !current_level})
;;
(* Delayed occurs check. We do not do the occurs check when unifying
a free type variable. Therefore, we may construct a cyclic type.
The following function, executed only at the end of the type checking,
checks for no cycles in the type.
Incidentally, OCaml does allow cycles in the type: types are generally
(equi-)recursive in OCaml.
*)
let rec cycle_free : typ -> unit = function
| TVar {contents = Unbound _} -> ()
| TVar {contents = Link ty} -> cycle_free ty
| TArrow (_,_,ls) when ls.level_new = marked_level -> failwith "occurs check"
| TArrow (t1,t2,ls) ->
let level = ls.level_new in
ls.level_new <- marked_level;
cycle_free t1;
cycle_free t2;
ls.level_new <- level
;;
(* Main unification *)
(* Quantified variables are unexpected: they should've been instantiated *)
(* The occurs check is lazy; therefore, cycles could be created
accidentally. We have to watch for them.
*)
(*
Update the level of the type so that it does not exceed the
given level l.
Invariant: a level of a type can only decrease
(assigning the type generic_level is special, and does
not count as the `update')
The existing level of the type cannot be generic_level
(quantified variables must be specially instantiated) or
marked_level (in which case, we encounter a cycle).
If the type to update is composite and its new and old
levels were the same and the new level is updated to a
smaller level, the whole type is put into the
to_be_level_adjusted queue for later traversal and adjustment
of the levels of components.
This work queue to_be_level_adjusted is akin to the list
of assignments from the old generation to the new maintained by a
generational garbage collector (such as the one in OCaml).
The update_level itself takes constant time.
*)
let to_be_level_adjusted = ref []
let reset_level_adjustment ()
= to_be_level_adjusted := []
let update_level : level -> typ -> unit = fun l -> function
| TVar ({contents = Unbound (n,l')} as tvr) ->
assert (not (l' = generic_level));
if l < l' then
tvr := Unbound (n,l)
| TArrow (_,_,ls) as ty ->
assert (not (ls.level_new = generic_level));
if ls.level_new = marked_level then failwith "occurs check";
if l < ls.level_new then begin
if ls.level_new = ls.level_old then
to_be_level_adjusted := ty :: !to_be_level_adjusted;
ls.level_new <- l
end
| _ -> assert false
;;
(* Unifying a free variable tv with a type t takes constant time:
it merely links tv to t (setting the level of t to tv if tv's
level was smaller). Therefore, cycles may be created accidentally,
and the complete update of type levels may have to be done
at a later time.
Incidentally, another unification may need to traverse the type
with the pending level update. That unification will do the level
update along the way.
*)
let rec unify : typ -> typ -> unit = fun t1 t2 ->
if t1 == t2 then () (* t1 and t2 are physically the same *)
else match (repr t1,repr t2) with
| (TVar ({contents = Unbound (_,l1)} as tv1) as t1, (* unify two free vars *)
(TVar ({contents = Unbound (_,l2)} as tv2) as t2)) ->
(* bind the higher-level var *)
if l1 > l2 then tv1 := Link t2 else tv2 := Link t1
| (TVar ({contents = Unbound (_,l)} as tv),t')
| (t',TVar ({contents = Unbound (_,l)} as tv)) ->
update_level l t';
tv := Link t'
| (TArrow (tyl1,tyl2,ll), TArrow (tyr1,tyr2,lr)) ->
if ll.level_new = marked_level || lr.level_new = marked_level then
failwith "cycle: occurs check";
let min_level = min ll.level_new lr.level_new in
ll.level_new <- marked_level; lr.level_new <- marked_level;
unify_lev min_level tyl1 tyr1;
unify_lev min_level tyl2 tyr2;
ll.level_new <- min_level; lr.level_new <- min_level
(* everything else is the unification error *)
and unify_lev l ty1 ty2 =
let ty1 = repr ty1 in
update_level l ty1;
unify ty1 ty2
;;
(* The type environment *)
type env = (varname * typ) list
;;
(* Sound generalization: generalize (convert to quantified vars)
only those free TVars whose level is greater than the current.
These TVars belong to dead regions.
A quantified var is a TVar at the generic_level.
We traverse only those parts of the type that may contain
type variables at the level greater than the current.
If a type has the level of the current or smaller, all
of its components have the level not exceeding the current -- and
so that type does not have to be traversed.
After generalization, a constructed type receives the generic_level
if at least one of its components is quantified.
However, before generalization we must perform the pending level updates.
After all, a pending update may decrease the level of a type
variable (promote it to a wider region) and thus save the variable
from quantification.
We do not need to do all of the pending updates: only those that
deal with types whose level_old > current_level. If
level_old <= current_level, the type contains no generalizable type
variables anyway.
*)
let force_delayed_adjustments () =
let rec loop acc level ty =
match repr ty with
| TVar ({contents = Unbound (name,l)} as tvr) when l > level ->
tvr := Unbound (name,level); acc
| TArrow (_,_,ls) when ls.level_new = marked_level ->
failwith "occurs check"
| TArrow (_,_,ls) as ty ->
if ls.level_new > level then ls.level_new <- level;
adjust_one acc ty
| _ -> acc
(* only deals with composite types *)
and adjust_one acc = function
| TArrow (_, _, ls) as ty when ls.level_old <= !current_level ->
ty::acc (* update later *)
| TArrow (_, _, ls) when ls.level_old = ls.level_new ->
acc (* already updated *)
| TArrow (ty1, ty2, ls) ->
let level = ls.level_new in
ls.level_new <- marked_level;
let acc = loop acc level ty1 in
let acc = loop acc level ty2 in
ls.level_new <- level;
ls.level_old <- level;
acc
| _ -> assert false
in
to_be_level_adjusted :=
List.fold_left adjust_one [] !to_be_level_adjusted;
;;
let gen : typ -> unit = fun ty ->
force_delayed_adjustments ();
let rec loop ty =
match repr ty with
| TVar ({contents = Unbound (name,l)} as tvr)
when l > !current_level -> tvr := Unbound (name,generic_level)
| TArrow (ty1,ty2,ls) when ls.level_new > !current_level ->
let ty1 = repr ty1 and ty2 = repr ty2 in
loop ty1; loop ty2;
let l = max (get_level ty1) (get_level ty2) in
ls.level_old <- l; ls.level_new <- l (* set the exact level upper bound *)
| _ -> ()
in loop ty
;;
(* instantiation: replace schematic variables with fresh TVars.
Only the components at generic_level are traversed, since only
those may contain quantified type variables.
*)
let inst : typ -> typ =
let rec loop subst = function
| TVar {contents = Unbound (name,l)} when
l = generic_level ->
begin
try (List.assoc name subst, subst)
with Not_found ->
let tv = newvar () in
(tv, (name,tv)::subst)
end
| TVar {contents = Link ty} -> loop subst ty
| TArrow (ty1,ty2,ls) when ls.level_new = generic_level ->
let (ty1,subst) = loop subst ty1 in
let (ty2,subst) = loop subst ty2 in
(new_arrow ty1 ty2, subst)
| ty -> (ty, subst)
in fun ty -> fst (loop [] ty)
;;
(* Trivial type checker. Type checking errors are delivered
as exceptions
*)
let rec typeof : env -> exp -> typ = fun env -> function
| Var x -> inst (List.assoc x env)
| Lam (x,e) ->
let ty_x = newvar () in
let ty_e = typeof ((x,ty_x)::env) e in
new_arrow ty_x ty_e
| App (e1,e2) ->
let ty_fun = typeof env e1 in
let ty_arg = typeof env e2 in
let ty_res = newvar () in
unify ty_fun (new_arrow ty_arg ty_res);
ty_res
| Let (x,e,e2) ->
enter_level ();
let ty_e = typeof env e in
leave_level ();
gen ty_e;
typeof ((x,ty_e)::env) e2
;;
let id = Lam("x",Var"x");;
let c1 = Lam("x",Lam("y",App (Var"x",Var"y")));;
(* Type-check the top-level expression *)
let top_type_check : exp -> typ = fun exp ->
reset_type_variables ();
reset_level_adjustment ();
show_exp exp;
print_newline ();
let ty = typeof [] exp in
cycle_free ty;
show_type ty;
print_newline();
print_newline();
ty;
;;
let
TArrow (TVar {contents = Unbound ("a", 1)},
TVar {contents = Unbound ("a", 1)}, {level_old = 1; level_new = 1})
=
top_type_check id
;;
let
TArrow
(TVar
{contents =
Link
(TArrow (TVar {contents = Unbound ("b", 1)},
TVar {contents = Unbound ("c", 1)}, {level_old = 1; level_new = 1}))},
TArrow (TVar {contents = Unbound ("b", 1)},
TVar {contents = Unbound ("c", 1)}, {level_old = 1; level_new = 1}),
{level_old = 1; level_new = 1})
=
top_type_check c1
;;
let
TArrow
(TArrow (TVar {contents = Unbound ("d", 1)},
TVar {contents = Unbound ("e", 1)}, {level_old = 1; level_new = 1}),
TArrow (TVar {contents = Unbound ("d", 1)},
TVar {contents = Unbound ("e", 1)}, {level_old = 1; level_new = 1}),
{level_old = 1; level_new = 1})
=
top_type_check (Let ("x",c1,Var"x"));;
let
TArrow (TVar {contents = Unbound ("b", 1)},
TVar {contents = Unbound ("b", 1)}, {level_old = 1; level_new = 1})
=
top_type_check (Let ("y",Lam ("z",Var"z"), Var"y"));;
let
TArrow (TVar {contents = Unbound ("a", 1)},
TArrow (TVar {contents = Unbound ("c", 1)},
TVar {contents = Unbound ("c", 1)}, {level_old = 1; level_new = 1}),
{level_old = 1; level_new = 1})
=
top_type_check (Lam ("x", Let ("y",Lam ("z",Var"z"), Var"y")));;
let
TArrow (TVar {contents = Link (TVar {contents = Unbound ("c", 1)})},
TVar {contents = Link (TVar {contents = Unbound ("c", 1)})},
{level_old = 1; level_new = 1})
=
top_type_check (Lam ("x", Let ("y",Lam ("z",Var"z"),
App (Var"y",Var"x"))));;
try
top_type_check (Lam ("x",App (Var"x",Var"x")));
assert false;
with Failure e -> print_endline e
;;
try
top_type_check (Let ("x",Var"x",Var"x"));
assert false;
with Not_found -> print_endline "unbound var"
;;
(* id can be `self-applied', on the surface of it *)
let
TVar
{contents =
Link
(TArrow (TVar {contents = Unbound ("c", 1)},
TVar {contents = Unbound ("c", 1)}, {level_old = 1; level_new = 1}))}
=
top_type_check (Let ("id",id, App (Var"id",Var"id")));;
let
TArrow (TVar {contents = Unbound ("i", 1)},
TVar {contents = Unbound ("i", 1)}, {level_old = 1; level_new = 1})
=
top_type_check (Let ("x",c1,
Let ("y",
Let ("z",App(Var"x",id), Var "z"),
Var"y")));;
(*
fun x -> fun y -> let x = x y in fun x -> y x;;
- : (('a -> 'b) -> 'c) -> ('a -> 'b) -> 'a -> 'b = <fun>
*)
let
TArrow
(TVar
{contents =
Link
(TArrow
(TVar
{contents =
Link
(TArrow (TVar {contents = Unbound ("d", 1)},
TVar {contents = Unbound ("e", 1)},
{level_old = 1; level_new = 1}))},
TVar {contents = Unbound ("c", 1)}, {level_old = 1; level_new = 1}))},
TArrow
(TVar
{contents =
Link
(TArrow (TVar {contents = Unbound ("d", 1)},
TVar {contents = Unbound ("e", 1)}, {level_old = 1; level_new = 1}))},
TArrow (TVar {contents = Unbound ("d", 1)},
TVar {contents = Unbound ("e", 1)}, {level_old = 1; level_new = 1}),
{level_old = 1; level_new = 1}),
{level_old = 1; level_new = 1})
=
top_type_check (Lam ("x", Lam("y",Let ("x",App (Var"x",Var"y"),
Lam ("x",App (Var"y",Var"x"))))));;
(* now sound generalization ! *)
let
TArrow (TVar {contents = Unbound ("a", 1)},
TVar {contents = Unbound ("a", 1)}, {level_old = 1; level_new = 1})
=
top_type_check (Lam ("x", Let ("y",Var"x", Var"y")));;
(* now sound generalization ! *)
let
TArrow (TVar {contents = Unbound ("a", 1)},
TArrow (TVar {contents = Unbound ("c", 1)},
TVar {contents = Unbound ("a", 1)}, {level_old = 1; level_new = 1}),
{level_old = 1; level_new = 1})
=
top_type_check (Lam ("x", Let ("y",Lam ("z",Var"x"), Var"y")));;
(* now sound generalization ! *)
let
TArrow
(TVar
{contents =
Link
(TArrow (TVar {contents = Unbound ("b", 1)},
TVar {contents = Unbound ("c", 1)}, {level_old = 1; level_new = 1}))},
TArrow (TVar {contents = Unbound ("b", 1)},
TVar {contents = Unbound ("c", 1)}, {level_old = 1; level_new = 1}),
{level_old = 1; level_new = 1})
=
top_type_check (Lam ("x", Let ("y",Lam ("z",App (Var"x",Var"z")), Var"y")));;
(* now sound generalization ! *)
let
TArrow
(TVar
{contents =
Link
(TArrow (TVar {contents = Unbound ("b", 1)},
TVar
{contents =
Link
(TArrow (TVar {contents = Unbound ("b", 1)},
TVar {contents = Unbound ("d", 1)},
{level_old = 1; level_new = 1}))},
{level_old = 1; level_new = 1}))},
TArrow (TVar {contents = Unbound ("b", 1)},
TVar {contents = Unbound ("d", 1)}, {level_old = 1; level_new = 1}),
{level_old = 1; level_new = 1})
=
top_type_check (Lam ("x", Lam("y",Let ("x",App (Var"x",Var"y"),
App (Var"x",Var"y")))));;
(* now sound generalization ! *)
try
top_type_check (Lam ("x",Let("y",Var"x", App (Var"y",Var"y"))));
assert false;
with Failure e -> print_endline e
;;
(* now sound generalization ! *)
(* fun x -> let y = let z = x (fun x -> x) in z in y;;
- : (('a -> 'a) -> 'b) -> 'b = <fun>
*)
let
TArrow
(TVar
{contents =
Link
(TArrow
(TArrow (TVar {contents = Unbound ("b", 1)},
TVar {contents = Unbound ("b", 1)}, {level_old = 1; level_new = 1}),
TVar {contents = Unbound ("c", 1)}, {level_old = 1; level_new = 1}))},
TVar {contents = Unbound ("c", 1)}, {level_old = 1; level_new = 1})
=
top_type_check (Lam ("x",
Let ("y",
Let ("z",App(Var"x",id), Var "z"),
Var"y")));;
print_endline "\nAll Done\n";;
