Theory test — Chapter 6¶

49 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 6                                   # interactive
./course quiz template 6 -o answers/ch06.yaml  # or fill in a file ...
./course quiz grade 6                             # ... and grade it

Question 1 derivation-rules · mapping · 1 pt · 01-judgments-and-safety

In the derivation of \(\emptyset \vdash (\lambda x{:}\mathsf{int}.\ x < 3)\ (1 + 1) : \mathsf{bool}\)
with the rules of Figure 6.1.1, which rule concludes the judgment for each subterm?

A: the whole application
B: \(\lambda x{:}\mathsf{int}.\ x < 3\)
C: \(x < 3\)
D: \(x\)
E: \(3\)
F: \(1 + 1\)

Answer with rule names such as T-App.

Keys: A, B, C, D, E, F

Answer format: one value per key

Question 2 derivation-invalid-node · set · 1 pt · 01-judgments-and-safety

A claimed derivation (children listed under each node):

A: ∅ ⊢ if 1 < 2 then 3 else 4 : int        children B, C, D
B: ∅ ⊢ 1 < 2 : bool                        children E, F
C: ∅ ⊢ 3 : int
D: ∅ ⊢ 4 : bool
E: ∅ ⊢ 1 : int
F: ∅ ⊢ 2 : int

At which nodes is the tree invalid in the sense of Definition 6.1.4 (the node with its
children is not an instance of any rule of Figure 6.1.1)?

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

Question 3 progress-preservation-mutations · mapping · 1 pt · 01-judgments-and-safety

The typed arithmetic language of the drill progress-preservation (TAPL Ch. 3 and 8) is
modified in one way at a time. Which property does each change destroy? Answer
progress, preservation or none.

M1: add the typing rule succ t : Nat if t : Bool
M2: replace T-If by: if t1 then t2 else t3 : T if t1 : Bool and t2 : T (t3 may have any type)
M3: remove the evaluation rule E-IfFalse
M4: add the evaluation rule if true then t2 else t3 → t3

Keys: M1, M2, M3, M4

Answer format: one value per key

Question 4 canonical-forms-role · single · 1 pt · 01-judgments-and-safety

In the proof of progress (Theorem 6.1.13), case T-If with the condition already a value
\(v\) of type \(\mathsf{bool}\): what justifies that E-IfTrue or E-IfFalse applies?

Preservation (Theorem 6.1.16)
The canonical forms lemma (Lemma 6.1.12): a closed value of type bool is true or false
The substitution lemma (Lemma 6.1.15)
Uniqueness of types (Theorem 6.1.10)

Answer format: one letter

Question 5 static-dynamic-rice · single · 1 pt · 02-classifying-type-systems

Figure 6.1.1 rejects if true then 1 else (true + 1), which never gets stuck. Why can no
static checker for a Turing-complete extension accept exactly the programs that never get
stuck?

Because type checking must run in linear time
Because 'can get stuck' is a non-trivial semantic property, undecidable by reduction from the halting problem (Theorem 6.2.2)
Because the else branch is dead code, and dead code is always an error
Because Figure 6.1.1 has no rule for if

Answer format: one letter

Question 6 dynamic-check-location · multi · 1 pt · 02-classifying-type-systems

In the dynamically checked evaluator (Algorithm 6.2.4), which operations test the tag of
a value? Select all.

application e1 e2 (the function position)
the operands of + and <
the condition of if
a variable reference x
a λ (building the closure)

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

Question 7 js-coercions · mapping · 1 pt · 02-classifying-type-systems

What does console.log print for each JavaScript expression (node 22)?

a: "5" - 1
b: "5" + 1
c: true + 1
d: "3" * "4"

Keys: a, b, c, d

Answer format: one value per key

Question 8 trapped-untrapped · mapping · 1 pt · 02-classifying-type-systems

Classify each execution error as trapped or untrapped (Definition 6.2.5):

