Chapter 6 exercises

You implement pebblec's type checker: the type of every declaration and expression, checked bidirectionally, with Pebble's one implicit conversion (the literal rule), places and reference arguments, the exclusivity rule, every type error at the position pebble-spec §13.3 prescribes, and no cascades. In the comparison lab you write a syntax-directed and a bidirectional checker for one small calculus and measure the difference; the ★ milestones add algorithmic subtyping against a brute-force oracle and gradual typing with cast insertion.

• The contract is one function of pebble/include/pebble/Sema/Sema.h: typeCheck(ModuleDecl*, ASTContext&, DiagnosticEngine&). It must set TypedDecl::setType on every variable, parameter and field, FunctionDecl::setReturnType, Expr::setType on every expression (the error type for ill-typed ones), and MemberExpr::setField. The rules are §5 and §7–§9 of the Pebble specification; the positions and notes of every diagnostic are §13.3; the type table the golden tests compare is §14.4 (printed by the provided dumpTypeTable, TypeTable.h).
• Your code goes anywhere under pebble/lib/Sema/Types/src/ (switch types). It starts with a Stub.cpp whose function stops with TODO(ch06): E1-E6: implement the bidirectional type checker (typeCheck); replace it and add files as you like.
• Provided: the lexer, parser and name resolution (Chapters 1, 4, 5; build with -DPEBBLE_USE_SOLUTION=lexer,parser,names if you skipped them), the AST with semantic types from the ASTContext (getIntType(), getFloatType(), getArrayType(T, N), getRefType(T, Mut), getErrorType(), …), the diagnostics E0401–E0424 and E0312 with the notes note_expected_due_to, note_declared_here, note_mut_argument_here, note_first_initialized_here, the tool ch06-typecheck, and the corpus tests/ch06/Inputs/ with golden .typed files.
• The lab is specified in labs/ch06-bidir/SPEC.md (contracts include/bidir/Bic.h, ★ Subtyping.h, ★ Gradual.h; milestones L1–L5); this page only orders it.

./course test 6                                                   # builds, then runs every test labelled ch06
ctest --preset linux -L '^ch06$' -R 'Types.E3'                    # one group while iterating (macOS: --preset macos)
build/linux/bin/ch06-typecheck tests/ch06/Inputs/basics.pbl       # your type table and diagnostics on any file
build/linux/bin/pebblec --emit=typed-ast tests/ch06/Inputs/calls.pbl   # the AST dump with a type on every node

Before you start, every ch06.Types.* test and ch06.lit fail with TODO(ch06): E1-E6: …, and every ch06.Bidir.* test except Provided_* with TODO(ch06). The golden tables were produced by the reference checker and cross-checked against an independent Python checker (tools/course/lib/pebble_types.py, run by tests/ch06/update_goldens.py); the diagnostics of the err-*.pbl lit tests were written by hand from §13.3.

Stuck? Work through the hints in order. The reference solution is in solutions/pebble/lib/Sema/Types/src/ (one possible design: a Checker class with synth and check, in four files); look at it only after you pass the tests, or after an honest hour.

---

E1 · Declarations and written types

Contract: typeCheck, first pass over items · Spec: pebble-spec §5, §6.2 · Tests: ch06.Types.E1_*, lit err-decls.test · Lessons: 6.1, 6.3

Give every struct field, parameter and function result its type (the TypeReprs were resolved by Chapter 5), before checking any body, so that calls and struct literals can be checked in any order. Reject [T; 0] (E0419, at the length literal), reference types anywhere but a parameter's outermost type (E0420), extern signatures with non-scalar or reference types (E0418, at the offending type), and a main whose signature is not fn main() -> int (E0312, at the name). An invalid written type becomes the error type.

Hint 1 — where to start

Two passes over ModuleDecl: pass 1 sets field, parameter and result types; pass 2 checks bodies. Write a helper validType(TypeRepr*, Position) that walks the repr (arrays nest) and reports E0419/E0420.

Hint 2 — the key idea

A reference type is valid exactly as the outermost type of a parameter: fn f(p: &[int; 4]) is fine, fn f(p: [∫ 4]), let r: &int and -> &int are E0420. Pass "is this a parameter's top level" down the walk.

E2 · Synthesis: literals, names, operators, casts, conditions

Contract: expression synthesis · Spec: pebble-spec §8.2–§8.5, §8.7 · Tests: ch06.Types.E2_*, lit basics.test, err-operators.test · Lessons: 6.3 (Algorithm 6.3.3)

Synthesize the type of every expression bottom-up: literals, names (the declaration's type; a reference parameter denotes its referent's type), arithmetic (+ - * / % and the wrapping &+ &- &* on two ints; + - * / % on two floats, §8.3–§8.4), bitwise and shift operators on int, comparisons, ==/!= on equal scalar types (E0422 for a non-scalar operand, E0402 for two different scalars), &&/||/! on bool, casts by the table of §8.7 (E0404), and conditions of if/while (E0410). Operator errors point at the operator (E0402, E0403). Integer literals above \(2^{63} - 1\) are E0424, except 9223372036854775808 directly under unary minus.

