8. Type Inference¶

8.1. Why Static Type Inference?¶

let val x = ref 0
in
  x := !x + 1;
  println (!x)
end

Fig 8.1 test8.sml

let val x = ref 0
in
  x := x + 1;
  println (x)
end

Fig 8.2 test13.sml

exception E of int;
fun g(y) = raise E(y);
fun f(x) =
    let
      exception E of real;
      fun z(y)= raise E(y);
    in
      x(3.0);
      z(3)
    end;
f(g);

Fig. 8.3 Exception Program

stdIn:216.8-216.12 Error: operator and operand don't agree [literal]
  operator domain: real
  operand:         int
  in expression:
    z 3

let val x = 6
in
  println x
  println "Done"
end

Fig 8.4 A bad function call

8.2. Type Inference Rules¶

RuleName

$\frac{Premise_1,~~Premise_2,~~...,~~Premise_n}{Conclusion}$

8.3. Using Prolog¶

letdec(
      bindval(idpat('x'),apply(id('ref'),int('0'))),
  [apply(id(':='),tuple([id('x'),
   apply(id('+'),tuple([apply(id('!'),id('x')),
         int('1')]))])),
   apply(id('println'),apply(id('!'),id('x')))
  ]).

Fig. 8.5 test8.sml prolog AST

finalStatus(typeerror) :- print('The program failed to pass the typechecker.'), nl, !.
finalStatus(_) :- print('The program passed the typechecker.'), nl, !.

warning([],_) :- !.
warning(_,fn(_,_)) :- !.
warning([_|_],_) :-
  print('Warning: type vars not instantiated in result type initialized to dummy types!'),
  nl, nl, !.

errorOut(error(E)) :-
     nl, nl, print('Error: Typechecking failed. Message was : '), nl,
     print(E), nl, nl, halt(0).
errorOut(typeerror(E)) :-
     nl, nl, print('Error: Typechecking failed due to type error. Message was : '), nl,
     print(E), nl, nl, halt(0).
errorOut(E) :-
     nl, nl, print('Error: Typechecking failed for unknown reason : '), nl,
     print(E), nl, nl, halt(0).
run :- print('Typechecking is commencing...'), nl,
       readAST(AST), print('Here is the AST'), nl, print(AST), nl, nl, nl,
       catch(typecheckProgram(AST,Type),E,errorOut(E)),
       nl, nl, print('val it : '), printType(Type,TypeVars), nl, nl,
       warning(TypeVars,Type), finalStatus(Type).
runNonInteractive :- run, halt(0).

Fig. 8.6 The Type Checker run Predicate

datatype
  exp = int of string
      | ch of string
      | str of string
      | bool of string
      | id of string
      | listcon of exp list
      | tuplecon of exp list
      | apply of exp * exp
      | expsequence of exp list
      | letdec of dec * (exp list)
      | handlexp of exp * match list
      | ifthen of exp * exp * exp
      | whiledo of exp * exp
      | func of string * match list
and
  match = match of pat * exp
and
  pat = intpat of string
      | chpat of string
      | strpat of string
      | boolpat of string
      | idpat of string
      | wildcardpat
      | infixpat of string * pat * pat
      | tuplepat of pat list
      | listpat of pat list
      | aspat of string * pat
and
  dec = bindval of pat * exp
      | bindvalrec of pat * exp
      | funmatch of string * match list
      | funmatches of (string * match list) list

Fig. 8.7 AST Description

type = bool
     | int
     | str
     | exn
     | tuple of type list
     | listOf of type
     | fn of type * type
     | ref of type
     | typevar of string
     | typeerror

Fig. 8.8 Small Types

8.4. The Type Environment¶

