我有困难理解维基百科上提供的HM系统的letrec定义,链接在这里:https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Recursive_definitions
对我来说,该规则大致转化为以下算法:
我观察到的行为如下:
您有什么想法可以纠正算法以正确生成
请注意,使用标准的
提前感谢您。
- 对letrec定义部分中的所有内容推断类型
- 给每个已定义标识符分配临时类型变量
- 使用临时类型递归处理所有定义
- 成对地将结果与原始临时变量统一(unify)
- 使用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
处理的示例。提前感谢您。