Flashcards — Chapter 7¶
78 cards. Review them with spaced repetition in the terminal (./course flash 7) or export them to Anki (./course flash export 7). Here, click a card to reveal its back.
robinson¶
What is a most general unifier (MGU)?
A unifier θ of E such that every unifier θ' of E is θ' = ρθ for some ρ. Unique up to renaming (Definition 7.1.3).
Robinson's algorithm in one sentence
Repeatedly take the leftmost-outermost disagreement pair of the first unsolved equation; fail on two different symbols or an occurs check; otherwise compose [x ↦ t] onto θ (Algorithm 7.1.7).
Robinson: termination measure and complexity
Each step removes a variable from θE for good, so ≤ |vars(E)| steps; but with tree-shaped substitutions the MGU itself can be exponential (x_i = f(x_{i-1}, x_{i-1})).
martelli-montanari¶
The six Martelli–Montanari rules
delete t=t; decompose f(s̄)=f(t̄); conflict f≠g; swap t=x; check x=t with x∈vars(t); eliminate x=t (substitute x everywhere, keep x=t solved).
What is solved form and why does it matter?
Equations x_i = t_i with distinct x_i not occurring in any t_j; its substitution is an idempotent MGU (Lemma 7.1.5).
Martelli–Montanari termination measure
Lexicographic (unsolved variables in the worklist, total size of worklist terms, number of t = x equations): eliminate lowers the first, delete/decompose the second, swap the third.
union-find-unification¶
Union-find unification: the key idea
Represent each term once as a graph node; keep classes of nodes known equal; merge classes (union before pushing argument pairs) instead of substituting; check cycles at the end (Algorithm 7.1.10).
Union-find unification complexity
O(N α(N) k): ≤ N−1 unions, each pop two finds, plus one DFS for the occurs check. Linear on the family that is exponential for Robinson.
Where is union-find unification in production?
OCaml's Ctype.unify (link_type), rustc's ena tables (separate int/float tables), GHC's meta variables, Swift's solver; LLVM's generic union-find is EquivalenceClasses.
occurs-check¶
Why does x = f(x) have no finite solution?
For any θ, θx is a proper subterm of θf(x), so |θf(x)| > |θx| (Lemma 7.1.18).
Eager vs deferred occurs check
Eager: test x ∈ vars(t) at every binding, O(N²) total. Deferred: one DFS for a cycle in the class graph at the end, O(N) (Algorithm 7.1.12).
What does OCaml's -rectypes do?
Skips the occurs check and accepts rational (cyclic) solutions: fun x -> x x : ('a -> 'b as 'a) -> 'b.
let-polymorphism¶
What is let-polymorphism?
let-bound variables get type schemes ∀ᾱ.τ generalized over variables not free in Γ; each use instantiates them freshly. λ-bound variables stay monomorphic.
Why is fun f -> (f 1, f true) untypable in HM?
f is λ-bound: one monotype τ1, which would have to equal both int → τ and bool → τ' (Proposition 7.2.10).
Principal type (Damas–Milner)
A typing of which every other typing is a substitution instance; every typable HM program has one and W computes it (Theorem 7.2.11).
algorithm-w¶
Algorithm W: what does each call return?
A pair (θ, τ): a substitution and a type with θΓ ⊢ e : τ. At e1 e2: W(e1), W(θ1Γ, e2), unify θ2τ1 with τ2 → β, compose.
Where does W report an error in e1 e2?
At the application, when unifying the function's synthesized type with argument → result fails.
Why is W quadratic on nested lets?
It applies its substitution to the whole environment and scans it for ftv at every let: Θ(n) per let, Θ(n²) for letChain(n).
algorithm-j¶
Algorithm J vs W
Same unifications in the same order, but one global union-find updated in place; Γ is never rewritten; types are dereferenced when read (Theorem 7.2.12).
Algorithm J's invariant
The global substitution only grows; at each call it equals W's composed substitution so far.
J in production
OCaml (typing/ctype.ml), SML/NJ, GHC's meta variables, rustc's InferCtxt — every production HM is J.
algorithm-m¶
Algorithm M in one line
M(Γ, e, ρ) returns θ with θΓ ⊢ e : θρ; the expected type ρ is pushed into every subterm and unified at the leaves (Lee & Yi 1998).
Why does M report errors earlier than W?
The context's expectation is imposed as soon as a subterm is entered, so the first contradicting leaf fails (fun f -> (f 1, f true): W at 1:16, M at 1:18).
Where is M-style inference in real compilers?
OCaml's type_expect ('because it is in the condition of an if-statement'), GHC's ExpRhoType in tcApp.
levels¶
What is a level in HM inference?
The let-depth at which a type variable became reachable from Γ; fresh variables get the current level, unification lowers levels, generalization takes variables with level > current (Rémy 1992).
Why lower levels when binding α := t?
Variables of t become reachable wherever α is; if α is in Γ they must not be generalized by an inner let (Lemma 7.3.7).
Levels: cost
O(|τ|) per let (only the generalized type is visited); lowering rides on the occurs check. Lab: J 0.87 ms vs W 286 ms on letChain(2000).
value-restriction¶
The value restriction
Generalize a let only if its right-hand side is a syntactic value (variable, literal, fun, tuple of values) — Wright 1995.
Why is let r = ref (fun x -> x) unsafe to generalize?
Two instances share one cell: store an int -> int, read it at bool -> bool, add 1 to true (Proposition 7.3.9).
How to recover polymorphism lost to the value restriction?
η-expand: let g = fun z -> f f z (a fun, hence a value). OCaml prints the weak variables as '_weak1.
hm-complexity¶
Complexity of HM typability
DEXPTIME-complete (Mairson; Kfoury–Tiuryn–Urzyczyn 1990); nearly linear for bounded let-depth and type size (McAllester 2003).
The pair tower
let x0 = fun z -> z in let x1 = (x0, x0) in … xn: principal type with 2^n arrows (Proposition 7.3.12).
A doubly exponential printed type
f0 = fun x -> (x, x); f_i = fun y -> f_{i-1} (f_{i-1} y): 2^(2^n) leaves; OCaml prints f4's type as 565 261 characters.
hm-x¶
HM(X) in one sentence
HM parameterized by a constraint system X: judgments C, Γ ⊢ e : τ and schemes ∀ᾱ. C ⇒ τ; sound for every X, principal types when X has principal solutions.
Generate then solve
Emit all constraints of the program (let-constraints solved once per let), then solve by rewriting: equalities by unification, predicates by X's rules (Algorithm 7.4.4).
Pebble's literals as HM(X)
X = Num with Num(int), Num(float): each integer literal is ν with Num ν; unsolved ν default to int.
outsidein¶
What is an implication constraint?
∀ā. (Q_g ⊃ W): wanteds W to solve under givens Q_g (from a GADT match or a signature) with skolems ā.
Untouchable variable
A unification variable from an outer level inside an implication; OutsideIn will not assign it there, because the givens could make several assignments valid.
Why do GADT matches lose principal types?
test (IsZero t) = True has types Term a -> Bool and Term a -> a, neither an instance of the other (Proposition 7.4.10).
swift-solver¶
Swift's constraint kinds
Bind/Equal, conversions, conformance (literal protocols with defaults), and disjunctions — one alternative per overload.
Why can Swift type checking be exponential?
Overload resolution with generics is NP-hard (3-SAT reduction, Proposition 7.5.6); search over disjunctions explores ∏ k_i states per component.
Swift's mitigations
Split the constraint graph into components; favor likely overloads; score solutions; abort with 'unable to type-check this expression in reasonable time' past the limits.
rust-inference¶
Rust's inference scope
One function body: HM-style unification without generalization; signatures are written.
Rust integer literal fallback
{integer} variables unify only with integer types; unresolved ones become i32 ({float}: f64) in fallback.rs.
When does rustc report E0282?
A general type variable (not an int/float literal variable) is still unresolved at the end of the body: 'type annotations needed'.
kotlin-inference¶
Kotlin's inference scope
The declaration (and the call): val n = 1 fixes n : Int immediately; later uses cannot change it.
Builder inference
For buildList { add(1) }, the element type E is postponed during the lambda, constrained by the calls on the receiver, then fixed (List<Int>).
Kotlin integer literal typing
An integer literal takes an expected integer type (val l: Long = 1) but is never a Double.
typescript-inference¶
TypeScript widening
let x = 1 declares number (widened); const x = 1 keeps the literal type 1.
Evolving array
let acc = []; acc.push(1); acc.push('s') — the array's element type is the union of what flows in: (string | number)[].
Does tsc infer a parameter's type from its uses?
No: without a contextual type it is implicitly any (TS7006 under --strict).
pebble-inference¶
Pebble's inference mode (§8.9)
Integer literals get numeric variables (int or float), unannotated let/var take the initializer's type, equalities are unified eagerly, undecided variables default to int at the end of each function.
Conservative extension (Theorem 7.6.11)
Every program Chapter 6 accepts is accepted by inferTypes with the same type table; more are accepted (let z = y * 2 with y a float).
E0416
A unification fails on the type of an inferred binding whose variable was decided earlier and a fresh variable would fit: report at the use, note at the constraint that decided it.
instance-resolution¶
What is evidence for a class constraint?
A dictionary: a parameter for C α, or an instance function applied to evidence for its context, e.g. eqList (eqPair eqInt eqBool).
Instance resolution algorithm
Match the predicate's type against instance heads, instantiate the context, resolve each premise recursively; variables become dictionary parameters or ambiguity errors.
Why does resolution terminate in Haskell 98?
Instance heads are constructors over distinct variables and contexts mention only those variables, so recursive calls are on strictly smaller types.
coherence¶
Coherence
Every closed constraint has at most one evidence term, so meaning does not depend on the solver's choices.
How does Rust enforce coherence?
Orphan rule (trait or type must be local; E0117) plus an overlap check of impl heads by unification (E0119).
When do two instances overlap?
When their heads unify after renaming apart: C [a] and C [Int] overlap.
dictionary-passing¶
Dictionary passing
Each constraint becomes an extra run-time parameter; one compiled copy; method calls are indirect (GHC Core: member = \@a $dEq …).
Monomorphization
One copy per instantiation reached from the entry points (rustc_monomorphize's collector); direct calls, larger code.
Specialization in GHC
SPECIALIZE pragmas or automatic specialization create monomorphic copies and rewrite calls with rules ('SPEC member').
higher-rank¶
Rank of a type
Monotypes 0; ∀ at the top 1; each polymorphic type left of an arrow adds 1: (∀a. a → a) → Int has rank 2.
How is rank-N checked?
With annotations, bidirectionally: skolemize the expected polymorphic type and check the argument against it; skolems must not escape.
Why annotations for rank 2?
Without them there is no principal type in HM's sense (Proposition 7.8.6).
impredicativity¶
Impredicative instantiation
Instantiating a type variable with a polymorphic type, e.g. head at b := ∀a. a → a.
Quick Look
Before checking an application, look at the arguments with known types to find instantiations forced to be polymorphic; stay predicative otherwise (GHC ≥ 9.2).
Why no full System F inference?
Typability and type checking in System F are undecidable (Wells 1999).
traversal-blame¶
Blame by traversal order
Report the first unification that fails in the algorithm's order; free, but order-dependent and biased (McAdam).
Does first-failure blame lie in an MUS?
Yes, the reported constraint is in some MUS; but it need not be a minimum error source (Proposition 7.9.7).
W vs M blame on the same program
W blames the application where synthesized types clash; M the leaf that contradicts the expected type.
mus-localization¶
Minimal unsatisfiable subset (MUS)
A conflicting set of constraints each of which is needed for the conflict; an error slice (Haack & Wells).
Minimum error source
A smallest set of locations hitting every MUS; removing its constraints makes the program typable (Lemma 7.9.3).
Deletion-based MUS
Drop each constraint in turn if the rest stays unsatisfiable: m satisfiability checks (Algorithm 7.9.5).
provenance¶
Provenance notes
Record, for each binding of a type variable, the constraint (location) that caused it, and cite it in errors.
Examples of provenance in compilers
rustc 'expected due to this', GHC 'arising from a use of …', OCaml 'because it is in the condition of an if-statement', Pebble's E0416 note.
What does Pebble's E0416 note point at?
The use or operator that first decided the inferred binding's type.