Hint 1 — where to start

One synth(Expr*) -> Type* with a switch on the expression kind, calling E->setType(T) before returning. Get the literals and names right first; basics.pbl needs little else.

Hint 2 — the key idea

The negative-literal exception is a property of the parent: when synthesizing unary -, look at whether the operand is an integer literal with that exact value before checking the literal's range.

E3 · Checking mode: expected types, the literal rule, notes, local inference

Contract: expression checking · Spec: pebble-spec §7, §8.1 (the propagation table) · Tests: ch06.Types.E3_*, lit literals.test, err-mismatch.test · Lessons: 6.4 (Algorithm 6.4.4)

Add check(Expr*, Type* Expected, Origin): an integer literal checked against float has type float (the only implicit conversion); the expected type is passed into parentheses, unary -, the operands of + - * / %, array literal elements and repeat values, and nowhere else — everywhere else synthesize and compare (E0401 at the start of the expression). The note "expected 'T' because of this" points at the annotation that set the expected type (a let/var annotation, a parameter type, the result type, a field type) and is absent for assignments, indices, for bounds and array elements in synthesis mode. let x = e without annotation takes e's synthesized type (Chapter 7 re-derives this as inference). return; in a function with a result is E0401 at the return.

Hint 1 — where to start

Implement check as: handle the forms of the propagation table; for anything else, T = synth(E) and compare. Then replace every "synthesize and compare with an annotation" in your statements with a check call.

Hint 2 — the key idea

Carry the note's position with the expected type: a small struct Origin { const TypeRepr *Annotation; } (null when there is no note) passed down unchanged through parentheses and operators, so that an error deep inside let v: [float; 2] = [1, -(n + 3)]; still notes the annotation.

E4 · Aggregates and places

Contract: arrays, structs, indexing, fields, categories · Spec: pebble-spec §8.8, §9.1–§9.2, §14.4 (categories) · Tests: ch06.Types.E4_*, lit aggregates.test · Lessons: 6.8 (Definition 6.8.1)

Array literals (non-empty: E0423; elements of one type, checked against the first element's type in synthesis mode), repeats [e; n], indexing (an array base: E0406; an int index), struct literals (every field exactly once in any order: E0407, E0408 once per missing field, E0409 with a note at the first initializer), field access (resolve MemberExpr::setField; E0407), and the category of every expression (value, place, mut-place) that the type table prints.

Hint 1 — where to start

The category is not stored in the AST: dumpTypeTable computes it from the tree (a name, a field or element of a place, or a parenthesized place). What you must get right is the types; read TypeTable.cpp to see the category rule you will reuse in E5.

E5 · Calls and reference arguments

Contract: calls, print/write, references, exclusivity · Spec: pebble-spec §8.6, §9.3, §10 · Tests: ch06.Types.E5_*, lit calls.test, references.test, err-calls.test · Lessons: 6.4, 6.8 (Algorithms 6.8.2 and 6.8.4)

Check argument counts (E0405 at the callee, note at the function's name), check each by-value argument against its parameter (so literals get the literal rule), require &place/&mut place for reference parameters with the same mode (E0411), a place operand (E0412), a mutable root for &mut (E0413, note at the declaration) and the exact parameter type; reject a root passed as &mut that appears in any other argument of the same call (E0414, once per call and variable, with the note at the &mut argument's root). print/write take one scalar or interpolated string (E0417); an interpolated string elsewhere is E0415. A call returning () in a value position is E0421.

Hint 1 — where to start

Write checkArgument(Arg, Param) following Algorithm 6.8.2, then checkExclusivity(Call) following Algorithm 6.8.4 as a separate pass over the arguments after all of them are typed.

Hint 2 — the key idea

For E0414, collect the name occurrences of each argument in source order (a small recursive visitor over the argument's expression tree, indices included), and keep a set of roots already reported for this call.

E6 · No cascades, totality, robustness

Contract: the error type everywhere · Spec: pebble-spec §13.3 ("The error type") · Tests: ch06.Types.E6_*, ch06.Types.Robust_*, lit err-cascade.test, spec-examples.test, pebblec-typed-ast.test · Lessons: 6.3 (Definition 6.3.2, Proposition 6.3.9)

Every expression gets a type, even inside ill-typed code, and every mistake is reported exactly once: no rule reports anything when a type involved is <error>. The tests generate random well-typed programs (accepted with the generated types), mutate one literal of each (exactly one error), and run every .pbl of Chapters 4–6 through typeCheck without crashing.

Hint 1 — the key idea

Make one helper compatible(A, B) that returns true if either is the error type, and use it for every comparison; make every "bad operand" check return early when an operand is the error type. Then grep your code for == on types.

---

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

Specified in labs/ch06-bidir/SPEC.md. Order: L1 (syntax-directed, after Lesson 6.3) → L2 (bidirectional, after Lesson 6.4) → L3 (the measurement with ch06-bidir-measure; write down your totals and explain each program where the two checkers differ) → L4 ★ (algorithmic subtyping, after Lesson 6.5) → L5 ★ (gradual typing, after Lesson 6.7). The reference solution's measurement is in the chapter README.