e1: C, writing a[10] into int a[4]
e2: Java, reading a[10] of an int[4]
e3: Python, "a" + 1
e4: C, INT_MAX + 1 on int

Keys: e1, e2, e3, e4

Answer format: one value per key

Question 9 covariant-array-soundness · mapping · 1 pt · 02-classifying-type-systems

The program "store an Animal through an Animal[] alias of a Dog[], then call bark()
on that element via the Dog[]" is written in TypeScript (tsc --strict) and in Java.
For each, what happens? Answer compile-error, trap (a run-time exception at the store) or
goes-wrong (compiles, and fails later with the error the types should exclude).

Keys: TypeScript, Java

Answer format: one value per key

Question 10 ts-unsound-features · multi · 1 pt · 02-classifying-type-systems

Which of these TypeScript features let a well-typed program (under --strict) produce a
run-time type error the types claim to exclude? Select all.

the type any
bivariant method parameters
covariant arrays
excess property checks on object literals
strictNullChecks

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

Question 11 error-type-cascade · number · 1 pt · 03-syntax-directed-checking

How many diagnostics does the reference type checker (pebblec --emit=typed-ast) report for
this Pebble program?

fn f(a: int, s: str) -> int {
    let x = a + s;
    let y = x * 2;
    let z = y + s;
    return z;
}
fn main() -> int { return f(1, "a"); }

Answer format: a number

Question 12 synth-order · sequence · 1 pt · 03-syntax-directed-checking

Algorithm 6.3.3 synthesizes the type of (a + b) * c bottom-up. In which order are the
types of these nodes completed? Nodes: a, b, c, S = a + b, P = (a + b) * c.

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

Question 13 find-clang-assignment · text · 1 pt · 03-syntax-directed-checking

Which Sema member function in clang/lib/Sema/SemaExpr.cpp decides whether a value of one
type can be assigned to (or initialize) an object of another type in C? Give the function
name without the Sema:: prefix.

Answer format: a short answer

Question 14 uac-result · mapping · 1 pt · 03-syntax-directed-checking

On x86-64 Linux (int 32 bits, long 64 bits), what is the type of each C expression
after the usual arithmetic conversions (Algorithm 6.3.6)? Variables: short s; unsigned char c; unsigned u; long l; unsigned long ul; float f;

e1: s + c
e2: 1 + u
e3: l + u
e4: ul + 1
e5: f + l

Answer with C type names: int, unsigned, long, unsigned long, float, double.

Keys: e1, e2, e3, e4, e5

Answer format: one value per key

Question 15 uac-minus-one · number · 1 pt · 03-syntax-directed-checking

What does printf("%d\n", -1 < 1u); print in C on x86-64 Linux?

Answer format: a number

Question 16 find-clang-uac · text · 1 pt · 03-syntax-directed-checking

Name the Sema member function that implements C11 §6.3.1.8, the usual arithmetic
conversions (without the Sema:: prefix).

Answer format: a short answer

Question 17 overload-ambiguity · mapping · 1 pt · 03-syntax-directed-checking

C++ declarations: void k(short); void k(long); void m(double); void m(int); void n(int); void n(unsigned char);. What does each call resolve to? Answer the chosen overload, e.g.
m(int), or ambiguous.

c1: k(1)
c2: m(2.5f)
c3: n('a')

Keys: c1, c2, c3

Answer format: one value per key

Question 18 java-phases · mapping · 1 pt · 03-syntax-directed-checking

Java 21 overloads: m(long)/m(Integer), n(Object)/n(int...),
o(Integer)/o(int...), p(double)/p(Integer). Which is chosen for m(1), n(1),
o(1), p(1)?

Keys: m(1), n(1), o(1), p(1)

Answer format: one value per key

Question 19 bidir-mode-of-premise · mapping · 1 pt · 04-bidirectional-typing

