Lab 6 · Two type checkers for one calculus (and ★ subtyping, ★ gradual casts)¶

Chapter: 6 · Type Systems & Type Checking · Lessons: 6.3 (syntax-directed checking), 6.4 (bidirectional typing), ★ 6.5 (algorithmic subtyping), ★ 6.7 (gradual typing) · Time: 6–9 hours (3–5 without the ★ parts) · Tests: ./course test 6 (label ch06; lab tests ch06.Bidir.* and ch06.lab.measure-smoke)

1. Goal¶

You write two type checkers for Bic, a small typed lambda calculus with let, if, integers, booleans and records:

a purely syntax-directed checker (Lesson 6.3): one judgment \(\Gamma \vdash e : \tau\), every term's type computed from its subterms' types, so every lambda needs its parameter annotated;
a bidirectional checker (Lesson 6.4, Algorithm 6.4.4): synthesis \(\Gamma \vdash e \Rightarrow \tau\) and checking \(\Gamma \vdash e \Leftarrow \tau\), so a lambda needs no annotation wherever a function type is expected.

Then you measure them on a corpus: how many of the written annotations each one really needs, and whether its error lands where the mistake is. The ★ milestones add algorithmic subtyping checked against a brute-force search for declarative derivations (L4), and gradual typing by cast insertion with blame, run by the provided evaluator (L5).

You design everything inside the checkers: the context, the traversal, how errors propagate. The provided code (provided/Lang.cpp) is the language: types, parser, printer, annotation erasure, corpus reader and an evaluator with casts.

2. The Bic language (provided)¶

2.1 Types¶

T ::= int | bool | top | bot | ? | T -> T | { l1: T1, ..., ln: Tn } | ( T )

-> associates to the right. Record labels are distinct; two record types are equal when they have the same labels with equal types, in any order (operator== in Bic.h). top and bot matter only for L4, ? only for L5; the checkers of L1–L2 treat them as ordinary base types.

2.2 Terms¶

e ::= x | n | true | false
    | fn x => e | fn (x: T) => e          lambda (extends as far right as possible)
    | e1 e2                               application (left-assoc., binds tighter than + -)
    | (e : T)                             annotation (ascription)
    | let x = e1 in e2 | let x: T = e1 in e2
    | if e1 then e2 else e3
    | e1 + e2 | e1 - e2                   left-assoc.
    | e1 < e2 | e1 == e2                  non-assoc., lowest binary precedence
    | { l1 = e1, ..., ln = en } | e.l     records and projection (binds tightest)
    | ( e )

# starts a comment to the end of the line. Every term has the position of its first token (Term::Line, Term::Col); an annotation (e : T) has the position of its (; a parenthesized (e) is just e; a binary term has the position of its left operand; an application the position of its function.

2.3 The tree (`include/bidir/Bic.h`)¶

A Program is a vector of Terms with integer child indices (Kids) and a Root. Useful provided functions: parseProgram, printProgram, parseType, printType, annotationCount and eraseAnnotation (pre-order numbering of lambda, let and ascription annotations), readCorpus, evaluate.

3. Requirements and contract¶

Implement in src/ (switch bidir):

CheckResult checkSyntaxDirected(const Program &P);   // L1
CheckResult checkBidirectional(const Program &P);    // L2

CheckResult is std::expected<Type, Diagnostic>: the program's type, or the first error in the order below with its position (the message is free text, not tested). Checking stops at the first error.

3.1 L1 — syntax-directed rules¶

Subterms are checked left to right; the error is the first failing premise.

Term	Rule	Error position when it fails
`x`	\(\Gamma(x)\)	`x` (unbound)
`n`, `true`, `false`	`int`, `bool`	—
`fn (x: T) => e`	\(T \to \tau_e\)	—
`fn x => e`	always an error	the `fn`
`e1 e2`	\(e_1 : A \to B\), \(e_2 : A\) gives \(B\)	`e1` if not a function; `e2` if its type is not \(A\)
`(e : T)`	\(e : T\) exactly	`e`
`let x [: T] = e1 in e2`	\(e_1 : T\) if annotated; \(x\) gets \(T\) or \(e_1\)'s type	`e1`
`if c then a else b`	\(c\): `bool`; \(a\), \(b\) equal types	`c`; `b` if the branch types differ
`+ - <`	both operands `int`; `<` gives `bool`	the first operand that is not `int`
`e1 == e2`	\(e_1\) is `int` or `bool`; \(e_2\) has the same type	`e1` (not comparable); `e2` (different type)
`{…}`	record of the fields' types	—
`e.l`	\(e\) a record with field \(l\)	`e` if not a record; the projection if no field `l`

3.2 L2 — bidirectional rules¶

The program is synthesized. Checking \(e \Leftarrow T\) has its own rules for the introduction forms and passes the expected type into let bodies and if branches; every other term is synthesized and compared with \(T\) (mode switch, error at that term).