typecheckProgram(Expression,Type) :-
    typecheckExp([('Exception',fn(typevar(a),exn)),
                  ('raise',fn(exn,typevar(a))),
                  ('andalso',fn(tuple([bool,bool]),bool)),
                  ('orelse',fn(tuple([bool,bool]),bool)),
                  (':=',fn(tuple([ref(typevar(a)),typevar(a)]),tuple([]))),
                  ('!',fn(ref(typevar(a)),typevar(a))),
                  ('ref',fn(typevar(a),ref(typevar(a)))),
                  ('::',fn(tuple([typevar(a),listOf(typevar(a))]),listOf(typevar(a)))),
                  ('>', fn(tuple([typevar(a),typevar(a)]),bool)),
                  ('<', fn(tuple([typevar(a),typevar(a)]),bool)),
                  (@,fn(tuple([listOf(typevar(a)),listOf(typevar(a))]),listOf(typevar(a)))),
                  ('Int.fromString',fn(str,int)),
                  ('input',fn(str,str)),
                  ('explode',fn(str,listOf(str))),
                  ('implode',fn(listOf(str),str)),
                  ('println',fn(typevar(a),tuple([]))),
                  ('print',fn(typevar(a),tuple([]))),
                  ('cprint',fn(typevar(a),cprint)),
                  ('type',fn(typevar(a), str)),
                  (+,fn(tuple([int,int]),int)),
                  (-,fn(tuple([int,int]),int)),
                  (*,fn(tuple([int,int]),int)),
                  ('div',fn(tuple([int,int]),int))],
           Expression,Type).

Fig. 8.9 The Prolog Type Environment

8.5. Integers, Strings, and Boolean Constants¶

typecheckExp(_,int(_),int).
typecheckExp(_,bool(_),bool).
typecheckExp(_,str(_),str).

Fig. 8.10 Constant Types

BoolCon

$\frac{}{\varepsilon\vdash bool(v) : bool}$

IntCon

$\frac{}{\varepsilon\vdash int(v) : int}$

StringCon

$\frac{}{\varepsilon\vdash str(v) : str}$

8.5.1. Example 8.1¶

Typechecking is commencing...
Here is the AST
int(5)
val it : int
The program passed the typechecker.

8.6. List and Tuple Constants¶

$[ 6, 5, 4 ] & : int~~list \\ ( "hi", true, 6) & : str * bool * int$

typecheckExp(Env,listcon(L),listOf(T)) :- typecheckList(Env,L,T).
typecheckExp(Env,tuple(L),tuple(T)) :- typecheckTuple(Env,L,T).

listOf(int)
tuple([str,bool,int])

ListCon

$& \forall i~~1\leq i \leq n, n \geq 0\\ & \frac{\varepsilon\vdash e_i:\alpha}{\varepsilon\vdash [e_1,e_2,...,e_n] : \alpha~~list}$

TupleCon

$& \forall ~~1\leq i \leq n, n \geq 0\\ & \frac{\varepsilon\vdash e_i:\alpha_i}{\varepsilon\vdash (e_1,e_2,...,e_n) : \times_{i=1}^n \alpha_i}$

8.6.1. Example 8.2¶

Typechecking is commencing...
Here is the AST
listcon([int(1),int(2),int(3),int(4)])
val it : int list
The program passed the typechecker.

8.7. Identifiers¶

exists(Env,Name) :-
    member((Name,_),Env), !.
find(Env,Name,Type) :-
    member((Name,Type),Env), !.
find(Env,Name,Type) :-
    writeMsg(['Failed to find ',
    Name,' with type ',Type,
    ' in environment : ']), print(Env), nl,
    throw(typeerror('unbound identifier')).
typecheckExp(Env,id(Name),Type) :-
    find(Env,Name,Type).

Fig. 8.11 Environment Lookup Predicates

Identifier

$\frac{}{\varepsilon[id \mapsto \alpha]\vdash id : \alpha}$

8.7.1. Example 8.3¶

Typechecking is commencing...
Here is the AST
id(println)
val it : 'a -> unit
The program passed the typechecker.

8.8. Function Application¶

println 6

FunApp

$\frac{\varepsilon\vdash e_1 : \alpha\rightarrow\beta, ~~ \alpha'\rightarrow\beta':inst(\alpha\rightarrow\beta),~~ \varepsilon\vdash e_2 : \alpha_{e2}, ~~ \alpha' : inst(\alpha_{e2})} {\varepsilon\vdash e_1 e_2 : \beta'}$

