在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页的底部，它表示“有时将类型的方法扩展到列表中。”由于它对我来说听起来不是强制性的，我决定跳过那部分，稍后重新审视它。

然后，我将TypeEnv的ftv函数直接编译为Clojure，如下所示：(ftv (vals env))。由于我已将ftv作为cond表单执行，并且没有seq s的条款，因此它简单地返回nil表示(vals env)。这当然就是静态类型系统设计要捕获的那种错误！无论如何，我只是重新定义ftv有关env地图的条款为(reduce set/union #{} (map ftv (vals env)))，它的工作原理。

Answer 1

很难说出有什么问题，但我猜测你的推广是错误的。

让我们手动键入术语。

\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，一旦一般化，可以被字符转换为t1）。