Hacker News
The article argues that choosing between Hindley-Milner and bidirectional typing is a false dichotomy, suggesting that developers should instead focus on whether their language requires generics and unification.
AI 生成摘要
這篇文章指出在 Hindley-Milner 與雙向類型系統之間做選擇是一個假命題，開發者實際上應該問的是自己的語言是否需要泛型與合一機制。
在開發程式語言時，選擇類型系統（Type System）往往是開發者面臨的第一道難關。本文探討了 Hindley-Milner（HM）與雙向類型檢查（Bidirectional Typing）之間的選擇，指出這兩者並非互斥的對立面，而是一種超集關係。作者認為開發者不應糾結於演算法的選擇，而應優先自問語言是否需要支援「泛型」，因為這決定了是否需要引入複雜的合一運算（Unification）。
針對文章提出的觀點，Hacker News 的討論進一步深化了類型系統在實務應用中的複雜性。有評論者指出，雖然文章強調泛型的重要性，但開發者還必須考慮「子類型」（Subtyping）的需求。如果語言計畫支援類別繼承或子類型關係，傳統的 HM 類型推導可能會變得不可判定（Undecidable），這也是為什麼許多現代語言在實踐中最終都會轉向雙向類型系統。以 Haskell 為例，雖然它最初是以 HM 為基礎，但為了支援更高級的特性如不透明類型（Impredicative Types）或顯式類型應用，也逐漸向雙向類型檢查靠攏。
此外，社群中也出現了關於類型系統「可解釋性」的討論。有意見認為，如果開發者選擇了 HM 系統，應該進一步考慮「組合式類型系統」（Compositional Type System）。這種做法能提供更好的類型推導說明，並在發生錯誤時給出更易於理解的錯誤訊息，這對於提升開發者體驗至關重要。討論中也流露出一種技術社群特有的浪漫情懷，有留言者回憶起在學術環境中，將類型推導與定理證明作為日常閒談話題的時光，認為這種對理論的純粹追求是推動技術演進的動力。
綜合來看，社群達成了一種共識：雙向類型檢查在處理複雜特性（如子類型、泛型與高級類型推論）時具有更高的靈活性與擴充性。雖然 HM 在自動推導上非常強大，但隨著語言功能的增加，純粹的 HM 往往難以支撐。因此，對於大多數通用型語言的開發者來說，將雙向類型檢查與合一運算結合，似乎是目前最穩健且具前瞻性的路徑。
在討論中，有評論者推薦深入研究組合式類型系統，並分享了相關的技術簡報：unsafePerform.IO 上的專案「Compositional Typing」，該資源詳細探討了如何透過組合式方法改善類型錯誤的解釋能力。