# ML - Type Interface

From my recitation class -

Can you please explain

• why does operator $"+"$ signature is $int \rightarrow (int \rightarrow int)$ ?

• How does this graph is build ?

• And what is mean $t=u \rightarrow s$ ?

Thanks in advance .

-

The graph, and the derivation on the left, present a simple approach to ML type inference by unification. The first steps are with the atomic subexpressions: 2 : int, + : int -> (int -> int), and so on. Next, building on, we have the subexpression plus 2, which is an application; the types of + and 2 must be unified with $p \to q$ and $p$ for some $(p,q)$, which leads to $p = \mathrm{int} \to \mathrm{int}$ and $q = \mathrm{int}$ and the type of (plus 2) is $\mathrm{int}$. The derivation on the left shows the type inference for $(\lambda x. ((+ \: 2) \: x))$ from the types of $(+ \: 2)$ and $x$.
The graph represents the unification steps (with some trivial steps for atomic subexpressions omitted). Four variables $r$, $s$, $t$, $u$ are created to designate the type of each of the non-atomic subexpressions. The straight lines show the expression tree. The curvy line links the occurrence of the variable $x$ with its binding site.