Theory test — Chapter 7

51 questions; you pass at 80 %. This page shows the questions only: take the test in the terminal, where every answer is graded and explained.

./course quiz 7                                   # interactive
./course quiz template 7 -o answers/ch07.yaml  # or fill in a file ...
./course quiz grade 7                             # ... and grade it

Question 1 unify-mgu · mapping · 1 pt · 01-unification

Give the most general unifier of the single equation
\(h(x, y, g(u)) \doteq h(g(y), g(z), x)\) (\(x, y, z, u\) variables; \(h\) ternary, \(g\) unary)
in solved form: the term bound to each of \(x\), \(y\), \(u\) (the MGU leaves \(z\) unbound).

Keys: x, y, u

Answer format: one value per key

Question 2 find-clang-deduction · text · 1 pt · 01-unification

Find where LLVM does it: in clang/lib/Sema/SemaTemplateDeduction.cpp (LLVM 23.1.2),
DeduceTemplateArgumentsByTypeMatch matches a parameter type against an argument type.
When a template parameter has already been deduced with a different value, which
enumerator of TemplateDeductionResult is returned? (Give the enumerator name.)

Answer format: a short answer

Question 3 mm-rule-sequence · sequence · 1 pt · 01-unification

Run Algorithm 7.1.8 (Martelli–Montanari, pop the first equation, decomposed equations go
to the front in order) on the list \(\langle f(x, a) \doteq f(g(y), y),\ g(z) \doteq x \rangle\)
(\(a\) a constant). Give the rules applied, in order (use delete, decompose, conflict,
swap, check, eliminate).

Answer format: items in order, e.g. A B C

Question 4 mm-termination-measure · single · 1 pt · 01-unification

Which quantity strictly decreases under the eliminate rule in the termination proof of
Theorem 7.1.15?

1. The total size of the terms in the worklist
2. The number of variables occurring in the worklist that are not left-hand sides of the solved part
3. The number of equations of the form t = x with t not a variable
4. The number of equations in the worklist

Answer format: one letter

Question 5 uf-unions · number · 1 pt · 01-unification