Algorithm 6.4.4 checks \((\lambda f.\ f\ 1)\) against \((\mathsf{int} \to \mathsf{int}) \to \mathsf{int}\).
Label each subterm with how it is visited, in the drill bidir-modes' vocabulary: check
(a checking rule), synth, or switch (checked, by synthesizing and comparing).

A: \(\lambda f.\ f\ 1\)
B: \(f\ 1\)
C: \(f\)
D: \(1\)

Keys: A, B, C, D

Answer format: one value per key

Question 20 pebble-literal-propagation · mapping · 1 pt · 04-bidirectional-typing

Pebble: fn f(x: int) -> float and fn g(x: float) -> float. In
let v: float = f(1) + 2 * g(3);, what type does the reference checker record for each
integer literal?

L1: the 1 in f(1)
L2: the 2
L3: the 3 in g(3)

Keys: L1, L2, L3

Answer format: one value per key

Question 21 find-rustc-expectation · text · 1 pt · 04-bidirectional-typing

In compiler/rustc_hir_typeck, which enum carries the expected type into expression
checking (its variant ExpectHasType is the checking mode ⇐)?

Answer format: a short answer

Question 22 local-inference-trace · mapping · 1 pt · 04-bidirectional-typing

Algorithm 6.4.6 on map(xs, fn x => x < 1) with
\(\mathit{map} : \forall \alpha\beta.\ [\alpha] \to (\alpha \to \beta) \to [\beta]\) and
\(xs : [\mathsf{int}]\), in synthesis mode. Give the final substitution (keys alpha, beta).

Keys: alpha, beta

Answer format: one value per key

Question 23 local-inference-limits · single · 1 pt · 04-bidirectional-typing

With \(\mathit{empty} : \forall \alpha.\ () \to [\alpha]\), what does Algorithm 6.4.6 do on
let e = empty() (no annotation)?

Infers α = int, the default element type
Reports that α cannot be inferred: no argument and no expected type constrain it
Leaves α free and generalizes e to a polymorphic type
Loops forever

Answer format: one letter

Question 24 subtype-queries · mapping · 1 pt · 05-subtyping

Algorithmic subtyping with records (width, depth, permutation), \(\top\), \(\bot\) and
contravariant parameters. Answer yes or no for each \(S <: T\).

q1: {a: int, b: bool} <: {b: top}
q2: {a: int} -> int <: {a: int, b: bool} -> top
q3: (top -> int) -> bot <: (int -> top) -> int
q4: {f: {x: int} -> bot} <: {f: {x: int, y: int} -> int}

Keys: q1, q2, q3, q4

Answer format: one value per key

Question 25 transitivity-elimination · single · 1 pt · 05-subtyping

Why can Algorithm 6.5.4 omit the transitivity rule S-Trans and still be complete for the
declarative system?

Because subtyping on records is not transitive
Because transitivity is admissible in the algorithmic system (Lemma 6.5.11): the algorithmic rules already derive every composition
Because the algorithm searches over intermediate types up to a size bound
Because transitivity only matters for nominal types

Answer format: one letter

Question 26 variance-positions · mapping · 1 pt · 05-subtyping

In class C[X] { m1(): X; m2(v: X): unit; m3(f: X -> int): unit; m4(): X -> int }, what is
the polarity (+ or -) of the occurrence of X in each member (Algorithm 6.5.7)?

Keys: m1, m2, m3, m4

Answer format: one value per key

Question 27 java-wildcards · mapping · 1 pt · 05-subtyping

Java 21, parameters List<? extends Number> ln and List<? super Integer> ls. Does each
statement compile (yes/no)?

s1: ln.add(1);
s2: Number n = ln.get(0);
s3: ls.add(1);
s4: Integer i = ls.get(0);

Keys: s1, s2, s3, s4

Answer format: one value per key

Question 28 nominal-structural · mapping · 1 pt · 05-subtyping

class Meters { value: number } and class Seconds { value: number } (no inheritance
between them). Is passing a Seconds where a Meters is expected accepted (yes/no)?

