haskell - Hindley-Milner 中的 `Let` 推理

Question

我正在尝试通过用我常用的语言 Clojure 实现算法 W 来自学 Hindley-Milner 类型推理。我遇到了 let 推理的问题，我不确定我是否做错了什么，或者我期望的结果是否需要算法之外的东西。

基本上，使用 Haskell 表示法，如果我尝试推断其类型:

\a -> let b = a in b + 1

我明白了:

Num a => t -> a

但我应该得到这个:

Num a => a -> a

同样，我实际上是在 Clojure 中执行此操作，但我认为问题不是 Clojure 特有的，因此我使用 Haskell 表示法使其更清晰。当我在 Haskell 中尝试时，我得到了预期的结果。

无论如何，我可以通过将每个 let 转换为函数应用程序来解决该特定问题，例如:

 \a -> (\b -> b + 1) a

但是我失去了 let 多态性。由于我对 HM 没有任何先验知识，我的问题是我是否遗漏了一些东西，或者这是否只是算法的工作方式。

编辑

如果有人遇到类似问题并想知道我是如何解决它的，我正在关注 Algorith W Step By Step .在第 2 页的底部，它说“将 Types 方法扩展到列表偶尔会很有用。”因为这对我来说听起来不是强制性的，所以我决定跳过那部分，稍后再看。

然后我将 TypeEnv 的 ftv 函数直接翻译成 Clojure，如下所示:(ftv (vals env))。因为我已经将 ftv 实现为 cond 形式并且没有用于 seq 的子句，所以它只是返回了 nil 为 (vals env)。这当然正是静态类型系统旨在捕获的那种错误!无论如何，我只是将 ftv 中与 env 映射相关的子句重新定义为 (reduce set/union #{} (map ftv (vals env))) 并且有效。

Answer 1

很难说哪里出了问题，但我猜你的 let-generalization 是错误的。

让我们手动输入术语。

\a -> let b = a in b + 1

首先，我们将 a 与一个新的类型变量相关联，比如 a::t0。

然后我们输入b = a。我们也得到 b::t0。

然而，这是关键点，我们应该不将 b 的类型泛化为 b::forall t0。 t0。这是因为我们只能对环境中不存在的 tyvar 进行概括:在这里，相反，我们在环境中确实有 t0，因为 a::t0 在那里.

如果您对它进行泛化，您将得到一种对于 b 而言过于笼统的类型。然后 b+1 变成 b+1::forall t0。 Num t0 => t0，并且整个术语得到 forall t0 t1。 Num t1 => t0 -> t1 因为 a 和 b 的类型不相关(t0，一旦泛化，就可以alpha 转换为 t1)。