互递归函数的Hindley Milner类型推断

Question

我正在制作一种强类型的玩具函数式编程语言。它使用Hindley Milner算法作为类型推断算法。

在实现该算法时，我有一个问题，即如何推断相互递归函数的类型。

let rec f n = if n == 0 then 0 else g (n - 1)
let rec g n = if n == 0 then 0 else f (n - 1)

f和g是相互递归的函数。现在，当类型检查器推断函数f的类型时，它也应该能够推断函数g的类型，因为它是一个子表达式。

但是，在那一刻，函数g还没有定义。因此，显然，类型检查器甚至不知道函数g的存在，以及函数g的类型。

真实世界的编译器/Intepreter使用哪些解决方案？

Answer 1

在OCaml中，相互递归的值由关键字和分隔，而不是另一个let rec。当类型系统到达递归定义时，它会将所有递归名称添加到环境中，然后像往常一样继续。

更新（感谢K.A.Buhr）：

完全可以创建类型为a的新变量（a是新的），然后将其统一。确保在正确的位置（通常在定义之后）概括变量。