3
$\begingroup$

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 .

$\endgroup$
3
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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