instanceOfList(Env,[],[],Env).
instanceOfList(Env,[H|T],[G|S],NewEnv) :-
    instanceOf(Env,H,G,Env1), instanceOfList(Env1,T,S,NewEnv).
instanceOf(Env,A,A,Env) :- var(A), !.
instanceOf(Env,A,A,Env) :- simple(A), !.
instanceOf(Env,fn(A,B), fn(AInst,BInst),Env2) :-
    instanceOf(Env,A,AInst,Env1), instanceOf(Env1,B,BInst,Env2), !.
instanceOf(Env,listOf(A),listOf(B),NewEnv) :- instanceOf(Env,A,B,NewEnv), !.
instanceOf(Env,ref(A),ref(B),NewEnv) :- instanceOf(Env,A,B,NewEnv), !.
instanceOf(Env,tuple(L),tuple(M),NewEnv) :- instanceOfList(Env,L,M,NewEnv), !.
instanceOf(Env,typevar(A),B,Env) :- exists(Env,A), find(Env,A,B), !.
instanceOf(Env,typevar(A),B,[(A,B)|Env]) :- !.
instanceOf(_,A,B,_) :-
    print('Type Error: Type '), printType(B,_),
    print(' is not an instance of '), printType(A,_), nl,
    throw(typeerror('type mismatch')), !.
inst(X,Y) :- instanceOf([],X,Y,_).

Fig. 8.12 The Instantiation Operator

typecheckExp(Env,apply(Exp1,Exp2),ITT) :-
        typecheckExp(Env,Exp1,fn(FT,TT)), typecheckExp(Env,Exp2,Exp2Type),
        inst(Exp2Type,Exp2TypeInst), catch(inst(fn(FT,TT), fn(Exp2TypeInst,ITT)),_,
        printApplicationErrorMessage(Exp1,fn(FT,TT),Exp2,Exp2Type,ITT)), !.

Fig. 8.13 Function Application Type Inference

8.8.1. Instantiation¶

8.8.2. Example 8.4¶

$\frac{\varepsilon\vdash println : \alpha\rightarrow unit,~~~ int\rightarrow unit:inst(\alpha\rightarrow unit),~~~\varepsilon\vdash 6 : int} { \varepsilon\vdash println~6 : unit}$

8.9. Let Expressions¶

8.9.1. Example 8.5¶

$\varepsilon_1 & = [x\mapsto\alpha\rightarrow\beta,~y\mapsto int,~z\mapsto\alpha\times\beta]\\ \varepsilon_2 & = [u\mapsto\alpha\times\beta\rightarrow\beta,~y\mapsto\ bool]\\ \varepsilon_2\oplus\varepsilon_1 &= [u\mapsto\alpha\times\beta\rightarrow\beta,~y\mapsto\ bool]\oplus[x\mapsto\alpha\rightarrow\beta,~y\mapsto int,~z\mapsto\alpha\times\beta]\\ & = [u\mapsto\alpha\times\beta\rightarrow\beta,~y\mapsto\ bool,x\mapsto\alpha\rightarrow\beta,~y\mapsto int, ~z\mapsto\alpha\times\beta]$

$\varepsilon\vdash dec \Rightarrow \varepsilon_{dec}$

Let

$\frac{\varepsilon\vdash dec\Rightarrow\varepsilon_{dec},~~\varepsilon_{dec}\oplus\varepsilon\vdash e_{sequence}:\beta}{\varepsilon\vdash let~dec~in~e_{sequence}~end:\beta}$

ValDec

$\frac{pat:\alpha\Rightarrow\varepsilon_{pat},~~\varepsilon\vdash e:close(\alpha)}{\varepsilon\vdash val~pat=e\Rightarrow\varepsilon_{pat}}$

ValRecDec

$\frac{[id:\alpha]\oplus\varepsilon\vdash e:\alpha}{\varepsilon\vdash val~rec~id=e\Rightarrow[ id:close(\alpha)]}$

