Hindley-Milner类型系统中letrec的正确形式是什么？

Question

我有困难理解维基百科上提供的HM系统的letrec定义，链接在这里：https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions 对我来说，该规则大致转化为以下算法:

1. 对letrec定义部分中的所有内容推断类型
   1. 给每个已定义标识符分配临时类型变量
   2. 使用临时类型递归处理所有定义
   3. 成对地将结果与原始临时变量统一(unify)
2. 使用forall关闭(infer)推断出的类型，将其添加到基础(context)中并使用该类型推断表达式部分的类型

我遇到了下面这样的程序问题:

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

我观察到的行为如下：

• p的定义得到临时类型a
• x的定义也得到了一些临时类型，但这已经超出了我们的范围
• 在x中，test的定义得到了临时类型t
• p从作用域中获取了临时类型a，使用变量的HM规则
• (f 5)通过应用的HM规则进行处理，结果类型为b（以及(a与Uint -> b一致）的统一）
• ((p 5) 5)通过相同的规则进行处理，导致更多的统一和类型c，现在，结果中的a与Uint -> Uint -> c一致
• 现在，test被关闭为类型forall c.c
• in test的变量得到了类型实例（或forall c.c），根据变量的HM规则，相应地得到了test :: d（它会立即与test::t统一）
• 结果中的x实际上具有类型d（或t，取决于统一的情绪）

问题是：x显然应该具有类型Uint，但我看不到这两个类型如何能够统一产生该类型。当test的类型被关闭并再次实例化时，存在信息丢失，我不确定如何克服或与替换/统一联系起来。

您有什么想法可以纠正算法以正确生成x::Uint类型？还是这是HM系统的属性，它根本无法为这种情况编写类型（我怀疑）？

请注意，使用标准的let将完全没有问题，但我不想用递归定义来混淆不能由let处理的示例。

提前感谢您。

- exa

Answer 1

回答自己的问题：

维基上的定义是错误的，尽管它至少在类型检查方面起作用。

将递归添加到HM系统的最简单和正确的方法是使用fix谓词，其定义为fix f = f (fix f)，类型为forall a. (a->a) -> a。双重不动点处理相互递归等。

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

- exa

---

维基上的定义看起来对我来说是正确的。你能具体指出哪里不正确吗？ - max