Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

From my recitation class -

enter image description here

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 .

share|cite|improve this question
up vote 3 down vote accepted

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.