首页 文章

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

提问于
浏览 次
11

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

对我来说，规则大致转换为以下算法：

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

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

  • 以临时类型递归处理所有定义

  • 成对，将结果与原始临时变量统一

  • close（使用 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 的变量测试获取带有新变量的类型实例（或 forall c.c ），与变量的HM规则相符，产生 test :: d （与 test::t 统一）

  • 结果 x 有效输入 d （或 t ，取决于统一的情绪）

问题： x 显然应该有 Uint 类型，但我认为这两者无法统一生成类型 . 当 test 的类型被关闭而实例'd again that I'不确定如何克服或连接替换/统一时，会丢失信息 .

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

请注意，对于标准 let ，这将完全正常，但我没有't want to obfuscate the example with recursive definitions that can'由 let 处理 .

提前致谢

functional-programming type-inference lambda-calculus hindley-milner

1 回答

  • 0

    回答我自己的问题：

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

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

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

    回复于

相关问题