Chapter 7 exercises¶

You rebuild Pebble's type checker on unification: integer literals and unannotated let/var get numeric type variables that any later use in the function body may decide, with int as the default (pebble-spec §8.9). The result accepts every program Chapter 6 accepts, with the same types, plus programs like let y = 1.5; let z = y * 2;, and reports conflicts on inferred bindings as E0416 with a note at the use that decided them. In the lab you implement Hindley–Milner inference for MiniML three ways (Algorithms W, J with levels, M), compare them, and ★ add type classes by dictionary passing.

The contract is one function of pebble/include/pebble/Sema/Infer.h: inferTypes(ModuleDecl*, ASTContext&, DiagnosticEngine&), with the postconditions of Chapter 6's typeCheck (a type on every declaration and expression, MemberExpr fields, the diagnostics of pebble-spec §13.3) and the rules of §8.9. pebblec keeps using typeCheck; the Chapter 7 tool ch07-infer runs your inferTypes and prints the same table as ch06-typecheck (§14.4).
Your code goes anywhere under pebble/lib/Sema/Infer/src/ (switch infer). It starts with a Stub.cpp whose function stops with TODO(ch07): E1-E4: implement type inference by unification (inferTypes).
Provided: everything Chapter 6 had (lexer, parser, names; build with -DPEBBLE_USE_SOLUTION=lexer,parser,names if you skipped them), the diagnostic E0416 and the note note_inferred_here, the tool ch07-infer, and the corpus tests/ch07/Inputs/. The Chapter 6 goldens tests/ch06/Inputs/*.typed are your goldens too (E1).
The lab is specified in labs/ch07-hm/SPEC.md (contracts include/hm/MiniML.h, ★ include/hm/Classes.h; milestones L1–L5); this page only orders it.

./course test 7                                                  # builds, then runs every test labelled ch07
ctest --preset linux -L '^ch07$' -R 'Infer.E2'                   # one group while iterating (macOS: --preset macos)
build/linux/bin/ch07-infer tests/ch07/Inputs/literals.pbl        # your type table and diagnostics
build/linux/bin/ch07-hm-bench                                    # the lab's measurement (L4)

Before you start, every ch07.Infer.* test and ch07.lit fail with TODO(ch07): E1-E4: …, and every ch07.HM.* test except Provided_* with TODO(ch07). The goldens tests/ch07/Inputs/*.typed were produced by the reference checker and cross-checked against the independent Python oracle tools/course/lib/pebble_infer.py (generate all constraints, then solve; tests/ch07/update_goldens.py); the expected diagnostics of err-infer.pbl were written by hand from §8.9.

Stuck? Work through the hints in order. The reference solution is in solutions/pebble/lib/Sema/Infer/src/ (one possible design: Chapter 6's checker with a Solver class for numeric variables); look at it only after you pass the tests, or after an honest hour.

E1 · A checker whose types may contain variables¶

Contract: inferTypes · Spec: pebble-spec §8.9 (first two bullets), §14.4 · Tests: ch07.Infer.E1_*, lit conservative.test · Lessons: 7.1, 7.6

Start from a checker equivalent to Chapter 6's (your own typeCheck, copied into this directory under a namespace of its own, or written anew): declarations, synthesis and checking modes, calls, references, places, every §13.3 diagnostic. Then change its type representation so that a type can be a numeric variable (or an array whose element contains one), and delay writing types into the AST until the function body is finished: record each expression's type during the walk and write the solved types at the end. With every integer literal still typed int or float as in Chapter 6, all Chapter 6 goldens must come out unchanged — that is the test E1_ReproducesEveryChapter6Table.

Hint 1 — where to start

Copy your Chapter 6 files and rename the namespace (the two libraries are linked into the same test binaries, so two pebble::types::Checker classes would clash). Make it pass E1_ReproducesEveryChapter6Table before introducing variables: that checks the copy.

Hint 2 — the key idea

You need a type that is either a const Type *, a variable, or an array of something that is not yet concrete (let a = [1, 2]; is [ν; 2]). Everything that stores types during the walk (bindings of let/var, recorded expression types, reference arguments) stores this new type; only the final write-back converts it.

E2 · Literals and bindings decided by unification¶

Contract: inferTypes · Spec: §8.9 (bullets 1–3) · Tests: ch07.Infer.E2_*, lit literals.test, lets.test · Lessons: 7.1 (union-find), 7.4, 7.6

Give every integer literal a fresh numeric variable and every unannotated let/var its initializer's type. Replace each "the two types must be equal" of Chapter 6 by unification, solved immediately: a variable meeting int or float is bound to it, two variables are merged, anything else fails (and reports the Chapter 6 error). Operands of &+ &- &* << >>, indices and for bounds unify with int; an operand of & | ^ that is still a variable becomes int; casts and print do not decide a variable. At the end of each function body, bind every remaining variable to int and write the types.

Hint 1 — where to start

let y = 1.5; let z = y * 2; is the first test to make pass: the literal's variable meets float at the *. Then let n = 1; let x: float = n;: the variable meets float in checking mode, three lines after the literal.

Hint 2 — the key idea

A union-find over variable numbers, where each root remembers the concrete type it is bound to (or none). Arrays need one more case in unification (same length, unify the elements). The checking forms of §8.1 still push expected types down: a literal checked against float simply unifies its fresh variable with float.

Hint 3 — a design sketch

Solver { vector<int> parent; vector<const Type*> bound; vector<SourceRange> origin; vector<ArrayNode> arrays; } with fresh, resolve, unify(a, b, where), defaultAll, zonk. Make unify check before it commits, so that a failing unification binds nothing (the next error must not see half a unification).

E3 · E0416: conflicts on inferred bindings¶

Contract: inferTypes · Spec: §8.9 (last bullet) · Tests: ch07.Infer.E3_*, lit err-infer.test · Lessons: 7.9

When a unification fails and one side is the type of a name bound by an unannotated let/var whose type held a variable at its declaration, that variable was decided by an earlier constraint, and a fresh variable in its place would have unified, report E0416 at the name instead of the Chapter 6 code, with the note "'x' is inferred to have type 'T' because of this" at the constraint that decided the variable (the checked expression, or the operator). Every other failure keeps its Chapter 6 code.

Hint 1 — where to start

Record, when a variable class is bound, where (the range passed to unify). Remember, for each unannotated binding, which class its type contained.

Hint 2 — the key idea

"Would a fresh variable have unified?" is a dry run of unification in which one class is treated as unbound. n == true with n inferred as int is not E0416: no numeric variable can be a bool.

E4 · Robustness and the lab¶

Contract: inferTypes, hm::infer, ★ hm::elaborate · Tests: ch07.Infer.E4_*, ch07.HM.*, ch07.lab.bench-smoke · Lessons: 7.2, 7.3, ★ 7.7

inferTypes must run on every input of tests/ch04–tests/ch07 that resolves, without crashing, and leave no expression untyped when it succeeds. Then do the lab: labs/ch07-hm/SPEC.md milestones L1–L4, and ★ L5.

Hint 1 — where to start

Error recovery is Chapter 6's: an ill-typed expression gets <error>, which unifies with everything and binds nothing. Make sure an expression whose recorded type contains a variable that is never bound (because an error stopped the walk) still gets a type — defaulting covers it.

Hint 2 — the lab

Follow the SPEC's milestones in order; W first, because its proofs (Lesson 7.2 §4) tell you exactly what each case must return. The SPEC's hints cover J's levels and the ★ dictionaries.