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