types - 在 Lambda 演算中推断类型

Question

我想知道是否有人会在 lambda 演算方面拥有一些不错的资源，特别是在类型推断方面。我正在准备考试，我似乎找不到任何关于 lambda 类型以及如何在我完成的任何教程中推断的信息。

我有一个考试题，我试图在星期二解决这个问题..

在下面的 lambda 演算表达式中推断所有变量和带括号的子表达式的类型： (\表示 lambda)

(((\x.(\y.(x,y)y))g)h)

我保证这不是家庭作业！任何帮助都会非常受欢迎。

Answer 1

为 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 相当不错，但在我看来，对于这样一个简单直观的主题来说，技术含量极高。