我正在编写一种不键入函数的语言。这意味着我需要推断函数调用的返回类型才能进行类型检查。但是，当有人编写递归函数时，类型检查器会进入无限递归状态，试图推断函数体内函数调用的类型。
类型检查器执行以下操作：
- 推断函数调用实际参数的类型。
- 创建实际参数类型到正式参数的映射。
- 使用映射对函数体内使用的参数进行批注类型。
- 推断并返回函数体的返回类型。
步骤 4 尝试推断函数体内函数调用的类型，该函数再次调用相同类型的检查器函数，从而导致无限递归。
一个递归函数的例子，给了我这个问题：
function factorial(n) = n<1 ? 1 : n*factorial(n-1); // Function definition.
...
assert 24 == factorial(4); // Function call expression usage example.
如何在不进入无限递归循环的情况下解决此问题？有没有办法推断递归函数调用的类型，而不必再次进入正文？还是一些从上下文推断类型的干净方法？
我知道简单的解决方案可能是向函数添加类型注释，这样问题就微不足道了，但在这样做之前，我想知道是否有办法在不诉诸那个的情况下解决这个问题。
我还希望解决方案适用于相互递归。
类型推断可能会有很大差异，具体取决于语言的类型系统以及您希望在何时需要注释时具有的属性。但无论你的语言是什么样子的，我认为有一个开创性的案例你真的应该阅读，那就是ML。 ML的类型推断有一个很好的甜蜜点，它在一个相对简单的范式中组合在一起。不需要类型注释，并且任何表达式都具有单个最通用的类型(此属性称为类型主体(。
ML的类型系统是Hindley-Milner类型系统，它具有参数多态性。表达式的类型可以是特定类型，也可以是"任意"。更准确地说，表达式的类型构造函数是特定类型构造函数或"any"，类型构造函数可以具有参数，这些参数本身具有特定类型构造函数或"any"。例如，空列表的类型为"任意列表"。可以单独具有"any"类型的两个表达式可以限制为具有相同的类型，无论它是什么，因此"any"用变量表示。例如，function list_of_two(x, y) = [x, y](以类似于您的语言的表示法(约束x和y具有相同的类型，因为它们插入到同一个列表中，但该类型可以是任何类型，因此此函数的类型是"α获取相同类型的任意两个参数，并返回 list 类型的值 α"。
Hindley-Milner 的基本类型推断算法是算法 W。它的核心是通过为每个子表达式提供一个变量类型来工作的：α₁、α₂、α₃、...然后，编程语言构造对这些变量施加约束。例如，如果列表包含两个类型为 α₁ 和 α₂ 的元素，并且列表本身的类型为 α₃，则此约束α₁ = α₂ 和 α₃ = α₁ 列表。将所有这些约束放在一起是一个统一问题。
约束基于程序的纯语法读取。如果存在递归调用，则无需知道函数的类型：它只是意味着存在一个约束，即函数返回类型的变量与其使用点的类型相同。这只是要添加到约束集的另一个等式。
我省略了 ML 的一个重要方面，即表达式的类型可以泛化：表达式可以在不同的地方与不同类型的一起使用。这就是允许多态性的原因。例如
let empty_list = [] in
(empty_list @ [3]), (empty_list @ ["hello"])
是一个有效的程序，其中empty_list一次用于"整数列表"类型，一次用于"字符串列表"类型。empty_list的类型是"对于任何α，α列表"：这就是参数多态性。泛化增加了算法的一些复杂性，但它也消除了其他地方的复杂性，因为这就是允许原则性的原因。没有它，let empty_list = [] in …将是模棱两可的：empty_list必须具有某种类型，但是如果不分析…就无法知道是什么类型，然后当您分析上述…时，您需要在整数和字符串之间进行选择。
根据您的语言类型系统，ML 和算法 W 可能可以直接重用，或者可能只是提供一些模糊的灵感。但是在推理过程中使用变量并逐步约束这些变量的原则是非常通用的。