Damas-Hindley-Milner (DHM) Type Inference (Reading Club 2026-Feb-11)

Simply Typed Lambda Calculus (STLC)

DHM Type System

• Polymorphic Types (polytypes)

Type Inference (Algorithm J)

• Substitution

• Universal Instantiation and Generalization in the Context of Types

  • delegate to CS2050

• Type Unification

• Inference

Algorithm W

• (convince yourself that W is sound) (4.2 or p. 367 of Milner 1978)

References

• Principal type-schemes for functional programs (Damas and Milner, 1982) shows that the algorithm does indeed find the most general type and that the problem is decidable.

• A Theory of Type Polymorphism in Programming (Milner, 1978) describes the original type system and inference algorithm (both primarily in Section 2).