Lab 7 · Hindley–Milner inference three ways (and ★ type classes by dictionary passing)¶

Chapter: 7 · Type Inference · Lessons: 7.1 (unification), 7.2 (Algorithms W, J, M), 7.3 (levels, value restriction, complexity), ★ 7.7 (type classes) · Time: 8–12 hours (5–7 without the ★ part) · Tests: ./course test 7 (label ch07; lab tests ch07.HM.* and ch07.lab.bench-smoke)

1. Goal¶

You write Hindley–Milner type inference for MiniML, a small ML with let-polymorphism, recursion, pairs, lists and references — three times:

Algorithm W (Lesson 7.2, Algorithm 7.2.7): substitutions returned and composed bottom-up;
Algorithm J with levels (Algorithm 7.2.8 + Lesson 7.3, Algorithm 7.3.2): one global union-find, updated in place, and generalization by comparing levels;
Algorithm M (Algorithm 7.2.9): top-down, every subterm receives the type its context expects.

All three must compute the same principal types on every well-typed program (with the value restriction), and W and J the same errors. Then you measure them on deeply nested lets, where W's substitution passing is quadratic and J with levels is near-linear. The ★ milestone adds an overloaded eq with type classes and translates programs to dictionary passing, run by the provided evaluator.

You design everything inside the algorithms: the type representation, substitutions, the union-find, environments, fresh-variable supply. The provided code (provided/) is the language: parser, printers, builtins, corpus reader, program generators and an evaluator.

2. MiniML (provided)¶

2.1 Syntax¶

e ::= n | true | false | () | x
    | fun x -> e                     extends as far right as possible
    | e1 e2                          application, left-assoc., binds tighter than operators
    | let x = e1 in e2
    | let rec f = fun x -> e1 in e2  the bound expression must be a fun
    | if e1 then e2 else e3
    | (e1, e2)                       pairs; (e) is just e
    | e1 + e2 | e1 - e2 | e1 * e2    left-assoc.; * binds tighter
    | e1 < e2 | e1 == e2             integers only; non-associative, lowest precedence

# starts a comment to the end of the line. Names are letters, digits, _ and ', not starting with a digit; keywords: fun let rec in if then else true false.

2.2 The tree and positions¶

A Program (include/hm/MiniML.h) is a vector of Expr nodes with integer child indices and a Root. Every node has a position (line, column; both from 1): the position of its first token, except that a binary operator node has the position of its operator and an application has the position of its function (its first token). Header lines of corpus files count as lines.

2.3 Types and their canonical spelling¶

τ ::= 'a | int | bool | unit | τ -> τ | τ * τ | τ list | τ ref

Results are compared as strings in canonical form (printType): type variables renamed 'a, 'b, … in order of first occurrence (left to right); -> right-associative and loosest; * non-associative and tighter (a product or arrow operand of * is parenthesized); list and ref postfix and tightest. Example: ('a -> 'b) -> 'a list -> 'b list. Build a TypeTerm (variables may have any name) and call printType.

2.4 Builtins¶

name	type	name	type
`fst`	`'a * 'b -> 'a`	`tail`	`'a list -> 'a list`
`snd`	`'a * 'b -> 'b`	`isnil`	`'a list -> bool`
`nil`	`'a list`	`ref`	`'a -> 'a ref`
`cons`	`'a -> 'a list -> 'a list`	`get`	`'a ref -> 'a`
`head`	`'a list -> 'a`	`set`	`'a ref -> 'a -> unit`

Every type variable of a builtin is universally quantified (builtins() returns them as TypeTerms). A user binding may shadow a builtin.

3. Requirements and contract¶

Implement in src/ (switch hm):

InferResult infer(const Program &P, Algorithm A);   // A = W, J or M

InferResult is std::expected<std::string, TypeError>: the canonical principal type of the whole program, or the first error the algorithm meets, with its kind and position. The message text is not tested.

3.1 Typing rules¶

HM with the value restriction (Lesson 7.2, Definition 7.2.4; Lesson 7.3, Definition 7.3.3): literals and () have their base types; + - * take two ints and give int; < and == take two ints and give bool; if needs a bool condition and branches of one type; fun binds a monomorphic parameter; let rec f = fun x -> e1 types the fun with f monomorphic inside, then generalizes; let x = e1 generalizes the type of e1 over the variables not free in the environment if e1 is a syntactic value (§3.4), and binds a monotype otherwise.

