Hindley-Milner tip çıkarımı, lambda hesabına dayanan fonksiyonel dillerin temel taşını oluşturur. Bu sistemde her ifadenin tipi, programcı tarafından açıkça belirtilmeden otomatik olarak hesaplanabilir. Algoritmanın kalbinde Robinson'ın unifikasyon prosedürü yatar: iki tip terimi verildiğinde, onları özdeş kılan en genel substitüsyonu bulmak. Tip değişkenleri α, β, γ sembolleriyle gösterilir ve substitüsyon σ bir değişkenden tipe olan bir eşleme olarak tanımlanır. Algoritma W olarak bilinen çıkarım prosedürü şu adımlarla ilerler: Bir değişken x ile karşılaşıldığında, ortam Γ'dan x'in tip şemasını al ve taze tip değişkenleriyle örneklendir. Bir lambda soyutlaması λx.e için taze bir α değişkeni yarat, x'i α ile ortama ekle, e'yi çıkar, sonuç tipini α → τ olarak oluştur. Bir uygulama (e1 e2) için e1 ve e2'yi bağımsız çıkar, taze β yarat, σ = unify(τ1, τ2 → β) hesapla, σ'yı tüm bilgi üzerine uygula. Let polimorfizmi Hindley-Milner sisteminin en kritik özelliğidir. let x = e1 in e2 kuralında, e1'in tipi genelleştirilerek bir tip şeması oluşturulur: ∀α1...αn.τ biçiminde. Burada αi'ler τ içinde serbest geçen ama ortamda bağlı olmayan değişkenlerdir. Bu genelleştirme adımı olmadan polimorfik fonksiyonların farklı tip argümanlarıyla kullanılması mümkün olmazdı. Hindley-Milner tip çıkarımı DEXPTIME-complete olmakla birlikte, pratik programlarda polinom zamanda çalışır. Tip çıkarımının başarısız olduğu durum, birleştirme sırasında döngüsel bir denklem ortaya çıkmasıdır: α ~ List α gibi. Oluşum kontrolü (occurs check) bu patologik durumu yakalar. ML, Haskell ve OCaml ailesi diller bu sistemin üzerine inşa edilmiş olup, güçlü statik güvenceleri sıfır tip anotasyonuyla birleştirmelerini sağlayan temel mekanizma budur.