在Hindley-Milner型系统中正确形式的letrec？

Question

我无法理解维基百科上给出的HM系统的letrec定义,这里:https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions

对我来说,规则大致转换为以下算法:

1. 推断letrec定义部分中 所有内容的类型
   1. 为每个定义的标识符分配临时类型变量
   2. 使用临时类型递归处理所有定义
   3. 成对,将结果与原始临时变量统一起来
2. close(with forall)推断类型,将它们添加到基础(context)并用它推断表达式部分的类型

我遇到这样的程序有问题:

letrec
 p = (+)     --has type Uint -> Uint -> Uint
 x = (letrec
       test = p 5 5
     in test)
in x

我观察的行为如下:

• p获取临时类型的定义a
• x获取一些临时类型的定义,但现在超出了我们的范围
• in x,test获取临时类型的定义t
• pa从范围中获取临时类型,使用HM规则作为变量
• (f 5)得到由HM规则应用,造成类型是处理b(以及(统一a与结合Uint -> b)
• ((p 5) 5)由同一规则处理,导致更多的统一和类型c,a现在结果统一Uint -> Uint -> c
• 现在,测试关闭以输入 forall c.c
• 变量测试in test获取forall c.c带有新变量的类型实例(或),与变量的HM规则相符,导致test :: d(与test::t右侧统一)
• 结果x有效类型d(或者t,取决于统一的情绪)

问题:x显然应该有类型Uint,但我认为这两者无法统一生成类型.当test关闭的类型和再次实例化时,我不确定如何克服或连接替换/统一时丢失信息.

知道如何纠正算法以x::Uint正确输入？或者这是HM系统的属性,它根本不会输入这种情况(我怀疑)？

请注意,这对于标准来说完全let没问题,但我不想使用无法处理的递归定义来混淆示例let.

提前致谢

Answer 1

回答我自己的问题：

Wiki 上的定义是错误的，尽管它在一定程度上至少对于类型检查有效。

在 HM 系统中添加递归最简单和正确的方法是使用fix谓词，带有定义fix f = f (fix f)和类型forall a. (a->a) -> a。相互递归通过双定点等处理。

Haskell 解决该问题的方法（在https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b#binding-groups中描述）是（粗略地）为所有函数派生一个不完整的类型，然后再次运行派生以相互检查它们。