hm.ml
(*
hm.ml
A naive implementation of Hindley-Milner type inference
for a mini ML
AMP, June 2007
*)
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 * <<vid*vid>>expr (* | x1::x2 -> e3 *)
| Fn of <<vid>>expr (* fn x => e *)
| App of expr * expr (* e1 e2 *)
| Let of expr * <<vid>>expr;; (* let x = e1 in e2 end *)
type tysc = (* type schemes *)
<<tyvar list>>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, <<aa>>t) -> (x, <<aa>>(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 <<aa>>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 s321 = compose s3 s21 in
let (s4, t4) = pt (apply_env s321 env) e3 in
let s5 = mgu (apply s4 t3) t4 in
(compose s5 (compose s4 s321), apply s5 t4)
| 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, <<x1,x2>>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(<<x>>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, <<x>>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, <<aa>>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(<<x>>(Vid x));;
pts [] id;;
let snd = Fn(<<x>>(Fn(<<y>>(Vid x))));;
pts [] snd;;
let e1 = Let(snd, <<f>>(App(Vid f, Vid f)));;
pts [] e1;;
let e2 = App(Fn(<<f>>(App(Vid f, Vid f))), snd);;
pts [] e2;;
This document was generated using caml2html