FunDecs

$& \forall i~1 \leq i \leq n, \forall j~1 < j \leq n,~~n \geq 1,\\ & \frac{[id_1\mapsto\alpha_1\rightarrow\beta_1~\{,~id_j\mapsto\alpha_j\rightarrow\beta_j\}]\oplus\varepsilon\vdash id_i~matches_i:\alpha_i\rightarrow\beta_i}{\varepsilon\vdash f\!un~id_1~matches_1~\{and~id_j~matches_j\}\Rightarrow[id_1\mapsto close(\alpha_1\rightarrow\beta_1)~\{,~id_j\mapsto close(\alpha_j\rightarrow\beta_j)\}]}$

8.10. Patterns¶

IntPat

$\frac{}{integer\_constant:int \Rightarrow [~]}$

BoolPat

$& \frac{}{true:bool \Rightarrow [~]} \\ & \frac{}{false:bool \Rightarrow [~]}$

StrPat

$\frac{}{string\_constant:str \Rightarrow [~]}$

NilPat

$\frac{}{nil:\alpha~list\Rightarrow[~]}$

ConsPat

$\frac{pat_1:\alpha\Rightarrow \varepsilon_{pat_1},~~pat_2:\alpha~list\Rightarrow \varepsilon_{pat_2}} {pat_1::pat_2 : \alpha~list\Rightarrow \varepsilon_{pat_1}+\varepsilon_{pat_2}}$

TuplePat

$& \forall i~1 \leq i \leq n, n \geq 0\\ & \frac{pat_i : \alpha_i \Rightarrow \varepsilon_{pat_i}} {(pat_1,pat_2,...,pat_n): \times_{i=1}^{n}\alpha_i\Rightarrow \sum^{n}_{i=1}\varepsilon_{pat_i}}$

ListPat

$& \forall i~1 \leq i \leq n, n \geq 0\\ & \frac{pat_i : \alpha \Rightarrow \varepsilon_{pat_i}} {[pat_1,pat_2,...,pat_n]: \alpha~list\Rightarrow \sum^{n}_{i=1}\varepsilon_{pat_i}}$

let
  val (x,y)::L = [(1,2),(3,4)]
in
  println x
end

Fig. 8.14 Pattern Matching

IdPat

$\frac{}{id:\alpha\Rightarrow[id\mapsto\alpha]}$

8.10.1. Example 8.6¶

letdec(
  bindval(infixpat(::,tuplepat([idpat(x),idpat(y)]),idpat(L)),
    listcon([tuple([int(1),int(2)]),tuple([int(3),int(4)])])),
  [apply(id(println),id(x))])
val (x,y)::L : (int * int) list
val it : unit
The program passed the typechecker.

$\dfrac{ (2) \varepsilon\vdash val~(x,y)::L = [(1,2),(3,4)]\Rightarrow\varepsilon_{dec} ~~~ (3) \varepsilon_{dec}\oplus\varepsilon\vdash println~x : unit }{ (1)\varepsilon\vdash let~val~(x,y)::L = [(1,2),(3,4)]~in~println~x~end : unit }(Let) \varepsilon_{dec} =[x\mapsto int, y\mapsto int, L\mapsto int * int~list]$

To prove (2):

$\dfrac{ (4) (x,y)::L : int\times int~list\Rightarrow\varepsilon_{dec} ~~~ (5) \varepsilon\vdash [(1,2),(3,4)] : int\times int~list }{ (2) \varepsilon\vdash val~(x,y)::L = [(1,2),(3,4)]\Rightarrow\varepsilon_{dec} }(ValDec)$

To prove (4):

$\dfrac{ (6) (x,y) : int \times int \Rightarrow [x\mapsto int, y\mapsto int] ~~~ (7) L : int\times int~list \Rightarrow[L\mapsto int\times int~list] }{ (4) (x,y)::L : int\times int~list\Rightarrow\varepsilon_{dec} }(ConsPat)$

To prove (6):

