11

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

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

  1. 推断letrec定义部分 中所有内容的类型
    1. 将临时类型变量分配给每个定义的标识符
    2. 递归处理所有具有临时类型的定义
    3. 成对，将结果与原始临时变量统一起来
  2. 关闭（用forall）推断的类型，将它们添加到基础（上下文）并用它推断表达式部分的类型

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

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

我观察到的行为如下：

  • p获取临时类型的定义a
  • 的定义也x有一些临时类型，但这已经超出了我们的范围
  • in 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显然应该有 type Uint，但我认为这两者不可能统一产生类型。当类型test被关闭并再次实例化时会丢失信息，我不确定如何克服或连接替换/统一。

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

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

提前致谢

4

1 回答 1

0

回答我自己的问题：

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

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

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

于 2015-07-13T11:39:35.077 回答