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

Question

我正在编写一种没有键入函数的语言。这意味着我需要推断函数调用的返回类型，以便进行类型检查。然而，当有人编写递归函数时，类型检查器进入无限递归，试图推断函数体中函数调用的类型。

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

1. 推断函数调用实际参数的类型

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

递归函数的一个例子给了我这个问题：

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

我如何在不进入无限递归循环的情况下解决这个问题？有没有一种方法可以推断递归函数调用的类型，而不必再次进入函数体？或者用一些干净的方法从上下文推断类型？

我知道简单的解决方案可能是向函数添加类型注释，这样问题就很简单了，但在这样做之前，我想知道是否有一种方法可以解决这个问题，而不必求助于它。

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

Answer 1

根据语言的类型系统以及在需要注释时希望具有的属性，类型推断可能会有很大的不同。但无论你的语言看起来像什么，我认为有一个开创性的案例你真的应该读一读，那就是ML。ML的类型推理有一个很好的最佳点，在一个相对简单的范例中，所有这些都可以结合在一起。不需要类型注释，任何表达式都有一个最通用的类型（这个属性称为类型公理）。

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

Hindley-Milner的基本类型推断算法是算法W。在其核心，它通过给每个子表达式一个变量类型来工作：α₁, α₂, α₃, … 然后，编程语言构造对这些变量施加约束。例如，如果一个列表包含两个α类型的元素₁ 和α₂ 列表本身具有类型α₃, 该约束α₁ = α₂ 和α₃ = α列表₁. 将所有这些约束放在一起是一个统一问题。

这些约束基于对程序的纯语法阅读。如果有递归调用，则不需要知道函数的类型：这只是意味着存在一个约束，即函数返回类型的变量与其使用点的类型相同。这只是要添加到约束集的又一个等式。

我忽略了ML的一个重要方面，即表达式的类型可以泛化：表达式可以在不同的地方与不同的类型一起使用。这就是允许多态性的原因。例如，

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

是一个有效的程序，其中empty_list一次用于“整数列表”类型，一次用于“字符串列表”类型。empty_list的类型是“for anyα， list ofα”：这是参数多态性。泛化给算法增加了一些复杂性，但也消除了其他地方的复杂性，因为这是允许原则的。没有它，letempty_list=[]in...将是模棱两可的：empty_list必须有某种类型，但是如果不分析...，就无法知道是什么类型，然后当你分析上面的...时，你需要在整数和字符串之间做出选择。

根据语言的类型系统，ML和算法W可以直接重用，也可以提供一些模糊的启示。但在推理过程中使用变量并逐步约束这些变量的原则非常普遍。