Hindley-Milner 是什麼以及函數式編程中它的用途是什麼？

01-27

一直寫OOP，最近入FP的坑對於Hindley-Milner的概念和作用不是很理解，請老司機解釋下，以及對於應用程序員它的實際用途是？
另外，目前fop相關的知識主要是某種編程語言書籍中提到的，感覺不成體系，請推薦技能樹點法。謝謝

Hindley-Milner是一個經典的類型系統，是ML家族語言的源頭。它在STLC（Simply Typed Lambda Calculus）的基礎上有限支持了parametric polymorphism，這意味著許多組合子的類型是泛化過的，可以apply到不同類型的參數上使用（一些trivial的例子包括：SKI，list的length/map/fold/filter等），減少boilerplate code，從實用角度來講是非常重要的特性。

Hindley-Milner的優點：

1. 有principal type，可以做100%的global type inference。不用標類型簽名~

2. 它的polymorphism是Rank-1的，不允許Rank-N polymorphism（將polymorphic function作為first-class value使用，而且其type variable不被capture住）。從編譯器實現的角度來講，這意味著我們可以採取類似C++ template的編譯策略：在每個polymorphic function的call site進行特化，polymorphic datatype也可以實現非常aggresive的unbox優化。（ref：Whole-Program Compilation in MLton）

Hindley-Milner的缺點：

1. Rank-N polymorphism有時候還是有用的。解決方式：沒有標類型簽名時，默認按HM系統進行推導，標了則可以使用Rank-N特性。這項工作最初是Martin Odersky做的（ref：Putting Type Annotations to Work），後來GHC Haskell也借鑒了這一思想。不過這樣一來polymorphism就不再是免費午餐了，有性能損耗。

對於程序員，實際的用途：你在進行typed functional programming的時候，如果不是整天玩黑魔法而是老實寫業務代碼，那涉及的類型基本上不出HM的框架。熟悉一下總是好的。

想要自己擼一把Hindley-Milner type reconstruction的話，關門，放Oleg：http://okmij.org/ftp/Haskell/AlgorithmsH.html#teval

至於技能樹怎麼點。。今天累了，不放書單了。從wikipedia看起總是好的~

HM 是 System F 的一個子集，通過限制多態類型特化時只能使用簡單類型作為參數讓類型推導可行化，推導演算法就是大名鼎鼎的 Algorithm W。很多現代的函數式語言的類型系統都是它的擴展，比如允許子型多態的 OCaml 和帶有帶界量化的 Haskell。

這個說的很詳細了，簡而言之就是在SystemF裡面需要進行顯示的標註，而hindley/milner用一個type scheme的策略來實現多態。比如在Let ploymorphism(let x= t)中先對t進行unification，生成type scheme，以後用到t時就new instance。每次生成的instance不一樣，就不會產生衝突的constraint。從而實現多態。

推薦一本書 types and programming languages.

如果你只是個用Haskell寫業務的，那麼Hindley-Milner對你沒有任何用途。那個東西是一個類型系統，包含了類型推導的演算法。你多寫幾行Haskell，感受一下GHC是如何在你的程序只有表達式的情況下，幫你還原出每一個聲明的類型的。

你們說了一堆也沒說 HM 到底是個啥啊（

HM 就是這六個：

$[frac{x : sigma in Gamma}{Gamma vdash x : sigma}] [frac{Gamma vdash e_0 : au o au hspace{.1 extwidth} Gamma vdash e_1 : au}{Gamma vdash e_0 e_1 : au }] [frac{Gamma, x : au vdash e : au}{Gamma vdash lambda x.e : au o au}] [frac{Gamma vdash e_0 : sigma hspace{.1 extwidth} Gamma,x : sigma vdash e_1 : au}{Gamma vdash ext{let } x = e_0 ext{ in } e_1 : au}] [frac{Gamma vdash e : sigma hspace{.1 extwidth} sigma sqsubseteq sigma}{Gamma vdash e : sigma}] [frac{Gamma vdash e : sigma hspace{.1 extwidth} alpha otin free(,Gamma),}{Gamma vdash e : forall alpha.sigma}]$

從上往下分別是

Variable Access

Application

Abstract

Variable Declaration

Subtype

Type Generalize

下課了。。。

順便列個書（paper）單：

Jean-Yves Girard, Une Extension de l』Interpretation de Go ?del a`
l』Analyse, et son Application a` l』E ?limination des Coupures dans
l』Analyse et la The ?orie des Types, Proceedings of the Second Scan-
dinavian Logic Symposium, Amsterdam, pp. 63-92, 1971（是法語的）
John C. Reynolds, Towards a Theory of Type Structure, 1974
Hindley, R., The Principal Type-scheme of an Object in Combinatory
Logic, Transactions of the American Mathematical Society 146, 29-60,
1969

我是來安利 Scala 的

先說用途：

是用來甩鍋的，讓碼農可以偷懶，編譯器給我老實幹活去

val a = 1 + 2

val b = 2.5 + 3.5

val f1 : Int =&> Int = _ * 2

val f2 : Double =&> Double = _ * 2

然後你分別跑 f1(a), f1(b), f2(a), f2(b) 看看

頭兩句省了你聲明值的類型，有看起來是弱類型語言的寫法，後兩個function卻又對操作類型有限定，而這個類型限定的又不是一成不變，Int 會在 f2 隱式轉化成 Double，但這個轉換是單向的，就是說 Double 是不會被隱式轉化成 Int。既簡單，又合理。寫著也清爽。

說完用途，

說是什麼：

在類型理論和FP（注，沒有FOP這種東西）裡面，代碼既公式為主要思路導向。

所以，就必須有一套理論基礎去保障這個思路的可行性。

手段為

1. 類型限定：不可能所有的類型都能同時應用在同一公式上，如 a ／ 3 如果 a 是「ab」這是弄啥呢？

2. 公式描述：既然有類型的限制，那麼相關的類型應該有相關的應用，是有窮盡的。

兩條件間的融合過程為類型推倒，對就是那種推倒，融為一體...

這個時候你寫一個

val f3 = _ * 4 看看？

我覺得題主更想問的不是HM是啥，SystemF是啥，而是在問：類型推斷為什麼在FP里那麼重要？

FP的世界裡基本元素只有類型和標記，沒有值沒有對象沒有賦值，理想的FP程序架構應該是只維護一個global context 的 state machine 其他副作用由compiler、runtime來保證consistency

換句話說，程序就是一個狀態變換：類似解方程，這種架構暗示了內在的可證性：不需要真正運行代碼就能判斷是否自洽，這在工程上是有好處的。類型系統就是實現這種判斷的工具，HM只是其中一種叫做SystemF類型系統的具有良好實踐性的子集。

HM就是一種類型系統啦，最出名的就是它的類型推導演算法，不用程序員寫類型標註，還能能實現類型多態，不過有限制，只能是let-polymorphism，

入門的話可以看看EOPL第七章，裡面有介紹如何實現簡單的類型推導器，習題7.29也提及了algorithm W，再找找別的大學的ppt看看，寫代碼實現一下，就能有點感性認知了