$\dfrac{ (8) x : int \Rightarrow[x\mapsto int] ~~~ (9) y : int \Rightarrow[y\mapsto int] }{ (6) (x,y) : int \times int \Rightarrow [x\mapsto int, y\mapsto int] }(TuplePat)$

Premises (7), (8), and (9) are true by virtue of the IdPat inference rule. Considering (5):

$\dfrac { (10)\varepsilon\vdash (1,2):int\times int ~~~ (11)\varepsilon\vdash (3,4):int\times int }{ (5) \varepsilon\vdash [(1,2),(3,4)] : int\times int~list }(ListCon)$

Considering (10) and a similar argument for (11):

$\dfrac{ (12)\varepsilon\vdash 1:int ~~~ (13)\varepsilon\vdash 2:int }{ (10)\varepsilon\vdash (1,2):int\times int }(TupleCon)$

Both (12) and (13) are true by the IntCon rule. A similar argument holds for (11). The proof nears completion by proving (3):

$\dfrac{ (14) \varepsilon_{dec}\oplus\varepsilon\vdash println : \alpha\rightarrow unit ~~~ int\rightarrow unit : inst(\alpha\rightarrow unit) ~~~ (15) \varepsilon_{dec}\oplus\varepsilon\vdash x : int } { (3) \varepsilon_{dec}\oplus\varepsilon\vdash println~x : unit }(FunApp)$

Both (14) and (15) are true by the Identifier rule concluding the proof of the type correctness of this program.

let val x = 5
    val y = 6
in
  println (x + y)
end

Fig. 8.15 test10.sml

Practice 8.1

Prove that the program given in figure 8.13 is correctly typed. The abstract syntax for this program is provided here.

letdec(bindval(idpat('x'),int('5')),
 [letdec(bindval(idpat('y'),int('6')),
     [apply(id('println'),apply(id('+'),tuple([id('x'),id('y')])))])
 ]).

You can check your answer(s) here.

Practice 8.2

Minimally, what must the type environment contain to correctly type check the program in figure 8.15.

You can check your answer(s) here.

8.11. Matches¶

let fun f(0,y) = y
      | f(x,y) = g(x,x*y)
    and g(x,y) = f(x-1,y)
in
  println (f(10,5))
end

Fig. 8.16 test11.sml

Matches

$& \forall i~1 \leq i \leq n, \forall j~1 < j \leq n,~n \geq 1\\ & \frac{\varepsilon\vdash id:\alpha\rightarrow\beta,~~pat_i:\alpha\Rightarrow \varepsilon_{pat_i},~~\varepsilon_{pat_i}\oplus\varepsilon\vdash e_i:\beta} {\varepsilon\vdash id~pat_1=e_1\{|~id~pat_j=e_j\}:\alpha\rightarrow\beta}$

or

$& \forall i~1 \leq i \leq n, \forall j~1 < j \leq n,~n \geq 1\\ & \frac{\varepsilon\vdash id:\alpha\rightarrow\beta,~~pat_i:\alpha\Rightarrow \varepsilon_{pat_i},~~\varepsilon_{pat_i}\oplus\varepsilon\vdash e_i:\beta} {\varepsilon\vdash id~pat_1=>e_1\{|~pat_j=>e_j\}:\alpha\rightarrow\beta}$

8.11.1. Example 8.7¶

letdec(
  funmatches(
    [funmatch(f,
       [match(tuplepat([intpat(0),idpat(y)]),id(y)),
        match(tuplepat([idpat(x),idpat(y)]),apply(id(g),
           tuple([id(x),apply(id(*),tuple([id(x),id(y)]))])))]),
     funmatch(g,
       [match(tuplepat([idpat(x),idpat(y)]),
          apply(id(f),tuple([apply(id(-),tuple([id(x),int(1)])),id(y)])))])]),
  [apply(id(println),apply(id(f),tuple([int(10),int(5)])))])

8.12. Anonymous Functions¶

(fn x => x+1)

Fig. 8.17 Anonymous Function

