类型Lambda Calculus

Question

我想找到lambda表达式\x y -> x y y的类型。我按以下方式进行。

1. 我们按操作的相反顺序进行，并“解压”表达式。假设整个表达式具有A类型。然后让y有x1类型，\x y -> x y有类型B。然后是A = B -> x1

1. 我们已经知道了y的类型，让\x y -> x成为C的类型。那么B = C -> x1.
2. The类型的\x y -> x显然是x1->x2->x1型。这是在前面的练习中给我们的，因为这个表达式接受两个参数并返回第一个参数。

把这一切加在一起，我们就知道：

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

正确的答案是：

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

我做错了什么？

Answer 1

在这里，我只是在下面写一些东西的类型，然后从那里开始：

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

另外一个是：

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

但,

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

是“无限”类型，即类型派生过程永不停止。