在Hindley的letrec的正确形式

2018-06-04 08:08:13

我无法理解维基百科上给出的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)得到由相同的规则处理，从而导致更多的unifications和类型c ， a现在在与结果统一Uint -> Uint -> c

现在，测试会关闭以键入forall cc

in test变量测试使用新变量获得类型实例（或者全部forall cc ），根据HM规则变量，产生test :: d （与test::t统一）

导致x有效地输入d （或t ，取决于统一的情绪）

问题是： x显然应该有Uint类型，但是我认为这两种方法无法统一以产生这种类型。当test类型被关闭并再次实例化时，我不知道如何克服或连接替代/统一，从而导致信息丢失。

任何想法如何修正算法以正确生成x::Uint打字？或者这是HM系统的一个属性，它不会输入这种情况（我怀疑）？

请注意，这对于标准let来说是完全可以的，但我并不想使用let无法处理的递归定义来混淆示例。

提前致谢

回答我自己的问题：

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

向HM系统添加递归的最简单和正确的方法是使用fix谓词，定义fix f = f (fix f)并键入forall a. (a->a) -> a forall a. (a->a) -> a 。相互递归由双重固定点等处理

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

链接地址: http://www.djcxy.com/p/14201.html