(* hm.ml A naive implementation of Hindley-Milner type inference for a mini ML AMP, July 2003 *) type t;; (* some type *) type tyvar = t name;; (* type variables, a *) type ty = (* types, t *) Tyvar of tyvar (* a *) | Bool (* bool *) | List of ty (* ty list *) | Fun of ty * ty;; (* t1 -> t2 *) type t;; (* another type *) type vid = t name;; (* value identifiers, x *) type expr = (* expressions, e *) Vid of vid (* x *) | True (* true *) | False (* false *) | If of expr * expr * expr (* if e1 then e2 else e3 *) | Nil (* nil *) | Cons of expr * expr (* e1 :: e2 *) | Case of (* case e1 of nil -> e2 *) expr * expr * <>expr (* | x1::x2 -> e3 *) | Fn of <>expr (* fn x => e *) | App of expr * expr (* e1 e2 *) | Let of expr * <>expr;; (* let x = e1 in e2 end *) type tysc = (* type schemes *) <>ty;; (* All a1,...,an.ty *) type tyenv = (* typing environments *) (vid * tysc)list;; type sub = (* type substitutions, s *) (tyvar * ty)list;; (* Substitute a type for a type variable in a type *) let subst (t : ty) (a : tyvar) : ty -> ty = let rec sub (t' : ty) : ty = match t' with Tyvar b -> if a = b then t else Tyvar b | Bool -> Bool | List t1 -> List(sub t1) | Fun(t1,t2) -> Fun(sub t1, sub t2) in sub;; (* Apply a type substitution to a type *) let rec apply (s : sub) (t : ty) : ty = match t with (Tyvar a) as t' -> (try List.assoc a s with Not_found -> t') | Bool -> Bool | List t1 -> List(apply s t1) | Fun(t1, t2) -> Fun(apply s t1, apply s t2);; (* Compose type substitutions, right-to-left, i.e. should have apply (compose s1 s2) t = apply s1 (apply s2 t) *) let compose (s1 : sub) (s2 : sub) : sub = (* if s2 associates t with a, apply s1 to t *) (List.map (function (a, t) -> (a, apply s1 t)) s2) @ (* if a is not in the domain of s2, but is in the domain of s1, then use s1 *) (List.filter (function (a, t) -> not(List.mem_assoc a s2)) s1);; (* Apply a type substitution to a typing environment *) let apply_env (s : sub) (env : tyenv) : tyenv = List.map (function (x, <>t) -> (x, <>(apply s t))) env;; exception Fail;; (* Calculate the most general unifier of two types, raising Fail if there is not one *) let mgu : ty -> ty -> sub = let rec unify (prob : (ty * ty)list) (s :sub) : sub = match prob with [] -> s | (Tyvar a, t) :: rest -> if (a freshfor t) then let rest' = List.map (function (t1,t2) -> (subst t a t1, subst t a t2)) rest in unify rest' ((a, t) :: s) else if t = Tyvar a then unify rest s else raise Fail | (t, Tyvar a) :: rest -> if (a freshfor t) then let rest' = List.map (function (t1,t2) -> (subst t a t1, subst t a t2)) rest in unify rest' ((a, t) :: s) else raise Fail | (Bool, Bool) :: rest -> unify rest s | (List t1, List t2) :: rest -> unify ((t1, t2) :: rest) s | (Fun(t1, t1'), Fun(t2, t2')) :: rest -> unify ((t1, t2) :: (t1', t2') :: rest) s | _ -> raise Fail in function t1 -> function t2 -> unify [(t1, t2)] [];; (* Calculate the list of type variables occurring in a type, without repeats *) let rec tv (t : ty) : tyvar list = match t with Tyvar a -> [a] | Bool -> [] | List t -> tv t | Fun(t1, t2) -> let aa = tv t1 in aa @ (List.filter (function a -> (a freshfor aa)) (tv t2));; exception Not_Typeable;; (* Calculate the principal type scheme for an expression in a given typing environment *) let pts (env: tyenv) (e : expr) : tysc = let rec pt (env : tyenv) (e : expr) : (sub * ty) = match e with Vid x -> (try let <>t = (List.assoc x env) in ([], t) with Not_found -> raise Not_Typeable) | True -> ([], Bool) | False -> ([], Bool) | If(e1, e2, e3) -> let (s1, t1) = pt env e1 in let s2 = mgu t1 Bool in let s21 = compose s2 s1 in let (s3, t3) = pt (apply_env s21 env) e2 in let s4 = mgu (apply (compose s3 s2) t1) t3 in (compose s4 (compose s3 s21), apply s4 t3) | Nil -> let (a : tyvar) = fresh in ([], List(Tyvar a)) | Cons(e1, e2) -> let (s1, t1) = pt env e1 in let (s2, t2) = pt (apply_env s1 env) e2 in let s3 = mgu (List(apply s2 t1)) t2 in (compose s3 (compose s2 s1), apply s3 t2) | Case(e1, e2, <>e3) -> let (s1, t1) = pt env e1 in let env1 = apply_env s1 env in let (a : tyvar) = fresh in let s2 = mgu t1 (List(Tyvar a)) in let (s3, t3) = pt (apply_env s2 env1) e2 in let s32 = compose s3 s2 in let (s4, t4) = pt ((x1, <<[]>>(apply s32 (Tyvar a))) :: (x2, <<[]>>(apply s32 t1)) :: (apply_env s32 env1)) e3 in let s5 = mgu t4 (apply s4 t3) in (compose s5 (compose s4 (compose s32 s1)), apply s5 t4) | Fn(<>e1) -> let (a : tyvar) = fresh in let (s1, t1) = pt ((x, <<[]>>(Tyvar a)) :: env) e1 in (s1, Fun(apply s1 (Tyvar a), t1)) | App(e1, e2) -> let (s1, t1) = pt env e1 in let (s2, t2) = pt (apply_env s1 env) e2 in let (a : tyvar) = fresh in let s3 = mgu (apply s2 t1) (Fun(t2, Tyvar a)) in (compose s3 (compose s2 s1), apply s3 (Tyvar a)) | Let(e1, <>e2) -> let (s1, t1) = pt env e1 in let env1 = apply_env s1 env in let aa = List.filter (function a -> (a freshfor env1)) (tv t1) in let (s2, t2) = pt ((x, <>t1) :: env1) e2 in (compose s2 s1, t2) in let (s, t) = pt env e in << List.filter (function a -> (a freshfor (apply_env s env))) (tv t) >>t;; (******************************************************************** Examples ********************************************************************) let (x : vid), (y: vid), (f :vid) = fresh, fresh, fresh;; let id = Fn(<>(Vid x));; pts [] id;; let snd = Fn(<>(Fn(<>(Vid x))));; pts [] snd;; let e1 = Let(snd, <>(App(Vid f, Vid f)));; pts [] e1;; let e2 = App(Fn(<>(App(Vid f, Vid f))), snd);; pts [] e2;;