ML - Type Interface

Question

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 .

Answer 1

ML functions take a single argument. There are two common techniques to pass two arguments to a function.

• One is to create a pair (2-tuple) p = (x, y) and apply the function to the pair; the type of the function is then ('a * 'b) -> 'c.
• The other approach is to make a function that takes one argument and returns a function that receives the second argument and does the work. This approach is what is done for + here and is called currying. The function then has the type 'a -> ('b -> 'c). Since this is common, the -> operator on types is chosen to be right-associative, so 'a -> ('b -> 'c) can be written 'a -> 'b -> 'c.

---

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.