我想知道是否有人会在 lambda 演算方面拥有一些不错的资源，特别是在类型推断方面。 我正在准备考试，我似乎无法在我完成的任何教程中找到任何关于 lambda 类型以及如何推断的信息。
我有一个考试题，我想在星期二解决这个问题..
推断以下 lambda 演算表达式中所有变量的类型和带括号的子表达式： (\表示 lambda)
(((\x.(\y.(x,y)y))g)h)
我保证这不是家庭作业！非常欢迎任何帮助。
【问题讨论】：
标签： types lambda calculus inference
为 lambda 项推断（最一般、最简单的）类型是一项非常简单且极具指导性的活动。当你试图破译一个 lambda 项时，从猜测它的类型开始是一个非常好的方法。
类型推断背后的一般思想是，您开始将泛型类型（类型变量）归因于任何标识符，然后根据您在术语中对标识符的使用来细化该类型。这在 lambda 演算中非常容易，因为标识符只能以两种方式使用：作为函数的参数或作为函数。
例如，在您的示例中，假设 x：α 和 y：β。但是 x 应用于 y， 因此它必须有一个函数类型，而且它的输入必须与参数 y 的类型兼容，因此我们将 α 细化为 (β -> γ)，其中 γ 是应用程序的（因此未知的）结果类型（ x y)。
项 (x y) 反过来应用于 y。这意味着 γ 实际上也必须是一个函数类型，也就是说，γ = β -> δ。
在这种情况下，这基本上结束了分析。
为了清楚起见，我在下面报告了所有子术语的类型（请注意所有应用程序的类型都很好）：
x : β -> β -> γ
y : β
(x y) : β -> γ
((x y) y) : γ
\y.((x y) y) : β -> γ
\x.\y.((x y) y) : (β -> β -> γ) -> β -> γ
此外，我们得出 g:β -> β -> γ 和 h:β 的结论。 整个表达式的类型为 γ。
这个术语提供了一个更有趣的例子 \y.\x.(y (y x))。 假设 x：α。那么 y 必须具有 α -> β 类型，其中 β 是结果 (y x) 的类型。该项再次作为 y 的输入传递，这意味着 α=β。 所以， \y.\x.(y (y x)) : (α -> α) -> α -> α
一般来说，在某些情况下，当您多次使用同一个标识符时，您需要统一它们的类型，推断它们之间最一般的实例。
关于 Damas-Milner 类型推理算法的 wikipage 相当不错，但在我看来，对于这样一个简单直观的主题来说，技术性很强。
【讨论】：