Run Algorithm 7.1.10 (union-find unification; one node per variable, one per occurrence of an
application; stack of pairs, the first equation's pair popped first) on
\(\{\,f(x, g(x)) \doteq f(g(y), z),\ z \doteq g(g(u))\,\}\). How many union operations are
performed?

Answer format: a number

Question 6 find-llvm-equivalence-classes · text · 1 pt · 01-unification

Find where LLVM does it: llvm/include/llvm/ADT/EquivalenceClasses.h (LLVM 23.1.2) is a
union-find. Which member function of EquivalenceClasses merges the classes of two
elements (Algorithm 7.1.10's union)?

Answer format: a short answer

Question 7 occurs-verdict · mapping · 1 pt · 01-unification

For each single equation, is the verdict ok (a unifier exists), clash or occurs?

• A: \(f(x, y) \doteq f(y, g(x))\)
• B: \(g(x) \doteq h(x, y)\)
• C: \(f(x, a) \doteq f(b, x)\)
• D: \(f(x, g(y)) \doteq f(g(y), x)\)

Keys: A, B, C, D

Answer format: one value per key

Question 8 occurs-rectypes · single · 1 pt · 01-unification

ocamlc -rectypes -i gives let self_apply = fun x -> x x the type
('a -> 'b as 'a) -> 'b. What does -rectypes change?

1. It replaces unification by one-sided matching
2. It omits the occurs check and accepts cyclic (rational-tree) solutions
3. It generalizes λ-bound variables
4. It turns off the value restriction

Answer format: one letter

Question 9 lambda-vs-let · multi · 1 pt · 02-hindley-milner

Which MiniML programs are typable in Hindley–Milner (with the builtins of the lab)?

1. let k = fun x -> fun y -> x in (k 1 true, k true 1)
2. (fun k -> (k 1 true, k true 1)) (fun x -> fun y -> x)
3. fun x -> let y = x in (y 1, y true)
4. let rec len = fun l -> if isnil l then 0 else 1 + len (tail l) in (len (cons 1 nil), len (cons true nil))

Answer format: letters, e.g. a, c

Question 10 principal-type · text · 1 pt · 02-hindley-milner

Give the principal type of fun f -> fun g -> fun x -> g (f x) in the lab's canonical form
(variables 'a, 'b, … in order of first occurrence).

Answer format: a short answer

Question 11 w-unifications · number · 1 pt · 02-hindley-milner

How many calls of Unify does Algorithm W (Algorithm 7.2.7) make on
let k = fun x -> fun y -> x in (k 1 true, k true 1)?

Answer format: a number

Question 12 w-subterm-type · mapping · 1 pt · 02-hindley-milner

Algorithm W on fun g -> (g 1, g 2 + 1). After inference, what are the (canonical) types of
these subterms? s1 = the whole program, s4 = the first occurrence of g, s6 = g 2 + 1.

Keys: s1, s4, s6

Answer format: one value per key

Question 13 j-links · single · 1 pt · 02-hindley-milner

What does Algorithm J do with the environment Γ after a unification that binds a type
variable occurring in Γ?

1. It applies the new substitution to every type in Γ
2. Nothing: the variable node is linked in the global union-find, and Γ's types are dereferenced when read
3. It re-generalizes every let-bound scheme in Γ
4. It copies Γ so that the old version stays valid

Answer format: one letter

Question 14 w-vs-j-cost · single · 1 pt · 02-hindley-milner

In the lab's measurement, doubling \(n\) in letChain(n) multiplies W's time by about 4.9 and
J's (with levels) by about 1.6. Which explanation fits?

1. W is exponential on let chains, J is linear
2. W does Θ(n) work per let (substituting into and scanning the environment), Θ(n²) in total; J with levels does work proportional to each let's type, near-linear in total
3. J skips the occurs check
4. W unifies more often than J

Answer format: one letter

Question 15 m-error-position · mapping · 1 pt · 02-hindley-milner

let g = fun h -> h true in g (fun n -> n + 1) is ill typed. At which position (line:col,
one line, columns from 1) do W, J and M report the error, using the lab's conventions?

Keys: W, J, M

Answer format: one value per key

Question 16 m-expected-type · single · 1 pt · 02-hindley-milner

In Algorithm M, what does the call for the function part of an application e1 e2 receive
as its expected type, when the application itself is expected to have type ρ?

1. ρ
2. β → ρ for a fresh β, which the argument is then checked against
3. a fresh variable, unified with ρ afterwards
4. nothing: functions are synthesized

Answer format: one letter

Question 17 levels-generalize · mapping · 1 pt · 03-generalization-and-complexity

Algorithm J with levels (Algorithm 7.3.2) on
fun a -> let f = fun x -> (a, x) in f. Just after leaving f's right-hand side (current
level back to 1), what are the levels of the type variables of a and of x?

Keys: a, x

Answer format: one value per key

Question 18 levels-lowering · single · 1 pt · 03-generalization-and-complexity

Why does binding a variable α to a type t lower the levels of the variables in t to lvl(α)?

1. To make instantiation faster
2. Because those variables are now reachable from wherever α is: if α is free in the context, so are they, and they must not be generalized by an inner let
3. To implement the value restriction
4. Because levels must decrease for termination

Answer format: one letter

Question 19 vr-schemes · mapping · 1 pt · 03-generalization-and-complexity

With the value restriction, how is each let-bound name of
let r = ref nil in let p = (fun x -> x, 1) in let q = fst p in let s = fun z -> get r in (q, s)
bound? Answer generalized (every variable of its type quantified), monomorphic (none) or
partly (some but not all).

Keys: r, p, q, s

Answer format: one value per key

Question 20 vr-unsound · single · 1 pt · 03-generalization-and-complexity

What goes wrong if let r = ref (fun x -> x) in … is generalized to
∀α. (α → α) ref?

1. Inference no longer terminates
2. One instance can store an int -> int function and another instance can read it at bool -> bool, so a well-typed program adds 1 to true
3. The occurs check fails
4. Nothing; the value restriction is only a performance optimization

Answer format: one letter

Question 21 tower-arrows · number · 1 pt · 03-generalization-and-complexity

How many -> occur in the principal type of pairTower(10) =
let x0 = fun z -> z in let x1 = (x0, x0) in … let x10 = (x9, x9) in x10?

Answer format: a number

Question 22 dexptime · single · 1 pt · 03-generalization-and-complexity

HM typability is DEXPTIME-complete, yet ML compilers are fast. Which statement reconciles the
two?

1. Compilers use approximate inference
2. The exponential cases need deep let-nesting that doubles type sizes; with bounded let-depth and type size, inference is nearly linear (McAllester)
3. Union-find makes the worst case polynomial
4. The value restriction removes the exponential cases

Answer format: one letter

Question 23 hmx-residual · text · 1 pt · 04-constraint-based-inference

In HM(X) with X = type classes, what is the principal (qualified) type of the lab's
fun x -> fun y -> eq x y, with eq : Eq 'a => 'a -> 'a -> bool? (Canonical form.)

Answer format: a short answer

Question 24 hmx-pebble-solution · mapping · 1 pt · 04-constraint-based-inference

Pebble's inference mode (pebble-spec §8.9), function body
let a = 2; let b = a * 3; let c = [4, 5]; let d = c[a] + 0.5; let e = 6 << 1; return 0;.
What type does each literal get? (Keys: the literal's value.)

Keys: 2, 3, 4, 5, 6

Answer format: one value per key

Question 25 find-tablegen-inference · text · 1 pt · 04-constraint-based-inference

Find where LLVM does it: in llvm/utils/TableGen/Common/CodeGenDAGPatterns.cpp (LLVM
23.1.2), which TreePattern member function repeatedly applies type constraints to a
pattern's trees until nothing changes?

Answer format: a short answer

Question 26 outsidein-untouchable · single · 1 pt · 04-constraint-based-inference

In OutsideIn(X), why may the solver not assign an outer unification variable from inside an
implication a ~ Bool ⊃ p ~ Bool?

1. Because unification inside implications is undecidable
2. Because the given a ~ Bool could make several incomparable assignments valid (p := Bool or p := a), so choosing one would be a guess
3. Because implications are solved after the program runs
4. Because outer variables are rigid

Answer format: one letter

Question 27 gadt-principal · single · 1 pt · 04-constraint-based-inference

What makes GHC accept test :: Term a -> Bool; test (IsZero t) = True?

1. The signature fixes the result type, so the wanted inside the implication is Bool ~ Bool
2. GHC defaults p to Bool
3. MonoLocalBinds
4. The pattern is exhaustive

Answer format: one letter

Question 28 swift-states · number · 1 pt · 05-swift-constraint-solver

In the lesson's Swift model (+ with overloads (Int,Int)->Int, (Double,Double)->Double,
(String,String)->String; * with the first two; integer literals may be Int or
Double), how many search states (alternatives attempted) does Algorithm 7.5.4 explore for
1 + 2 * 3 with no contextual type, solving the * disjunction first?

Answer format: a number

Question 29 swift-family-states · number · 1 pt · 05-swift-constraint-solver

The 3-SAT family of Lesson 7.5 §5 with \(n = 4\) (variables \(x_1, \dots, x_4\); clauses
\((x_4 \vee x_4 \vee x_4)\) and \((\neg x_4 \vee \neg x_4 \vee \neg x_4)\); disjunctions searched in
the order pick_1 … pick_4, clause_1, clause_2): how many states does the search explore?

Answer format: a number

Question 30 rust-fallback · mapping · 1 pt · 06-local-and-flow-inference

In rustc 1.94, what type does each variable get?
let a = 1; let b: u8 = a; let c = 2; let d = 2.0;

Keys: a, c, d

Answer format: one value per key

Question 31 rust-scope · single · 1 pt · 06-local-and-flow-inference

Why does rustc report E0282 for let v = Vec::new(); println!("{}", v.len()); but not for
let c = 2;?

1. Vec::new is not generic
2. Only integer and float literal variables have a fallback; a general type variable left unresolved at the end of the body is an error
3. println! needs the element type
4. The body is not an inference scope

Answer format: one letter

Question 32 kotlin-builder · text · 1 pt · 06-local-and-flow-inference

Kotlin 2.2: what is the type of val xs = buildList { add(1); add(2) }? (Kotlin spelling.)

Answer format: a short answer

Question 33 kotlin-scope · single · 1 pt · 06-local-and-flow-inference

Kotlin 2.2 rejects val n = 1 followed by val d: Double = n, while Pebble's inference mode
accepts the analogous let n = 1; let d: float = n;. Why?

1. Kotlin has no integer literal types
2. Kotlin's inference scope is the declaration: n : Int is fixed there; Pebble's is the function body, so the later use decides n
3. Kotlin defaults to Long
4. Pebble has implicit conversions

Answer format: one letter

Question 34 ts-widening · single · 1 pt · 06-local-and-flow-inference

In tsc 6.0, let n = 1; gets the declared type number and const one = 1; the type 1.
Why the difference?

1. const declarations are inferred from their uses
2. A mutable declaration gets the widened type of its initializer (literal type 1 widened to number), so later assignments of other numbers are allowed; a const keeps the fresh literal type
3. number is the default type of numeric literals
4. let declarations are flow-typed

Answer format: one letter

Question 35 ts-evolving · text · 1 pt · 06-local-and-flow-inference

tsc 6.0 with --strict: function late() { let acc = []; acc.push(1); acc.push("s"); return acc; }.
What return type does tsc declare for late? (tsc's spelling.)

Answer format: a short answer

Question 36 pebble-literal-types · single · 1 pt · 06-local-and-flow-inference

In Pebble's inference mode, let y = 1.5; let z = y * 2; is accepted. What does Chapter 6's
checker (ch06-typecheck) report for the same lines?

1. Nothing: both checkers accept it
2. E0402 at the *: in synthesis mode the literal 2 synthesizes int
3. E0401 at the literal
4. E0416

Answer format: one letter

Question 37 pebble-e0416 · mapping · 1 pt · 06-local-and-flow-inference

ch07-infer on this body (line numbers on the left):

2    let k = 1;
3    let m = k + 2.5;
4    let j: int = k;
5    let w = 3;
6    let t = w == false;
7    let u: bool = 7;

Which error code is reported on each of lines 4, 6 and 7?

Keys: 4, 6, 7

Answer format: one value per key

Question 38 evidence-term · text · 1 pt · 07-type-classes-and-traits

In the lab's ★ milestone (instances Eq int, Eq bool, Eq 'a => Eq ('a list),
(Eq 'a, Eq 'b) => Eq ('a * 'b) with instance functions eqInt, eqBool, eqList,
eqPair), give the dictionary (evidence term) for Eq ((int * bool) list).

Answer format: a short answer

Question 39 find-rustc-selection · text · 1 pt · 07-type-classes-and-traits

Find it in rustc: which struct in compiler/rustc_trait_selection/src/traits/select/mod.rs
(rustc 1.94.1) has the method select that resolves a trait obligation to an impl?

Answer format: a short answer

Question 40 coherence-overlap · set · 1 pt · 07-type-classes-and-traits

Instance heads of one class C: I1 = C [a], I2 = C [Int], I3 = C (a, Int),
I4 = C (Bool, b), I5 = C Int. Which pairs overlap (write them like I1-I2)?

Answer format: items separated by commas or spaces, e.g. {a, b}

Question 41 orphan-rule · multi · 1 pt · 07-type-classes-and-traits

In crate mine (defining the type Point and the trait Shape), which impls does Rust's
orphan rule allow?

1. impl std::fmt::Display for Point
2. impl Shape for Vec<u8>
3. impl std::fmt::Display for Vec<u8>
4. impl<T> Shape for T

Answer format: letters, e.g. a, c

Question 42 dict-translation · number · 1 pt · 07-type-classes-and-traits

With NoMonomorphismRestriction, GHC infers x0 :: Eq a => a -> Bool for x0 z = z == z,
and x1 = (x0, x0), x2 = (x1, x1), x3 = (x2, x2). How many dictionary parameters does
x3 take after the dictionary-passing translation?

Answer format: a number

Question 43 mono-copies · number · 1 pt · 07-type-classes-and-traits

A Rust program calls the generic fn member<T: PartialEq>(x: &T, xs: &[T]) -> bool as
member(&1i32, …), member(&2u8, …), member(&3i32, …) and member(&"s", …). How many
copies of member (not counting its closures) does monomorphization emit at opt-level 0?

Answer format: a number

Question 44 rank-of-type · mapping · 1 pt · 08-higher-rank-and-impredicativity

Give the rank (Definition 7.8.1) of each type:

• A: Int -> Int
• B: forall a. a -> a
• C: (forall a. a -> a) -> Int
• D: ((forall a. a -> a) -> Int) -> Bool
• E: Int -> (forall a. a -> a)

Keys: A, B, C, D, E

Answer format: one value per key

Question 45 rank2-check · multi · 1 pt · 08-higher-rank-and-impredicativity

With both :: (forall a. a -> a) -> (Int, Bool), which calls does GHC 9.4 accept?

1. both id
2. both not
3. both (\x -> x)
4. both (+ 1)

Answer format: letters, e.g. a, c

Question 46 impredicative-instantiation · single · 1 pt · 08-higher-rank-and-impredicativity

With ImpredicativeTypes, how does Quick Look type head ids where ids :: [forall a. a -> a]?

1. It generalizes head's result
2. It looks at the argument ids, whose type is known, and instantiates head's type variable with the polymorphic type forall a. a -> a
3. It rejects it; impredicative instantiation is never inferred
4. It instantiates with a fresh monotype and unifies later

Answer format: one letter

Question 47 system-f-undecidable · single · 1 pt · 08-higher-rank-and-impredicativity

Why do all practical systems with arbitrary-rank or impredicative polymorphism require some
annotations?

1. Because type inference for System F is undecidable (Wells 1999)
2. Because unification is NP-hard
3. Because of the value restriction
4. Because principal types always exist but are too large

Answer format: one letter

Question 48 blame-first-failure · text · 1 pt · 09-error-localization

Where (line:col) does Algorithm W report the error in
fun y -> (y + 1, (if y then 2 else 3, y * 4)) (one line, columns from 1)?

Answer format: a short answer

Question 49 mus-count · number · 1 pt · 09-error-localization

How many minimal unsatisfiable subsets does the labelled constraint set of
fun f -> ((f 1, f 2), f true) have (Algorithm 7.9.4's constraints)?

Answer format: a number

Question 50 min-error-source · set · 1 pt · 09-error-localization

For the same program fun f -> ((f 1, f 2), f true), the two MUSes have the locations
{1:12, 1:14, 1:23, 1:25} and {1:17, 1:19, 1:23, 1:25}. Which locations are, each on its own,
a minimum error source?

Answer format: items separated by commas or spaces, e.g. {a, b}

Question 51 provenance-note · single · 1 pt · 09-error-localization

rustc's E0308 for let n = 1; let a: u8 = n; let b: u64 = n; says "expected due to this" at
the u64 annotation. What does Pebble's E0416 note point at for the analogous program?

1. The annotation of the second binding
2. The use that decided n's type (the checked n in let a: int = n)
3. The declaration of n
4. The literal 1

Answer format: one letter