How to Choose Between Hindley-Milner and Bidirectional Typing
9 days ago
- #type-systems
- #generics
- #programming-languages
- The choice between Hindley-Milner (HM) and Bidirectional (Bidir) type systems is a common dilemma for new programming language developers.
- The question should not be framed as a choice between HM and Bidir, but rather whether the language needs generics, as this determines the need for unification.
- Unification is central to HM and is necessary for generics, allowing type variables to be solved (e.g., Rust's `Vec<T>`).
- Bidirectional typing can work without unification, relying on annotations, but it can also incorporate unification, making it a superset of HM.
- Adding a `check` function to an HM system can easily make it bidirectional, with minimal code changes.
- Generics are essential for general-purpose languages but may add unnecessary complexity for learning exercises or domain-specific languages (DSLs).
- The decision to include generics should guide the choice of type system, with bidirectional typing offering flexibility for both scenarios.