Keys: Java, TypeScript

Answer format: one value per key

Question 29 hotspot-display · number · 1 pt · 05-subtyping

A JVM stores each class's primary superclasses in a display indexed by depth: Object
at depth 0, its direct subclass at 1, and so on. With class A, class B extends A,
class C extends B, class D extends C, which display slot of the object's class does a
fast instanceof B test compare with B?

Answer format: a number

Question 30 occurrence-and-else · mapping · 1 pt · 06-flow-sensitive-typing

\(x : \mathsf{number} \mid \mathsf{string} \mid \mathsf{null}\). For the guard
typeof x === "number" && x > 0, give the set of types of \(x\) when the whole guard is
true (then) and when it is false (else), by T-And of Definition 6.6.2.

Keys: then, else

Answer format: one value per key (a set: {x, y})

Question 31 mypy-else-branch · set · 1 pt · 06-flow-sensitive-typing

mypy 1.19.1, def describe(x: int | str | None): after if x is None: return ..., the
code tests if isinstance(x, int) and x > 0: return .... What does reveal_type(x) show
on the next line? Give the set of types.

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

Question 32 narrowing-trace · mapping · 1 pt · 06-flow-sensitive-typing

Algorithm 6.6.3 on

function f(x: number | string | boolean | null | undefined) {
    if (x == null) return;
    x;  // p2
    if (typeof x === "string" || typeof x === "boolean") {
        x;  // p3
    } else {
        x;  // p4
        x = "s";
    }
    x;  // p5
}

Give the type of x at each probe as a set.

Keys: p2, p3, p4, p5

Answer format: one value per key (a set: {x, y})

Question 33 kotlin-stability · multi · 1 pt · 06-flow-sensitive-typing

In Kotlin 2.2, after if (v is String), in which cases is v.length accepted by a smart
cast? Select all.

v is a function parameter
v is a local val
v is a var property of a class (h.value)
v is a local var that a lambda captures and assigns

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

Question 34 consistency-not-transitive · mapping · 1 pt · 07-gradual-typing

Consistency (Definition 6.7.2). Answer yes or no for each pair:

k1: int ~ ?
k2: int -> ? ~ ? -> bool
k3: int -> bool ~ bool -> ?
k4: {a: int} ~ {a: ?, b: int}
k5: ? ~ int -> int

Keys: k1, k2, k3, k4, k5

Answer format: one value per key

Question 35 gradual-cast-insertion · number · 1 pt · 07-gradual-typing

How many casts does Algorithm 6.7.4 insert into the Bic program
(fn (x: int) => x + 1) ((fn y => y) 3)?

Answer format: a number

Question 36 blame-label · single · 1 pt · 07-gradual-typing

(fn (g: ? -> ?) => g 1) (fn (b: bool) => if b then 1 else 2) fails at run time. Which
term's position does the blame label name?

the literal 1 in g 1
the argument function fn (b: bool) => ..., where it was cast to ? -> ?
the parameter b inside the second function
the whole application

Answer format: one letter

Question 37 mypy-any-no-cast · single · 1 pt · 07-gradual-typing

def inc(x: int) -> int: return x + 1, and v = load() where load() -> Any returns
"41". What happens with mypy --strict and then python3 on print(inc(v))?

mypy reports an error at inc(v)
mypy accepts; Python raises a TypeError inside inc, at x + 1
mypy accepts; Python raises a TypeError at the call inc(v), naming parameter x
mypy accepts; Python prints 42

Answer format: one letter

Question 38 place-category · mapping · 1 pt · 08-places-and-references

Pebble, inside fn h(p: &int, q: &mut int) -> int { var xs = [1, 2]; let k = 0; ... }:
what category does the type table of ch06-typecheck print for each expression
(value, place or mut-place)?

e1: xs[k]
e2: k
e3: p
e4: q
e5: xs[0] + 1

Keys: e1, e2, e3, e4, e5

