在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）。