Mode	Term	Rule
synth	`x`, literals, annotated `fn`, operators, records, projection	as in §3.1, except that operands of `+ - <` are checked against `int`, the right side of `==` is checked against the left side's type, and the argument of an application is checked against the parameter type
synth	`fn x => e`	error at the `fn`
synth	`(e : T)`	check \(e \Leftarrow T\), result \(T\)
synth	`let x: T = e1 in e2`	check \(e_1 \Leftarrow T\); `let x = e1` synthesizes \(e_1\)
synth	`if c then a else b`	check \(c \Leftarrow\) `bool`, synthesize \(a : A\), check \(b \Leftarrow A\)
check \(T\)	`fn x => e`, `fn (x: S) => e`	\(T\) must be \(A \to B\) (else error at the `fn`); an annotation \(S\) must equal \(A\) (else error at the `fn`); check \(e \Leftarrow B\) with \(x : A\)
check \(T\)	`if c then a else b`	check \(c \Leftarrow\) `bool`, \(a \Leftarrow T\), \(b \Leftarrow T\)
check \(T\)	`let`	the binding as in synthesis; check the body \(\Leftarrow T\)
check \(T\)	`{l1 = e1, …}`	if \(T\) is a record type with exactly these labels, check each field against its type; otherwise mode switch
check \(T\)	anything else	synthesize \(S\); error at the term if \(S \ne T\)

3.3 Observable behavior¶

