I want to find the type of the lambda expression \x y -> x y y
. I proceed as follows.
A
. Then let y
have type x1 and \x y -> x y
have type B
. Then A = B -> x1
y
, and let \x y -> x
be of the type C
. Then B = C -> x1
.\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?
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.