1

我试图通过用我常用的语言 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 中尝试时，我得到了预期的结果。

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

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

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

编辑

如果有人有类似的问题并想知道我是如何解决的，我会按照Algorith W Step By Step进行操作。在第 2 页的底部，它说“将Types方法扩展到列表有时会很有用。” 因为这听起来对我来说不是强制性的，所以我决定跳过那部分，稍后再重新审视。

然后我将ftv函数 forTypeEnv直接翻译成 Clojure，如下所示(ftv (vals env))：由于我已经实现ftv为cond表单并且没有seqs 的子句，所以它只是返回nil了(vals env). 这当然正是静态类型系统旨在捕获的那种错误！无论如何，我只是重新定义了与地图ftv相关的条款，并且它有效。env(reduce set/union #{} (map ftv (vals env)))

4

1 回答 1

6

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

让我们手动输入术语。

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

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

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

但是，这是关键点，我们不应该概括to 的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）。

于 2017-06-12T21:53:44.260 回答