關於Scala，「沒有全局類型推斷」是什麼意思？

Question

我讀過Scala的類型推斷不是全局的，所以人們必須在方法上放置類型註釋。 （這是否是「本地」類型推斷？）

我只有一點理解，其原因是從其面向對象的性質，但清晰度避開了我。是否有解釋「全球類型推斷」，爲什麼Scala不能讓初學者理解？

Answer 1

全局類型推斷的典型示例是Hindley-Milner：它需要一個給定的程序並「計算」所有必需的類型。然而，爲了達到這個目的，給定的語言需要有一些屬性（HM有擴展，試圖克服這些限制）。 HM不喜歡的兩件事是繼承和方法重載。據我瞭解，這些是Scala採用HM或其變體的主要障礙。請注意，實際上甚至嚴重依賴於HM的語言也不會達到100％的推論，例如，即使在Haskell中，你也需要不時的類型註釋。因此斯卡拉使用更有限的類型推斷形式（如你所說的「本地」），這種形式仍然比沒有好。據我所知，Scala團隊試圖在發佈到發佈的時候嘗試改進類型推斷，但到目前爲止，我只看到了更小的步驟。與HM風格類型推理器的差距仍然很大，並且不能完全關閉。

Answer 2

問題在於HM類型推斷通常在具有子類型，超載或類似特徵的語言中是不可判定的。 ^Ref這意味着越來越多的東西可以被添加到推理程序，以推斷更多特殊情況，但總是會有代碼在哪裏會失敗。

斯卡拉決定在方法參數中進行類型註釋，而其他一些地方是強制性的。這看起來似乎很麻煩，但考慮到這有助於記錄代碼並向編譯器提供它可以在一個地方理解的信息。另外，HM推理的語言經常會遇到這樣的問題，即有時在遠離原始錯誤的代碼中檢測到編程錯誤，因爲HM算法剛剛出現並偶然發生（偶然）推斷具有錯誤類型的代碼的其他部分它在失敗之前推斷出來。

Scala的推理基本上從外部（方法定義）到內部（方法內部的代碼），因此限制了錯誤類型註釋的影響。

HM推理的語言從內部到外部工作（忽略了添加類型註釋的可能性），這意味着一個單一方法中的小代碼更改有可能改變整個程序的含義。這可能是好的或壞的。

---

編號：Lower bounds on type inference with subtypes