Is this behavior in a programming language inconsistent?

Question

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?

Answer 1

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.