<p>Yes, your type inference seems incomplete. This example can be dealt with fairly trivially, by computing the respective type equations, e.g. in the style Hindley/Milner does it.</p>
<p>Alpha-renaming the example makes it easier to follow:</p>
<pre><code>((\x.x) (\y.y)) 10
</code></pre>
<p>For maximum clarity, let's start by assigning type variables to each sub expression:</p>
<ul>
<li>x : A</li>
<li>(\x.x) : B</li>
<li>y : C</li>
<li>(\y.y) : D</li>
<li>(\x.x) (\y.y) : E</li>
<li>10 : F</li>
<li>((\x.x) (\y.y)) 10 : G</li>
</ul>
<p>Now, the typing rules of the language impose certain equality constraints for each language construct:</p>
<ul>
<li>From the typing rule for lambda, applied to (\x.x), it follows that B = A -&gt; A</li>
<li>Likewise, D = C -&gt; C</li>
<li>From the typing rule for application, applied to (\x.x) (\y.y), it follows that A = D and E = D</li>
<li>From the typing rule for integers it follows that F = Int</li>
<li>From the typing rule for application, applied to (...) 10, it follows that E = F -&gt; G</li>
</ul>
<p>In summary, this yields the following equations:</p>
<ol>
<li><p>B = A -&gt; A</p>
</li>
<li><p>D = C -&gt; C</p>
</li>
<li><p>A = D</p>
</li>
<li><p>E = D</p>
</li>
<li><p>F = Int</p>
</li>
<li><p>E = F -&gt; G</p>
<p>Now you just solve the equations using unification:</p>
</li>
<li><p>From (2) and (3) it follows that A = C -&gt; C</p>
</li>
<li><p>From (2) and (4) it follows that E = C -&gt; C</p>
</li>
<li><p>From (5) and (6) it follows that E = Int -&gt; G</p>
</li>
<li><p>From (8) and (9) it follows that C -&gt; C = Int -&gt; G, and thus, C = Int and C = G, and thus, G = Int</p>
</li>
<li><p>From (7) and (10) it follows that A = Int -&gt; Int</p>
</li>
</ol>
<p>A and C are the types you are ultimately interested in, because they are the ones you have to assign to x and y, respectively. They yield the typed term</p>
<pre><code>((\x:(Int-&gt;Int).x) (\y.Int.y)) 10
</code></pre>
<p>Its overall type is G = Int.</p>

CC BY-SA 3.0
2014-07-19T19:51:58.420Z
2014-07-19T21:01:33.887Z
2020-06-17T09:38:08.363Z
Andreas Rossberg
<p>I'm developing a tiny programming language to try to wrap my head around type inference, and I'm trying to figure out if its behavior makes sense or not. Here's the problem:</p>

<p>The identity function <code>\x.x</code> can't be unified to a single type, but applied to something, it can, i.e. <code>(\x.x) 10 : Int</code>. However, right now, the expression:</p>

<pre><code>((\x.x) (\x.x)) 10
</code></pre>

<p>can't be unified, because the expression <code>(\x.x) (\x.x)</code> doesn't have a single type. The type checker doesn't do any evaluation, so it can't tell that the above expression is equivalent to <code>\x.x</code>. The type checker only sees the expression, tries to determine the type of it, and fails before trying to apply it to <code>10</code>. </p>

<p>Is this typical behavior, or am I being inconsistent with my type inference?</p>

<pl.programming-languages><type-theory><lambda-calculus><type-inference>
Is this behavior in a programming language inconsistent?
Benjamin Kovach
# Is this behavior in a programming language inconsistent?

(Asked by: username_0 on 2014-07-19)

I'm developing a tiny programming language to try to wrap my head around type inference, and I'm trying to figure out if its behavior makes sense or not. Here's the problem:
The identity function \x.x can't be unified to a single type, but applied to something, it can, i.e. (\x.x) 10 : Int. However, right now, the expression:
((\x.x) (\x.x)) 10

can't be unified, because the expression (\x.x) (\x.x) doesn't have a single type. The type checker doesn't do any evaluation, so it can't tell that the above expression is equivalent to \x.x. The type checker only sees the expression, tries to determine the type of it, and fails before trying to apply it to 10. 
Is this typical behavior, or am I being inconsistent with my type inference?

**Tags:** pl.programming-languages, type-theory, lambda-calculus, type-inference

---

## 1 answers

### Answer by username_1 on 2014-07-19. Score: 14 | Accepted answer

Yes, your type inference seems incomplete. This example can be dealt with fairly trivially, by computing the respective type equations, e.g. in the style Hindley/Milner does it.
Alpha-renaming the example makes it easier to follow:
((\x.x) (\y.y)) 10

For maximum clarity, let's start by assigning type variables to each sub expression:

x : A
(\x.x) : B
y : C
(\y.y) : D
(\x.x) (\y.y) : E
10 : F
((\x.x) (\y.y)) 10 : G

Now, the typing rules of the language impose certain equality constraints for each language construct:

From the typing rule for lambda, applied to (\x.x), it follows that B = A -> A
Likewise, D = C -> C
From the typing rule for application, applied to (\x.x) (\y.y), it follows that A = D and E = D
From the typing rule for integers it follows that F = Int
From the typing rule for application, applied to (...) 10, it follows that E = F -> G

In summary, this yields the following equations:

B = A -> A

D = C -> C

A = D

E = D

F = Int

E = F -> G
Now you just solve the equations using unification:

From (2) and (3) it follows that A = C -> C

From (2) and (4) it follows that E = C -> C

From (5) and (6) it follows that E = Int -> G

From (8) and (9) it follows that C -> C = Int -> G, and thus, C = Int and C = G, and thus, G = Int

From (7) and (10) it follows that A = Int -> Int


A and C are the types you are ultimately interested in, because they are the ones you have to assign to x and y, respectively. They yield the typed term
((\x:(Int->Int).x) (\y.Int.y)) 10

Its overall type is G = Int.


---

