Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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?

share|improve this question

1 Answer 1

up vote 14 down vote accepted

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.

share|improve this answer

Your Answer

 
discard

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.