Flashcards — Chapter 6¶
77 cards. Review them with spaced repetition in the terminal (./course flash 6) or export them to Anki (./course flash export 6). Here, click a card to reveal its back.
judgments¶
Typing judgment Γ ⊢ e : τ — what do the three parts mean?
Under context Γ (types of the free variables), term e has type τ. A judgment is derivable iff some finite tree of rule instances has it at the root (Definition 6.1.4).
What makes a rule system syntax-directed (Definition 6.1.5)?
Exactly one rule per term form, and every premise is about an immediate subterm. Then the derivation is determined by the term and checking is one recursive pass (Algorithm 6.1.6).
Why does subsumption break syntax-directedness?
Γ ⊢ e : σ, σ <: τ ⟹ Γ ⊢ e : τ applies to every term form, so a checker would have to guess where to use it; the algorithmic system builds it into the elimination rules instead (Lesson 6.5).
Uniqueness of types (Theorem 6.1.10) — statement and why it holds.
In Figure 6.1.1, Γ ⊢ e : τ and Γ ⊢ e : τ' imply τ = τ'. By induction: one rule per form, λ carries its parameter type.
safety¶
Progress (Theorem 6.1.13).
If ∅ ⊢ e : τ then e is a value or e → e' for some e'. Key lemma: canonical forms.
Preservation (Theorem 6.1.16).
If ∅ ⊢ e : τ and e → e' then ∅ ⊢ e' : τ. Key lemma: substitution (for E-Beta and E-LetV).
Stuck term (Definition 6.1.8).
A closed normal form that is not a value, e.g. true + 1 or 3 4. Safety = no well-typed term reaches one.
Adding the rule 'if true then t2 else t3 → t3' to the arithmetic language breaks which theorem?
Neither: both branches have the if's type, and no new normal form appears. Nondeterminism alone does not break safety.
static-dynamic¶
Why is every sound static type checker conservative?
'Can get stuck' is undecidable for a Turing-complete language (Theorem 6.2.2, reduction from halting), so a decidable sound checker must reject some safe programs.
Where does a dynamically checked language test tags (Algorithm 6.2.4)?
At elimination forms: application, arithmetic and comparison operands, if conditions. Introductions and variables never fail.
Dynamic typing as static typing with one type (Definition 6.2.3)?
Every term has type dyn; values carry tags; each primitive checks tags and raises a trapped error on mismatch.
strong-weak¶
Trapped vs untrapped error (Cardelli).
Trapped: execution stops in a defined way (exception). Untrapped: continues with an arbitrary result (C undefined behavior). A safe language has no untrapped errors.
JavaScript: "5" - 1 and "5" + 1?
4 and "51": - converts to numbers, + concatenates when either operand is a string — two coercion tables for similar symbols.
Two ways a language is weakly typed (Definition 6.2.5).
Untrapped errors (C: out-of-bounds, type punning) or silent conversions between unrelated types (JavaScript's +).
soundness¶
Sound for a set of errors W (Definition 6.2.7).
No well-typed program can produce an outcome in W. 'Intentionally unsound' = the spec documents accepted programs that do.
How does Java keep covariant arrays sound?
Every array records its run-time element type and each store checks the value's class (Algorithm 6.2.8), throwing ArrayStoreException.
Three documented unsound features of TypeScript.
any; bivariant method parameters; covariant arrays (plus unchecked index access without noUncheckedIndexedAccess).
syntax-directed¶
The error type (Definition 6.3.2): what rule do checks follow?
<error> is compatible with every type: no rule reports a mismatch, bad operand or argument when a type involved is <error>. One report per mistake (Proposition 6.3.9).
Cost of never reporting cascades?
Independent errors whose types flow through an <error> value are hidden until the first one is fixed.
In which order does syntax-directed synthesis complete node types?
Post-order, left to right: children before parents. The first error found is the leftmost innermost.
Clang function that decides the C assignment premise?
Sema::CheckAssignmentConstraints (clang/lib/Sema/SemaExpr.cpp).
conversions¶
C usual arithmetic conversions for int and unsigned int?
Equal rank, one unsigned → unsigned int. So -1 < 1u is false (-1 becomes 2^32 − 1).
C: long + unsigned int on LP64?
long: higher rank and able to represent every unsigned int value.
Pebble's only implicit conversion?
An integer literal checked against float denotes the float value (pebble-spec §8.1). let n = 1; let x: float = n; is E0401.
Coercion vs subtyping semantics.
Coercion inserts a conversion function (changes representation); subset semantics reuses the value. Coherence: every derivation must insert equivalent conversions.
overloading¶
C++ ICS ranks, best to worst.
Exact match (incl. lvalue transformations, qualification), promotion, conversion; then user-defined, then ellipsis.
Why is f(1, 2) ambiguous with f(int, double) and f(double, int)?
Each candidate is better on one argument and worse on the other; a best viable function must be at least as good on every argument and better on one.
Java's three overload phases.
1: subtyping/widening only; 2: plus boxing/unboxing; 3: plus varargs. A later phase runs only if the earlier found nothing: m(1) with m(long), m(Integer) picks m(long).
bidirectional¶
The two judgments of bidirectional typing.
Γ ⊢ e ⇒ τ (synthesize: τ is output) and Γ ⊢ e ⇐ τ (check: τ is input).
Pfenning's recipe for modes.
Introduction forms check (λ, records, literals in Pebble); elimination forms synthesize (application, projection); annotations switch check → synth; the mode switch compares a synthesized type with the expected one.
Why can an unannotated λ be the argument of f but not the function in an application?
The argument is checked against f's parameter type (→I⇐ gets the parameter type); the function position synthesizes, and λx.e cannot synthesize without x's type.
rustc's representation of checking mode?
Expectation::ExpectHasType(ty) in rustc_hir_typeck; NoExpectation is synthesis; check_expr_with_expectation is the entry point.
local-inference¶
Local type inference (Pierce–Turner) solves type arguments from…
…the call's own arguments and expected type only (matching, no global unification). Unconstrained variables: 'cannot infer'.
Why defer unannotated λ arguments in Algorithm 6.4.6?
Their parameter types come from type variables solved by other arguments; checking them first would need a guess.
map(xs, fn x => x + 1) with xs : [int]?
α ↦ int from xs; then the deferred λ's body synthesizes int, β ↦ int; result [int].
subtyping¶
Function subtyping rule.
S1 → S2 <: T1 → T2 iff T1 <: S1 (parameters contravariant) and S2 <: T2 (results covariant).
Record subtyping: width, depth, permutation.
More fields is a subtype (width); each common field a subtype (depth); order irrelevant. The algorithm fuses all three: for each label of T, S has it with a subtype.
Why no transitivity rule in the algorithm?
It is admissible (Lemma 6.5.11); with it the checker would have to guess an intermediate type. Without it the recursion is on smaller types: termination (Theorem 6.5.12).
Top and bottom.
Every type <: top; bot <: every type. bot is the type of a diverging expression (never in TypeScript).
variance¶
Polarity of X in m(f: X -> int).
Positive: parameter (−) of a parameter (−).
Why must a mutable container be invariant?
Reading needs covariance and writing contravariance; with both, only equality is safe (Java arrays show the covariant hole).
Declaration-site vs use-site variance.
Declaration-site: the class declares +X/-X (Scala, Kotlin out/in, C#) and the checker verifies its members. Use-site: each use chooses (Java ? extends / ? super).
nominal-structural¶
Nominal vs structural subtyping.
Nominal: only declared relations (extends/implements). Structural: compatible shapes suffice (TypeScript, Go interfaces, OCaml objects).
How does TypeScript simulate a nominal type?
Branding: add a phantom field of a unique literal type so otherwise equal shapes differ.
How does HotSpot test a primary-superclass relation in O(1)?
Each class stores its superclasses at fixed depths (a display); x instanceof B loads slot depth(B) and compares (Click & Rose 2002).
occurrence-typing¶
Occurrence typing judgment (Definition 6.6.2).
Γ ⊢ e : τ ; ψ+ | ψ− — the proposition that holds if e evaluates to true, and the one if false. Branches are checked in Γ refined by ψ+ and ψ−.
Else-proposition of e1 && e2.
ψ1− ∨ (ψ1+ ∧ ψ2−): the first test failed, or it passed and the second failed.
After isinstance(x, int) and x > 0 fails, can x still be int?
Yes: isinstance may have passed and x > 0 failed. mypy shows int | str.
narrowing¶
Narrow(g1 || g2, S).
(T1, F1) = Narrow(g1, S); (T2, F2) = Narrow(g2, F1); return (T1 ∪ T2, F2).
typeof x === "object" narrows a primitive union to…
null — JavaScript's historical quirk (and objects).
What makes a variable stable for a Kotlin smart cast?
No write can occur between test and use: a val, a parameter, or a local var not written on the path and not captured by a writing lambda. Mutable properties never are.
gradual¶
Consistency ~ (Definition 6.7.2).
? ~ τ and τ ~ ? for all τ; otherwise same constructor and pointwise. Reflexive, symmetric, NOT transitive.
Where does cast insertion put a cast?
Wherever a subterm of type S is used at a consistent but different type T: ⟨S ⇒ T⟩ labelled with the subterm's position. Never between equal types.
The gradual guarantee (SVCB15).
Making annotations less precise keeps a program well typed (with a less precise type) and keeps its value; it can only remove run-time failures.
Why does G-If return the meet of the branch types?
Returning ? for unequal branches would make a less annotated program get a more precise type, breaking the static gradual guarantee.
blame¶
Blame label.
The source position carried by a cast; a failing cast reports it, naming the boundary where a promise was made.
How is a function cast ⟨S1→S2 ⇒ T1→T2⟩ run?
It wraps the function: calls cast the argument T1 ⇒ S1 and the result S2 ⇒ T2, with the same label.
Positive vs negative blame (Wadler–Findler).
Positive: the value broke its promise (bad result). Negative: the context did (bad argument). Blame theorem: the more precisely typed side is never blamed.
What do TypeScript and mypy do at an any/Any boundary at run time?
Nothing: annotations are erased, no casts; errors surface inside typed code.
lvalues¶
Place categories in Pebble (Definition 6.8.1).
value, place, mut-place. Names, fields and elements of places are places; mutability comes from the root binding (var, &mut parameter).
C++ value categories.
lvalue (has identity, not movable), xvalue (has identity, movable: std::move(x)), prvalue (no identity: x + 1, f()).
Rust &mut (v[0] + 1) vs Pebble &mut (xs[0] + 1)?
Rust accepts it (materializes a temporary place; the change is lost); Pebble reports E0412 (not a place).
exclusivity¶
Law of Exclusivity (SE-0176).
Two accesses to the same variable may not overlap unless both are reads.
Pebble's E0414 rule.
If an argument is &mut place, its root variable must not appear in any other argument of the same call — reported once per call and variable.
Why is swap(&mut a[0], &mut a[1]) rejected though the elements differ?
The rule compares roots: indices are not known statically in general. Rust says v[_]; split_at_mut proves disjointness in a library.
borrowck¶
NLL region (RFC 2094).
A set of CFG points where a reference may still be used, computed from liveness and outlives constraints by a fixed point.
Loans in scope.
Forward gen/kill dataflow: generated at the borrow, killed where the point leaves the loan's region or an assignment overwrites a prefix of the borrowed path.
Polonius vs NLL.
Polonius (Datalog): origins contain loans; a loan is live where it is in a live origin. It tracks per-point subsets, so it accepts conditional-return cases NLL rejects.
monomorphization¶
Monomorphization.
Compile one copy per instance f<τ…> reachable from the roots (worklist, Algorithm 6.9.2). Fast code, big binaries.
When does monomorphization not terminate?
Polymorphic recursion that grows type arguments (depth<T> calls depth<(T,)>): infinitely many instances; rustc hits its recursion limit.
Pathological growth of monomorphization.
f_i<T> calling f_{i+1}<T> and f_{i+1}<Box<T>> doubles the instances per level: 2^(n+1) − 1.
erasure¶
Erasure of a type variable.
The erasure of its leftmost bound (Object if none): in Box<T extends Comparable<T>>, T erases to Comparable.
What does javac insert after a call of a generic method?
A checkcast to the source type when the erased return type is more general; plus boxing/unboxing of primitives, and bridge methods for overrides.
Why do erased casts never fail (Theorem 6.9.8)?
Source type soundness gives every value a class below the erasure of its static type; casts are inserted only to that type. Unchecked conversions (heap pollution) break it.
dictionary¶
Dictionary passing (Wadler–Blott).
Each class constraint C a becomes an argument holding C's methods at a; instance declarations become dictionary values ($fNumInt).
Swift witness table.
The dictionary of a protocol conformance, passed with type metadata (size, alignment, copy) so generic code handles unboxed values.
How does GHC remove dictionary overhead?
Specialization (SPECIALISE, the specialiser) clones functions at used types; worker/wrapper passes only the needed methods.