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

Posted 2021-05-01

我正在制作一种强类型玩具函数式编程语言。它使用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的类型。

现实编译器/口译员使用哪些解决方案？

答案

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

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

完全有可能创建一个类型为'a的新变量（'a是新鲜的），然后将其统一起来。一定要在正确的位置概括你的变量（通常在定义之后）。