functional-programming - Hindley-Milner 类型系统中 letrec 的正确形式？

Question

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

对我来说，规则大致转化为以下算法:

推断 letrec 中所有内容的类型定义部分

为每个定义的标识符分配临时类型变量

递归处理所有具有临时类型的定义

成对，将结果与原来的临时变量

统一起来

关闭(用 forall )推断的类型，将它们添加到基础(上下文)并用它推断表达式部分的类型

我在使用这样的程序时遇到了问题:

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 一致

现在，测试结束输入 forall c.c

in test的变量测试根据变量的 HM 规则，使用新变量获取类型实例(或 forall c.c )，结果是 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 中描述)是(粗略地)为所有函数派生一个不完整的类型，然后再次运行派生以相互检查它们。