3.2 The three algorithms¶

W: Algorithm 7.2.7. Substitutions are values; every recursive call receives the environment with the substitution so far applied.
J: Algorithm 7.2.8 with levels (Algorithm 7.3.2). One mutable union-find over type nodes; the environment is never rewritten; generalization compares levels (no scan of the environment). A value-restricted let lowers its type's levels to the let's level.
M: Algorithm 7.2.9: M(Γ, e, ρ) with ρ the expected type; the initial call uses a fresh variable.

3.3 Error kinds and positions¶

kind	when	position reported
`Unbound`	a variable that is neither bound nor a builtin	the variable
`Mismatch`	two different type constructors must be equal	see below
`Occurs`	a variable must equal a type that strictly contains it	see below

Positions, W and J: an application's own unification (function type against argument -> result) at the application; a condition at the condition; the two branches of an if at the else branch; an operand of an operator at the operand; the recursive binding of let rec (its variable against the fun's type) at the fun. M: at the subterm whose own unification with its expected type fails — a literal, a variable (at its instantiation), a fun (against α → β), a pair (against α * β) or an operator (its result type) — in the order Algorithm 7.2.9 visits them. Unification is complete for the pair being unified before the error is reported, so the kind is Occurs exactly when the failing step is an occurs check.

3.4 The value restriction¶

A syntactic value is a variable, a literal, (), a fun, or a pair of values (isSyntacticValue). Only syntactic values are generalized. Example: let r = ref nil in … gives r the monotype t list ref, so its element type is fixed by the first use.

3.5 Observable behavior¶

On every well-typed program the three algorithms return the same canonical type.
On every ill-typed program W and J return the same error (kind and position); M returns an error too (possibly elsewhere).
No algorithm crashes or loops on any parsed program; J on letChain(4000) finishes within 2 s on the CI runner.

4. The corpus and the tests¶

