<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:

1. B = A -> A
2. D = C -> C
3. A = D
4. E = D
5. F = Int
6. E = F -> G

   Now you just solve the equations using unification:
7. From (2) and (3) it follows that A = C -> C
8. From (2) and (4) it follows that E = C -> C
9. From (5) and (6) it follows that E = Int -> G
10. From (8) and (9) it follows that C -> C = Int -> G, and thus, C = Int and C = G, and thus, G = Int
11. 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.


---

