“让我们在欣德利进行推理
我试图通过在我通常使用的语言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的知识，我的问题是我在这里是否缺少某些东西，或者这只是算法的工作方式。
编辑
如果任何人有类似的问题，并想知道我是如何解决它，我是按照算法W步骤。 在第2页的底部，它说：“将类型方法扩展到列表有时会很有用。” 由于它对我来说听起来不是强制性的，我决定跳过那部分，稍后重新审视它。
然后我翻译的ftv函数TypeEnv直接进入Clojure的如下： (ftv (vals env)) 由于我已经实施了ftv作为cond形式，并且没有seq s的子句，它仅仅返回nil (vals env) 。 这当然就是静态类型系统设计要捕获的那种错误！ 无论如何，我只是重新定义了有关env map的ftv的子句(reduce set/union #{} (map ftv (vals env)))并且它工作正常。
很难说出有什么问题，但我想你的推广是错误的。
让我们手动键入术语。
a -> let b = a in b + 1
首先，我们将a与一个新的类型变量相关联，比如a :: t0 。
然后我们输入b = a 。 我们也得到b :: t0 。
然而，这是关键点，我们不应该一概而论的类型b到b :: forall t0. t0 b :: forall t0. t0 。 这是因为我们只能概括一个在环境中不存在的tyvar：在这里，相反，我们确实在环境中有t0 ，因为a :: t0在那里。
如果你推广它，你会得到一个太普通类型的b 。 那么b+1变成b+1 :: forall t0. Num t0 => t0 b+1 :: forall t0. Num t0 => t0 ，整个学期得到forall t0 t1. Num t1 => t0 -> t1 forall t0 t1. Num t1 => t0 -> t1因为a和b的类型是不相关的（ t0 ，一旦一般化，可以被alpha转换为t1 ）。