Answer format: one value per key

Question 39 lvalue-cpp-bind · set · 1 pt · 08-places-and-references

Which of these C++ lines does clang++ 23 reject? (int f(); void inc(int &r); int a[3]; const int k = 1; int x = 0;)

L1: a[1] = 5;
L2: x + 1 = 2;
L3: f() = 3;
L4: k = 4;
L5: inc(x + 1);
L6: inc(x);

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

Question 40 exclusivity-roots · set · 1 pt · 08-places-and-references

Pebble, with var a = [1, 2]; var b = [3, 4]; var s = S { x: 1, y: 2 };,
fn swap(a: &mut int, b: &mut int) and fn add(d: &mut int, s: &int). Which calls get
E0414?

c1: swap(&mut a[0], &mut b[0]);
c2: swap(&mut s.x, &mut s.y);
c3: add(&mut a[0], &a[1]);
c4: add(&mut a[1], &b[a[0]]);

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

Question 41 e0414-once · number · 1 pt · 08-places-and-references

With fn three(a: &mut int, b: &mut int, c: &mut int) and var n = 0;, how many E0414
does three(&mut n, &mut n, &mut n); produce?

Answer format: a number

Question 42 nll-region · mapping · 1 pt · 08-places-and-references

Rust, lines numbered:

2    let mut v = vec![1];
3    let r = &v;          // loan L1
4    let n = r.len();
5    v.push(n);
6    let s = &v;          // loan L2
7    println!("{}", s.len());
8    v.push(2);
9    println!("{}", s.len());

By Definition 6.8.5 and Algorithm 6.8.6 (liveness), give the lines of each loan's region
after its borrow (the lines where the reference may still be used).

Keys: L1, L2

Answer format: one value per key (a set: {x, y})

Question 43 loans-in-scope · set · 1 pt · 08-places-and-references

Same program as the previous question. At which lines does Algorithm 6.8.8 report a
conflicting access to v?

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

Question 44 mono-instances · number · 1 pt · 09-implementing-generics

Rust: fn h<U>(u: U), fn g<U>(u: U) { h(u) }, fn f<T: Copy>(t: T) { g(t); g(Bx(t)); }
(with struct Bx<T>(T)) and main calls f(1i32) and f(1i64). How many instances of
f, g and h in total does Algorithm 6.9.2 produce?

Answer format: a number

Question 45 mono-polyrec · single · 1 pt · 09-implementing-generics

Why does rustc reject fn depth<T>(x: T, n: u32) -> u32 { if n == 0 { 0 } else { 1 + depth((x,), n - 1) } }
called as depth(1u8, 3), although it recurses only three times at run time?

Because tuples cannot be generic arguments
Because monomorphization instantiates depth at T, (T,), ((T,),), … without evaluating n, so the worklist never empties (Theorem 6.9.7)
Because recursion is not allowed in generic functions
Because the borrow checker rejects moving x

Answer format: one letter

Question 46 erasure-checkcast · number · 1 pt · 09-implementing-generics

javac 21 compiles static String first(List<String> xs) { return xs.get(0) + xs.get(1).trim(); }.
How many checkcast instructions does javap -c show in first?

Answer format: a number

Question 47 erasure-bound · text · 1 pt · 09-implementing-generics

In class Box<T extends Comparable<T>> { T get(); }, what type does get() return in the
JVM descriptor (the erasure of T)? Give the simple class name.

Answer format: a short answer

Question 48 dictionary-translation · number · 1 pt · 09-implementing-generics

Under the dictionary-passing translation (Algorithm 6.9.6), how many dictionary parameters
does f :: (Eq a, Show b) => a -> b -> String get?

Answer format: a number

Question 49 ghc-dfun · text · 1 pt · 09-implementing-generics

In GHC 9.4's Core (-ddump-simpl -dsuppress-all), what is the name of the dictionary that
useInt = sumSq passes for the constraint Num Int?

Answer format: a short answer