User Tools

Site Tools


hofl_type_inference

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

hofl_type_inference [2015/10/08 15:20] (current)
Line 1: Line 1:
 +====== Type inference for a functional language ======
  
 +Implement the type inference algorithm presented in the given lecture.
 +
 +
 +===== Syntax of expressions and types =====
 +
 +<code ocaml>
 +type ide = Ide of string;;
 +
 +type exp =
 +    N of int
 +  | Val of ide
 +  | Add of exp * exp
 +  | Sub of exp * exp
 +  | Mul of exp * exp
 +  | Div of exp * exp
 +  | True
 +  | False
 +  | Eq of exp * exp
 +  | Leq of exp * exp
 +  | Not of exp
 +  | And of exp * exp
 +  | Or of exp * exp
 +  | If of exp * exp * exp
 +  | Let of ide * exp * exp
 +  | Letrec of ide * exp * exp
 +  | Fun of ide * exp
 +  | Apply of exp * exp
 +;;
 +</​code>​
 +
 +<code ocaml>
 +type etype = 
 +    TBool 
 +  | TInt 
 +  | TVar of string ​
 +  | TFun of etype * etype;;
 +</​code>​
 +
 +===== Type constraints =====
 +
 +The first phase of type inference consists in constructing a set of type constraints.
 +This is the goal of the function ''​tconstraints''​. The first argument is the expression
 +to be analysed. The second argument is a type environment,​ with type ''​(ide * etype) list''​.
 +The result is a value of type ''​etype * (etype * etype) list'',​ where the 
 +first item is the type of the expression, and the second item is the list of constraints.
 +
 +<code ocaml>
 +let rec tconstraints e tr = match e with
 +  N n -> (TInt,[])
 +| Val x ->  (applyenv tr x,[])
 +| Add (e1,e2)
 +| Sub (e1,e2)
 +| Mul (e1,e2)
 +| Div (e1,e2) ->
 +    let (t1,c1) = tconstraints e1 tr in
 +    let (t2,c2) = tconstraints e2 tr in
 +    let c = [(t1,TInt); (t2,TInt)] in
 +    (TInt, c @ c1 @ c2)
 +| True
 +| False -> (TBool,[])
 +| Eq (e1,e2)
 +| Leq (e1,e2) ->
 +    let (t1,c1) = tconstraints e1 tr in
 +    let (t2,c2) = tconstraints e2 tr in
 +    let c = [(t1,TInt); (t2,TInt)] in
 +    (TBool, c @ c1 @ c2)
 +| Not e1 ->
 +    let (t1,c1) = tconstraints e1 tr in
 +    let c = [(t1,​TBool)] in
 +    (TBool, c @ c1)
 +| And (e1,e2)
 +| Or (e1,e2) ->
 +    let (t1,c1) = tconstraints e1 tr in
 +    let (t2,c2) = tconstraints e2 tr in
 +    let c = [(t1,​TBool);​ (t2,TBool)] in
 +    (TBool, c @ c1 @ c2)
 +| If(e0,​e1,​e2) ->
 +    let (t0,c0) = tconstraints e0 tr in
 +    let (t1,c1) = tconstraints e1 tr in
 +    let (t2,c2) = tconstraints e2 tr in
 +    let c = [(t0,​TBool);​ (t1,t2)] in
 +    (t1, c @ c0 @ c1 @ c2)
 +| Let (x,e1,e2) ->
 +    let (t1,c1) = tconstraints e1 tr in
 +    let (t2,c2) = tconstraints e2 (bind tr x t1) in
 +    (t2, c1 @ c2)
 +| Letrec (x,e1,e2) ->
 +    let tx = gentide() in
 +    let (t1,c1) = tconstraints e1 (bind tr x tx) in
 +    let (t2,c2) = tconstraints e2 (bind tr x tx) in
 +    let c = [(tx,t1)] in
 +    (t2, c @ c1 @ c2)
 +| Fun (x,e1) ->
 +    let tx = gentide() in
 +    let (t1,c1) = tconstraints e1 (bind tr x tx) in
 +    (TFun (tx,t1), c1)
 +| Apply (e1,e2) ->
 +    let tx = gentide() in
 +    let (t1,c1) = tconstraints e1 tr in
 +    let (t2,c2) = tconstraints e2 tr in
 +    let c = [(t1,​TFun(t2,​tx))] in
 +    (tx, c @ c1 @ c2)
 +;;
 +</​code>​
 +
 +<code ocaml>
 +val tconstraints : exp -> (ide * etype) list -> etype * (etype * etype) list = <fun>
 +</​code>​
 +
 +The function gentide given below genereates a fresh type identifier.
 +
 +<code ocaml>
 +let nextsym = ref (-1);;
 +let gentide = fun () -> nextsym := !nextsym + 1; TVar ("?​T"​ ^ string_of_int (!nextsym));;​
 +</​code>​
 + 
 +
 +===== Unification =====
 +
 +The second phase provides for finding a solution to the set of constraints ​
 +constructed in the first phase. This is done by the ''​unify''​ function.
 +The first argument is the list of constraints. ​
 +The result, of type ''​(etype * etype) list'',​ is a list of substitution from
 +type variables to types.
 +
 +<code ocaml>
 +val unify : (etype * etype) list -> (etype * etype) list = <fun>
 +</​code>​
 +
 +Some auxiliary functions are helpful. ​
 +  * ''​applysubst1''​ substitutes a type for a type identifier in a type.
 +  * ''​applysubst''​ substitutes a type for a type identifier in a list of constraints.
 +  * ''​occurs''​ tells wheter a type identifier occurs in a type.
 +
 +<code ocaml>
 +val applysubst1 : etype -> string -> etype -> etype = <fun>
 +val applysubst : (etype * etype) list -> string -> etype -> (etype * etype) list = <fun>
 +val occurs : string -> etype -> bool = <fun>
 +</​code>​
 +
 +<code ocaml>
 +let rec applysubst1 t0 x t = match t0 with
 +    TInt -> TInt
 +  | TBool -> TBool
 +  | TVar y -> if y=x then t else TVar y
 +  | TFun (t1,t2) -> TFun (applysubst1 t1 x t, applysubst1 t2 x t)
 +;;
 +
 +let rec applysubst l x t = match l with
 +    [] -> []
 +  | (t1,​t2)::​l'​ -> (applysubst1 t1 x t, applysubst1 t2 x t)::​(applysubst l' x t)
 +;;
 +
 +let rec occurs x t = match t with
 +  TInt
 +| TBool -> false
 +| TVar y -> x=y
 +| TFun (t1,t2) -> (occurs x t1) || (occurs x t2)
 +;;
 +
 +let rec unify  l = match l with
 +  [] -> []
 +| (TInt,​TInt)::​l'​ -> unify l'
 +| (TBool,​TBool)::​l'​ -> unify l'
 +| (TVar x, t)::l' ->
 +    if occurs x t then failwith "​Occurs check"
 +    else (TVar x,​t)::​(unify (applysubst l' x t))
 +| (t, TVar x)::l' ->
 +    if occurs x t then failwith "​Occurs check"
 +    else (TVar x,​t)::​(unify (applysubst l' x t))
 +| (TFun(t1,​t2),​TFun(t1',​t2'​))::​l'​ ->
 +    unify ((t1,​t1'​) :: (t2,​t2'​) :: l')
 +| _ -> failwith "​Unsolvable constraints"​
 +;;
 +</​code>​
 +
 +Finally, the function ''​type_inference''​ combines the two phases above to infer
 +a type for an expression, or return an error if the expression is not typable.
 +
 +<code ocaml>
 +let type_inference e =
 +  let rec resolve t s = (match s with
 +    [] -> t
 +  | (TVar x, t'​)::​s'​ -> resolve (applysubst1 t x t') s'
 +  | _ -> failwith ("​Ill-formed substitution"​)) in
 +  let (t,c) = tconstraints e emptyenv in
 +  resolve t (unify c)
 +;;
 +</​code>​
 +
 +<code ocaml>
 +val type_inference : exp -> etype = <fun>
 +</​code>​
 +
 +===== Examples =====
 +
 +
 +<code ocaml>
 +let e0 = Let(Ide "​succ",​
 +      ​Fun(Ide "​x",​ Add(Val(Ide "​x"​),​ N 1)),
 +      ​Apply(Val(Ide "​succ"​),​N 8));;
 +
 +let (t0,c0) = tconstraints e0 emptyenv;;
 +# val t0 : etype = TVar "?​T8"​
 +# val c0 : (etype * etype) list =
 +  [(TVar "?​T7",​ TInt); (TInt, TInt);
 +   (TFun (TVar "?​T7",​ TInt), TFun (TInt, TVar "?​T8"​))]
 +
 +unify c0;;
 +# - : (etype * etype) list = [(TVar "?​T7",​ TInt); (TVar "?​T8",​ TInt)]
 +
 +type_inference e0;;
 +# - : etype = TInt
 +</​code>​
 +
 +
 +<code ocaml>
 +let e1 = Letrec(Ide "​fact",​
 + Fun(Ide "​x", ​
 +     If(Eq(Val(Ide "​x"​),​N 0),
 +        N 1, 
 +        ​Mul(Val(Ide "​x"​),​
 +    ​Apply(Val(Ide "​fact"​),​Sub(Val(Ide "​x"​),​ N 1))))),
 +        ​Apply(Val(Ide "​fact"​),​N 5));;
 +
 +type_inference e1;;
 +# - : etype = TInt
 +</​code>​
 +
 +
 +<code ocaml>
 +let mul2 = Let(Ide "​mul", ​
 + Fun(Ide "​x",​ Fun (Ide "​y",​ Mul(Val (Ide "​x"​),​ Val (Ide "​y"​)))),​
 + Fun(Ide "​x",​ Apply(Apply (Val (Ide "​mul"​),​ N 2), Val(Ide "​x"​))))
 +;;
 +
 +type_inference mul2;;
 +# - : etype = TFun (TInt, TInt)
 +</​code>​
 +
 +
 +<code ocaml>
 +let double = Fun(Ide "​f", ​
 + Fun (Ide "​x",​ Apply(Val(Ide "​f"​),​Apply(Val(Ide "​f"​),​Val(Ide "​x"​)))))
 +;;
 +
 +type_inference double;;
 +# - : etype = TFun (TFun (TVar "?​T21",​ TVar "?​T21"​),​ TFun (TVar "?​T21",​ TVar "?​T21"​))
 +</​code>​
 +
 +<code ocaml>
 +let doubleboolnat = 
 +    Let(Ide "​double",​
 + Fun(Ide "​f", ​
 +     Fun (Ide "​x",​ Apply(Val(Ide "​f"​),​Apply(Val(Ide "​f"​),​Val(Ide "​x"​))))),​
 + Let(Ide "​a",​ Apply(Apply(Val(Ide "​double"​),​Fun(Ide "​x",​ Apply(succ,​Apply(succ,​Val(Ide "​x"​))))),​N 2),
 +     Let(Ide "​b",​ Apply(Apply(Val(Ide "​double"​),​ Fun(Ide "​x",​ Val(Ide "​x"​))),​ True), ​
 + N 2)))
 +;;
 +
 +type_inference doubleboolnat;;​
 +# Exception: Failure "​Unsolvable constraints"​.
 +</​code>​
hofl_type_inference.txt ยท Last modified: 2015/10/08 15:20 (external edit)