手动推导Haskell表达式(\x y z -> (x y) z)的类型的方法

我们可以按以下四步完成推导：

• 第一步：为所有未知量分配初始类型占位符
  该lambda表达式接收3个参数x、y、z，返回(x y) z的计算结果。我们先给每个量分配临时的类型变量：
  x :: a，y :: b，z :: c，返回值类型为d，此时整个表达式的初始类型框架为a -> b -> c -> d
• 第二步：从子表达式x y推导约束
  Haskell中只有函数类型可以被应用，形如f arg的结构说明f一定是参数类型和arg匹配的函数。这里x被应用到y，因此x不能是任意类型a，必须是接收b类型参数、返回值为某未知类型e的函数，即a = b -> e，此时x y的类型为e
• 第三步：从(x y) z推导约束
  现在x y的类型为e，它又被应用到z（类型c），同理可得e必须是接收c类型参数、返回值为整个表达式结果d的函数，即e = c -> d
• 第四步：合并所有约束得到最终类型
  把约束代回初始类型框架：x的类型为b -> e，而e = c -> d，因此x :: b -> c -> d。替换初始框架里的a后，最终类型为：
  (b -> c -> d) -> b -> c -> d

你可以在GHCi中执行:t (\x y z -> (x y) z)验证推导结果，该表达式本质是柯里化函数的应用变形，和\x y z -> x y z完全等价。

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