Both checkers accept every fully annotated well-typed program with the same type (Lesson 6.4, Theorem 6.4.9's annotated case).
Erasing annotations never changes an accepted program's type, and if the syntax-directed checker accepts a program, the bidirectional one does too.
Neither checker crashes or loops on any parsed program; each is linear in the program size times the size of the types involved.

4. The corpus and the measurement (L3)¶

corpus/*.bic holds one program per file with header lines:

Header	Meaning
`# sd: <type>` or `# sd: error L:C`	what `checkSyntaxDirected` must return
`# bd: …`	the same for `checkBidirectional`
`# value: v`	the program is well typed; `evaluate` prints `v`
`# blame: L:C`	the program is ill typed; `L:C` is where the actual mistake is
`# gradual: value v` or `# gradual: blame L:C`	★ L5: the result of `evaluate(insertCasts(P))`

Files 01–12 are well typed, 20–29 ill typed, 40–45 gradual. Positions count lines from the top of the file, header lines included.

ch06-bidir-measure corpus (provided, tools/measure.cpp) prints, for each well-typed program, the minimal number of annotations each checker needs (exhaustively over all subsets of the written annotations: the smallest set that, with every other annotation erased, is still accepted with the same type), and for each ill-typed program whether each checker's error position equals the blame header. It exits 1 if a checker disagrees with an sd/bd header. Record your totals in the chapter's exercise answers: the reference solution prints

annotations written: 32; needed by syntax-directed: 24; by bidirectional: 9
ill-typed programs: 10; error at the blamed position: syntax-directed 5, bidirectional 10

Performance target: the whole measurement runs in under a second (it type-checks each program up to \(2^{n}\) times for \(n \le 7\) annotations).

5. ★ L4 — algorithmic subtyping (`include/bidir/Subtyping.h`, your code in `extras/`)¶

Implement bool isSubtype(const Type &S, const Type &T) for types without ?: top above everything, bot below everything, int and bool only below themselves, functions contravariant in the parameter and covariant in the result, records with width, depth and permutation. It must be Algorithm 6.5.4 — a syntax-directed procedure with no transitivity rule and no search — and terminate on all inputs.

The tests compare it with an oracle: the declarative relation of Definition 6.5.2 (with reflexivity and transitivity) computed as a least fixed point over all 2705 types of up to 5 nodes over int, bool, top, bot, arrows and records with labels a, b; every one of the 180 625 pairs of types of up to 4 nodes must agree (10 061 of them are subtypes). Theorem 6.5.13 says they agree on all types; the test checks it where it can.

6. ★ L5 — gradual typing by cast insertion (`include/bidir/Gradual.h`, your code in `extras/`)¶

6.1 Contract¶

std::expected<Program, Diagnostic> insertCasts(const Program &P);
std::expected<Type, Diagnostic> checkGradual(const Program &P);

insertCasts returns P with Cast nodes added (Algorithm 6.7.4); checkGradual returns the type of the result. Build a Cast as a new Term with K = TermKind::Cast, From = the source type, Ann = the target type, Kids = {the wrapped term}, the wrapped term's Line/Col, and Blame = "line:col" of the wrapped term; replace the child index in the parent (or Root).

6.2 Gradual rules (Lesson 6.7, Definitions 6.7.2–6.7.3)¶

The checker is syntax-directed (like L1) with consistency \(\sim\) instead of equality; an unannotated lambda parameter has type ?. A cast \(\langle S \Rightarrow T\rangle\) is inserted exactly where a subterm of type \(S\) is used at a consistent but different type \(T\) — never between equal types:

Term	Rule, casts
`e1 e2`, \(e_1 : A \to B\)	\(e_2 : S\) with \(S \sim A\); cast \(e_2\) to \(A\); result \(B\)
`e1 e2`, \(e_1 :\) `?`	\(e_2 : S\); cast \(e_1\) to \(S \to\) `?`; result `?`
`(e : T)`, `let x: T = e …`	\(e : S\), \(S \sim T\); cast \(e\) to \(T\)
`+ - <`	each operand \(\sim\) `int`, cast to `int`
`if c then a else b`	\(c \sim\) `bool` (cast); \(A \sim B\); result \(A \sqcap B\), both branches cast to it
`e1 == e2`	as in §3.1 with `?` allowed on either side; if exactly one side is `?`, cast it to the other side's type
`e.l`, \(e :\) `?`	result `?`; checked when it runs

A type error is reported like in §3.1, at the subterm whose type is not consistent (e.g. true + 1 at true).

6.3 The evaluator (provided)¶

evaluate runs casts as Definition 6.7.5: a cast to ? injects the value with its type; a cast from ? checks the injected type (and recursively casts it); a cast between function types wraps the function, and calling the wrapper casts the argument backwards and the result forwards with the same label; record casts go field by field. A failing cast stops the program with blame <label>. The tests check:

the six gradual corpus files (# gradual: headers);
programs without ? get no casts, the same type as L1, and the same value (Theorem 6.7.8);
the gradual guarantee (Theorem 6.7.7): every well-typed corpus program and 200 random programs keep their value when every annotation is replaced by ?;
if returns the meet: L5_IfResultIsTheMeet.

7. What the tests check (`tests/ch06/unit/BidirTest.cpp`)¶

Test	Checks
`Provided_*`	the parser, printer and annotation erasure (pass from the start)
`L1_SyntaxDirectedCorpus`, `L1_HandCases`	every `# sd:` header; types and error positions of §3.1
`L2_BidirectionalCorpus`, `L2_HandCases`	every `# bd:` header; checking mode through annotations, `let`, `if`, records, but not through application or projection
`L3_BothAcceptFullyAnnotatedProgramsWithTheSameType`	300 random fully annotated programs
`L3_ErasureNeverChangesTheTypeAndBidirectionalAcceptsMore`	> 1000 random erasures: an accepted type is the original type; SD accepts ⇒ BD accepts; BD accepts more than 50 that SD rejects
`L4_*` ★	hand cases; agreement with the declarative oracle on all small types
`L5_*` ★	§6.3
`ch06.lab.measure-smoke`	`ch06-bidir-measure corpus` exits 0

8. Milestones¶

Milestone	Command	Passes when
L1	`ctest --preset linux -R 'Bidir.L1'`	the syntax-directed checker matches §3.1
L2	`-R 'Bidir.L2'`	the bidirectional checker matches §3.2
L3	`-R 'Bidir.L3'` and `ch06-bidir-measure labs/ch06-bidir/corpus`	the properties of §3.3 hold; you have the numbers of §4 and can explain each difference
L4 ★	`-R 'Bidir.L4'`	subtyping agrees with the oracle
L5 ★	`-R 'Bidir.L5'`	casts, blame and the guarantee

(--preset macos on macOS.)

9. Hints¶

Hint 1 — where to start

Write L1 as one recursive function type(int node) -> CheckResult with a switch on TermKind, and a context that is a vector of (name, type) pairs searched from the back (push at fn and let, pop after the body). Return early on the first error: if (!T) return T;.

Hint 2 — the key idea

L2 is two mutually recursive functions, synth(node) and check(node, type). check handles fn, if, let and records itself, and ends with the mode switch for everything else: synth then compare. The only place an expected type enters synthesis is an annotation ((e : T), let x: T) or a parameter type at an application. If an L2 corpus file fails, print which mode each subterm is visited in and compare with the rules table.

Hint 3 — a design sketch

L4: switch on the shape of the pair. T is top or S is bot: true. Two arrows: recurse on (T's parameter, S's parameter) and (S's result, T's result). Two records: for every label of T, S must have it with a subtype. L5: one function type(node, parent, slot) that returns the node's type and may replace parent.Kids[slot] by a cast; a helper expect(node, slot, want) that types a child, checks consistency and inserts the cast. Copy what you need from Nodes[i] before recursing: pushing a cast node can reallocate the vector.

10. Stretch goals¶

Add polymorphic let with explicit type application and implement local type-argument synthesis (Algorithm 6.4.6).
Add subsumption to the bidirectional checker (L2 + L4): replace the mode switch's equality by isSubtype, and find a program the syntax-directed checker with subsumption cannot type without a search.
★ Give casts two blame labels with polarity [WF09] and make corpus 42 blame the caller.