The Damas-Milner’s type system 2
r ® e1 _ Intero r ® e2 _ Intero
-----------------------------------------------------
r ® Sum(e1,e2) _ Intero
- ok for type checking
- for type inference, judgments have to be understood as going from expressions to pairs (environment,type), i.e.
- we need to compute an environment making the judgment valid
- the algorithm is not straightforward
r[x ¬ t1] ® e _ t2
-----------------------------------------------------
r ® Fun(x,e) _ Mkarrow(t1, t2)
r[f ¬ Mkarrow(t1, t2)] ® Fun(x,e) _ Mkarrow(t1, t2)
---------------------------------------------------------------------
r ® Rec(f,x,e) _ Mkarrow(t1, t2)
- even worse: no hints on how to choose t1 and on how to solve the recursive definition