如何对没有显式返回类型的递归函数进行类型检查？

Question

我正在编写一种不带类型的语言，这意味着我需要推断函数调用的返回类型以进行类型检查。但是，当有人编写递归函数时，类型检查器会陷入无限递归，尝试推断函数体内部函数调用的类型。

类型检查器执行以下操作：

1. 推断函数调用实际参数的类型。 2. 创建实际参数类型到形式参数的映射。 3. 使用映射在函数体中使用的参数上注释类型。 4. 推断并返回函数体的返回类型。

步骤4尝试推断函数体内部函数调用的类型，该函数调用再次调用相同的类型检查器函数，从而导致无限递归。

下面是一个给我带来问题的递归函数示例：

function factorial(n) = n<1 ? 1 : n*factorial(n-1); // Function definition.
...
assert 24 == factorial(4); // Function call expression usage example.

如何避免无限递归循环的问题？有没有一种方法可以推断递归函数调用的类型而不必再次进入函数体内？或者有一种从上下文中推断类型的简洁方式吗？

我知道添加函数类型注释可能是一个简单的解决方案，这样问题就很容易解决了，但在这样做之前，我想知道是否有一种方法可以在不使用这种方法的情况下解决这个问题。

我还希望解决方案适用于相互递归的情况。

最初的回答：如何在无需添加类型注释的情况下避免无限递归循环？是否有一种从上下文中推断递归函数调用类型的简便方式？此外，如何处理相互递归的情况？

- tgonzalez89

---

你需要为函数分配一些占位符类型，然后在更多信息可用时填充它。我们称factorial的类型为T，然后继续。我们知道T是一个函数。接下来，我们看到该函数需要一个参数，因此我们将T更新为“一个参数的函数”。然后我们发现，在n < 1的情况下，它返回1。因此，T必须是“返回整数的一个参数函数”。现在当我们查看n*factorial(n-1)时，我们现在知道n被乘以一个整数，等等。 - Kaz

请注意，虽然[so]倾向于接受关于应用计算机科学的边缘问题，但这些问题更适合在[cs.se]上讨论，并且在那里获得良好的答案的机会更大。请勿重新发布，但如果您希望您的问题出现在[cs.se]上，您可以标记您的问题并要求管理员迁移它。 - Gilles 'SO- stop being evil'

Answer 1

类型推断可以根据语言的类型系统及你想要的注释需要性质而有很大的变化。但无论你的语言看起来像什么，我认为有一个非常重要的案例你应该阅读，那就是ML。ML的类型推断占据了一个非常好的平衡点，在相对简单的范式下完美地契合在一起。不需要任何类型注释，并且任何表达式都有一个最通用的类型（这个特性称为 typing 的 principle）。

ML的类型系统是Hindley-Milner类型系统，具有参数多态性。表达式的类型可以是特定的类型，也可以是“任意”的类型。更准确地说，表达式的类型构造器可以是特定的类型构造器或“任意”，而类型构造器本身可以具有参数，这些参数本身可以是特定的类型构造器或“任意”。例如，空列表的类型为“任意类型的列表”。两个独立的表达式可能具有“任意”类型，但可以被限制为具有相同的类型，无论它是什么，因此“任意”用变量表示。例如，function list_of_two(x, y) = [x, y]（在类似于你的语言的符号中）限制了x和y具有相同的类型，因为它们被插入到同一个列表中，但是该类型可以是任何类型，因此此函数的类型为“取任何两个相同类型α的参数，并返回类型为α的列表的值”。

Hindley-Milner 的基本类型推断算法是 W 算法。它的核心思想是为每个子表达式赋予一个变量类型：α₁，α₂，α₃，… 然后编程语言的构造会对这些变量施加约束。例如，如果一个列表包含两个类型分别为 α₁ 和 α₂ 的元素，而列表本身的类型为 α₃，则有约束条件 α₁ = α₂ 且 α₃ = α₁ 的列表。将所有这些约束条件放在一起就形成了一个 合一（unification）问题。

这些约束条件基于程序的纯语法解读。如果存在递归调用，你不需要知道函数的类型：这只意味着返回类型的变量与其使用点处的类型相同，这只是要添加到约束集合中的另一个方程。

我漏掉了机器学习中一个重要的方面，即表达式的类型可以被泛化：一个表达式可以在不同的地方使用不同的类型。这就是多态性的实现方式。例如，

let empty_list = [] in
(empty_list @ [3]), (empty_list @ ["hello"])

这是一个有效的程序，在该程序中，empty_list 一次使用了“整数列表”类型，一次使用了“字符串列表”类型。 empty_list 的类型是“对于任何α，α列表”：这就是参数多态性。泛化会使算法变得更加复杂，但它也会在其他地方减少复杂性，因为这就是允许原则性的原因。如果没有它，let empty_list = [] in … 将是模棱两可的： empty_list 必须具有某种类型，但是在没有分析 … 的情况下，没有办法知道它的类型，然后当你分析上面的 … 时，你需要在整数和字符串之间做出选择。

根据您的语言类型系统的不同，ML 和算法 W 可能直接可重用，或者只提供一些模糊的灵感。但是，在推断期间使用变量，并逐步约束这些变量的原则非常普遍。

- Gilles 'SO- stop being evil'

---

这篇文章非常清晰地解释了Hindley-Milner类型系统，甚至包括一个例子。它很好地补充了这个答案。对于任何想要为自己的语言实现该系统的人来说，这是一个很好的起点。 - tgonzalez89