AnonFun: $\frac{[id\mapsto\alpha\rightarrow\beta]\oplus\varepsilon\vdash id~matches:\alpha\rightarrow\beta} {\varepsilon\vdash fn~id~matches:\alpha\rightarrow\beta}$

8.12.1. Example 8.8¶

func(anon@0,[match(idpat(x),apply(id(+),tuple([id(x),int(1)])))])

$\frac{[anon@0\mapsto int\rightarrow int]\oplus\varepsilon\vdash anon@0~x => x+1:int\rightarrow int} {\varepsilon\vdash fn~anon@0~x => x+1 :int\rightarrow int}$

Practice 8.3

Provide a complete proof that the program in figure 8.17 is correctly typed.

You can check your answer(s) here.

8.13. Sequential Execution¶

Sequence

$& \forall i~1 \leq i \leq n, \forall j~1 < j \leq n,~n \geq 1\\ & \frac{\varepsilon\vdash e_i : \alpha_i} {\varepsilon\vdash e_1 \{ ; e_j\} : \alpha_n}$

8.14. If-Then and While-Do¶

IfThen

$\frac{\varepsilon\vdash e_1:bool,~~\varepsilon\vdash e_2:\alpha,~~~\varepsilon\vdash e_3:\alpha}{\varepsilon\vdash i\!f~e_1~then~e_2~else~e_3 : \alpha}$

WhileDo

$\frac{\varepsilon\vdash e_1:bool,~~\varepsilon\vdash e_2:\alpha}{\varepsilon\vdash while~e_1~do~e_2 : \alpha}$

typecheckExp(Env,ifthen(Exp1,Exp2,Exp3), RT) :-
    typecheckExp(Env,Exp1,bool), typecheckExp(Env,Exp2,RT), typecheckExp(Env,Exp3,RT), !.
typecheckExp(Env,ifthen(Exp1,Exp2,Exp3), _) :-
    typecheckExp(Env,Exp1,bool), typecheckExp(Env,Exp2,ThenType), typecheckExp(Env,Exp3,ElseType),
    print('Error: Result types of then and else expressions must match.'), nl,
    print('Then Expression type is: '), printType(ThenType,_), nl,
    print('Else Expression type is: '), printType(ElseType,_), nl,
    throw(typeerror('result type mismatch in if-then-else expression')).
typecheckExp(Env,ifthen(Exp1,_,_), _) :-
    typecheckExp(Env,Exp1,Exp1Type), Exp1Type \= bool,
    print('Error: Condition of if then expression must have bool type.'), nl,
    print('Condition Expression type was: '), printType(Exp1Type,_), nl,
    throw(typeerror('type not bool in if-then-else expression condition')).

Fig. 8.18 If-Then Prolog Code

8.15. Exception Handling¶

Handler

$\frac{\varepsilon\vdash e:\alpha, ~~ [handle@\mapsto~exn\rightarrow\alpha]\oplus\varepsilon\vdash handle@~matches : exn\rightarrow\alpha} {\varepsilon\vdash e~handle~matches : \alpha}$

8.16. Chapter Summary¶

8.17. Review Questions¶

What appears above and below the line in a type inference rule?
Why don’t infix operators appear in the abstract syntax of programs handled by the type checker?
What does typevar represent in figure 8.6?
What does typeerror represent in figure 8.6?
What does the type of the list [(“hello”,1,true)] look like as a Prolog term?
What is the type environment?
Give an example of the use of the overlay operator.
What pattern(s) are used in this let expression?
```
let val (x,y,z) = ("hello",1,true) in println x end
```
What is the pattern as a Prolog term?
Give an example where the Sequence rule might be used to infer a type.
Give a short example of where the Handler rule might be used to infer a type.

8.18. Exercises¶

The following program does not compile correctly or typecheck correctly using the mlcomp compiler and type inference system. However, it is a valid Standard ML program. Modify both the mlcomp compiler and type checker to correctly compile and infer its type. This program is included in the compiler project as test20.sml.

let val [(x,y,z)] = [(l+s+s2{h}ellop{,}1,true)] in println x end