Type inference with unification

[Fatemeh]

Hi
I don't understand the "unification algorithm "and "Type inference
with unification" which are in lecture 10
For instance what these functions do
infer env (fun arg) =
(s1,T1) := infer env fun
(s2,T2) := infer (env s1) arg
b := freshVar env
s3 := unify (T1 s2) (T2 -> b)
return (s3 + s2 + s1, b s3)

infer env (\x -> body) =
b := freshVar env
(s,T) := infer (env, x : b) body
return (s, (b s) -> T)

Is there any body who can explain these parts for me?

Thanks
Fatemeh

[Aarne Ranta]

Hello Fatemeh,

These functions infer the type of an expression in an environment where the variables are given their most general polymorphic types. The return is a type and a substitution of types to type variables.

The book gives more details about this. And you will certainly hear more if you take the functional language compilation course. 

Since we didn't have time to work out the polymorphic type checking properly, there will be no exam questions about it.

Regards

  Aarne.