(* 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 = *) 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 = *) 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";;

Public snippets