type-inferencelambda-calculus

Typed Lambda Calculus


I want to find the type of the lambda expression \x y -> x y y. I proceed as follows.

  1. We go in the reverse order of operations and "unpack" the expression. Assume the whole expression has type A. Then let y have type x1 and \x y -> x y have type B. Then A = B -> x1
  2. We already know the type of y, and let \x y -> x be of the type C. Then B = C -> x1.
  3. The type of \x y -> x is obviously x1->x2->x1. This is given to us in the previous exercise and makes sense because this expression takes in two arguments and returns the first.

Putting it all together we have that:

A = B -> x1 = C -> x1 -> x1 = (x1 -> x2 -> x1) -> x1 -> x1

The correct answer is somehow:

(x1 -> x1 -> x2) -> x1 -> x2 

What am I doing wrong?


Solution

  • Here I just write stuff's types under it and go from there:

    foo = \x   y ->   x   y    y
    foo    x   y =    x   y    y 
           a   b                 :  c
                      a   b    b :  c
                      a   b :  b -> c
                      a : b -> b -> c
    foo : a -> b -> c
        ~ (b -> b -> c) -> b -> c
    

    And another one:

    bar = \x    y -> x (y   x)
    bar    x    y =  x (y   x)
           a    b                        :  c
                     a (b   a)           :  c
                      ---------
                        b   a :  d
                        b : a -> d
                     a :         d       -> c
    
    bar :  a -> b -> c
        ~ (d -> c) -> ( a       -> d) -> c
        ~ (d -> c) -> ((d -> c) -> d) -> c
    

    But,

    baz   x = x   x
          a   a   a :  b
              a : a -> b
    
    baz : a -> b
        ~ (a -> b) -> b
        ~ ((a -> b) -> b) -> b
        ~ (((a -> b) -> b) -> b) -> b
        ........
    

    is an "infinite" type, i.e. the process of type derivation never stops.