求解λ表达式\x y -> x y y的类型时出错，求错误原因

你的推导过程回顾 #

• 假设整体类型为A，令y的类型为x1，\x y -> x y的类型为B，得出A = B -> x1
• 令\x y -> x的类型为C，得出B = C -> x1
• 认为\x y -> x的类型是x1->x2->x1，代入后得到A = (x1 -> x2 -> x1) -> x1 -> x1

正确结果应为：(x1 -> x1 -> x2) -> x1 -> x2

错误原因分析 #

• 拆解逻辑错误：λ表达式\x y -> x y y的实际结构是(\x -> (\y -> (x y) y))，要从最内层的函数应用(x y) y开始推导，而非将外层拆解为(\x y -> x y)再接收y作为参数——你完全搞反了函数应用的顺序和参数绑定关系。
• 类型变量复用冲突：你将外层y的类型设为x1后，直接套用\x y -> x的通用类型x1->x2->x1，这里的x1是该λ表达式第一个参数的类型，和外层y的x1是完全无关的类型变量，强行复用导致类型匹配错误。

正确推导步骤 #

• 设y的类型为a（避免变量名混淆）
• 分析x y y：x需要先接收一个类型为a的参数（即y），返回的结果仍能接收一个类型为a的参数（还是y），最终返回类型b。因此x的类型是a -> a -> b
• 整个λ表达式先接收x（类型a->a->b），再接收y（类型a），最终返回x y y的结果（类型b）。所以整体类型为(a -> a -> b) -> a -> b，替换为你使用的变量名就是(x1 -> x1 -> x2) -> x1 -> x2，与正确结果一致。

内容的提问来源于stack exchange，提问作者Angela Riley