corpus/*.mml, one program per file, with header lines:

header	meaning
`# type: τ`	the program is well typed; all three algorithms return `τ`
`# error-wj: L:C kind`	W and J fail with this position and kind
`# error-m: L:C kind`	M fails with this position and kind

Files 01–20 are well typed, 30–42 ill typed. The headers were computed by the independent Python oracle tools/course/lib/hm.py and are checked against it by tools/course/tests/test_ch07.py.

test	checks
`HM.Provided_*`	the provided parser, printers and evaluator (pass in the skeleton)
`HM.L1_W_Corpus`, `L2_J_Corpus`, `L3_M_Corpus`	every corpus header, per algorithm
`HM.L2_J_AgreesWithW_RandomPrograms`	W and J identical on 500 random programs (types and errors)
`HM.L3_M_AgreesWithW_OnTypes_RandomPrograms`	M succeeds exactly when W does, with the same types
`HM.L2_ValueRestriction`	non-values are not generalized
`HM.L2_Levels_EscapingVariables`	variables free in the environment are not generalized (`nestedLets(30)` and a hand example)
`HM.L2_J_DeepLetChain`	J on `letChain(4000)`: correct type, under 2 s
`HM.L1_PairTower_ExponentialType`	`pairTower(6)`'s type has 64 arrows (W and J)
`HM.L5_*` (★)	§6
`lab.bench-smoke`	`ch07-hm-bench --quick` runs and the three algorithms agree

5. Measurement (L4)¶

ch07-hm-bench (provided, tools/bench.cpp) runs W, J and M on three families of provided/MiniML.cpp — letChain(n) (let x1 = fun y -> y in let x2 = x1 in …), nestedLets(n) (every let inside a fun, so the environment holds a monomorphic variable) and pairTower(n) (Lesson 7.3's exponential family) — prints the median of three runs in milliseconds, and exits 1 if the algorithms disagree. Fill in:

family	n	W ms	J ms	M ms
letChain	1000
letChain	2000
nestedLets	2000
pairTower	14

The reference solution (RelWithDebInfo, the course container) prints 58 / 0.54 / 153 ms and 286 / 0.87 / 818 ms for letChain 1000 and 2000, 1036 / 1.95 / 2782 ms for nestedLets 2000, and 672 / 470 / 742 ms for pairTower 14 (Lesson 7.2 §8). Explain the ratios between consecutive sizes.

6. ★ Type classes by dictionary passing (L5)¶

Implement in classes/ (switch hm-classes) the contract of include/hm/Classes.h:

std::expected<Elaboration, ClassError> elaborate(const Program &P);

MiniML gains one overloaded builtin, eq : Eq 'a => 'a -> 'a -> bool, and the instances Eq int, Eq bool, Eq unit, Eq 'a => Eq ('a list), (Eq 'a, Eq 'b) => Eq ('a * 'b) — none for functions or references.

6.1 Inference¶

Algorithm J with levels and the value restriction, where every use of eq (and of any let-bound name whose scheme has constraints) creates an Eq predicate. At a generalizing let (and at the top level), reduce the predicates created in its right-hand side by the instances (Algorithm 7.7.4) to predicates on type variables; a variable this let generalizes becomes a dictionary parameter of the binding, in the order its variable first occurs in the binding's type. Elaboration::Type is printQualified(constrained variables, type), e.g. Eq 'a => 'a -> 'a -> bool.

6.2 Translation¶

Elaboration::Translated is a plain MiniML program (no eq) that evaluate runs: each eq becomes its dictionary (eqInt, eqList eqBool, a parameter, …) — for the one-method class Eq, the dictionary is the method —; each constrained let becomes fun _d1 -> … -> e1 and each use of it applies the dictionaries; a top-level constraint becomes a leading fun parameter. Parameter names are free as long as they do not clash with user names.

6.3 Errors¶

kind	when	position
`Type`	a plain inference error	as J (§3.3)
`NoInstance`	a predicate on a function or reference type	the `eq` (or constrained name) that created it
`Ambiguous`	a predicate on a variable that the generalized type does not mention	the `eq` that created it

corpus-classes/*.mml has # qtype: and # value: headers (well typed: the qualified type and the value of the translation) or # error: L:C kind (type, no-instance, ambiguous); HM.L5_Classes_Corpus checks them, and HM.L5_Classes_TranslationHasNoEq checks that no eq is left.

7. Milestones¶

#	milestone	command
L1	W: literals, `fun`, application, `let` with generalization, then the rest	`./course test 7 -R 'HM.L1'`
L2	J with levels; the value restriction in all algorithms	`./course test 7 -R 'HM.L2'`
L3	M	`./course test 7 -R 'HM.L3'`
L4	measure	`build/<preset>/bin/ch07-hm-bench`
L5 ★	type classes	`./course test 7 -R 'HM.L5'`

Before you start, every ch07.HM.* test except Provided_* fails with TODO(ch07): L1-L3: … (L5: TODO(ch07): L5 (★): …).

8. Hints¶

Hint 1 — where to start

Write W first with the simplest representation: a type is a tree (variable number or constructor with arguments), a substitution a map from variable numbers to types, an environment a list of (name, scheme). Get fun x -> x and let id = fun x -> x in (id 1, id true) right, then add the remaining forms one by one. The builtins are schemes whose variables are all quantified: convert each TypeTerm once.

Hint 2 — the key idea for J

In J a type variable is a node that may be linked to another node; find follows links. Nothing is ever substituted into the environment: whenever you look at a type, dereference it. Give each variable node a level; let increments the current level while inferring its right-hand side; binding a variable to a type lowers every variable in that type to the variable's level (do it in the occurs check); generalization marks the variables whose level is still greater than the current one as generic. Instantiation copies generic nodes and shares the rest.

Hint 3 — M and error positions

M is W with the unification moved to the leaves: each case first unifies the expected type with the shape it has (α → β for fun, int for a literal, …), then recurses with the parts. The test headers tell you where each error must be reported; when a test fails, print the unification that failed and compare with the rule in §3.3.

Hint 4 — ★ dictionaries

Record each predicate with the node that created it. At a let, after inferring the right-hand side, reduce its predicates: a list or pair type splits into its components, int/bool/unit disappear, a function or reference is an error, a variable stays. The variables that this let generalizes and that remain in predicates become parameters. Build the translated program as text and parse it with parseProgram: dictionaries are expressions like (eqList eqInt).

9. Stretch goals¶

Report both W's and M's error position for the corpus's ill-typed programs, and compare them with where you would fix the program (Lesson 7.9).
Add Ord with lt, and the superclass Eq (a dictionary for Ord contains one for Eq).
Implement Algorithm 7.9.5's minimal unsatisfiable subsets for let-free programs and report the minimum error source.