Skip to main content

Types, Compilers, and Semantic Preservation

Prerequisites: S4 lexical environments and interpreter; S1 induction. Budget: 35-50 hours. Outcome: implement a small type checker and an optimization whose preconditions are explicit.

Diagnostic​

Trace a closure that captures x=3 and is called in a scope with x=100. Explain why a conditional must not evaluate both branches. If you cannot, return to S4's abstraction and interpretation worked examples.

Define a small language first​

Use integers, booleans, addition, equality, variables, let bindings, and conditionals. Define values, evaluation order, and failure behavior before optimization. For this assignment, integer arithmetic is exact, evaluation is eager except for the selected conditional branch, and expressions have no side effects. These restrictions are deliberate proof assumptions.

A typing environment maps variables to types. Addition requires two integers and produces an integer. A conditional requires a boolean condition and branches of the same type. A variable must exist in the environment. A let binding checks its value, extends the environment for the body, and respects lexical shadowing.

Type soundness is a claim about this formal language and its rules. Progress means a well-typed closed term is a value or can take a step. Preservation means evaluation preserves its type. A passing test suite is evidence about your checker, not a proof of these theorems for an arbitrary implementation.

Worked example: checking and folding​

For let x = 2 + 3 in if x == 5 then x + 1 else 0, the binding has type Int. Equality has type Bool, and both branches have type Int, so the full expression has type Int and evaluates to 6.

Fold 2+3 to 5. Propagate x only where that binding is visible; replace the comparison with true and select the first branch. The result is 6. Under the declared pure, exact-integer semantics these steps preserve the result.

Now consider a real language expression 0 * readSensor(). Replacing it with 0 can discard an effect or exception. Similarly, reassociating floating-point addition can change results. The arithmetic identity alone is not enough; optimization must preserve the language's observable behavior.

Guided assignment​

  1. Write a grammar and AST, an evaluator, and a type checker. A simple recursive parser is sufficient.
  2. Add a constant-folding pass returning a new AST. Retain source locations for useful diagnostics.
  3. Check that the original and transformed ASTs type-check with the same type and evaluate equally.
  4. Include nested shadowing, unbound names, mismatched conditional branches, and a nonselected failing branch if your language supports an explicit error expression.
  5. Generate bounded well-typed ASTs and compare evaluator results before and after optimization. Fix and record any discovered counterexample.

Acceptance: the example evaluates to 6; 1 + true and an Int/Bool branch mismatch are rejected; shadowing does not replace the wrong variable; the optimizer preserves tested outcomes. Attach an inductive argument for constant folding over your AST cases, stating any unsupported operations.

Transfer and deeper extension​

Add a print expression. Which optimizations remain valid, and how must the observation oracle change? Check: compare both value and output sequence; elimination or reordering of effects can invalidate previously safe rules.

For further depth, lower into a small intermediate representation and add dead-code elimination using liveness. Define use/definition sets and a fixed-point computation before touching production compiler code. This is a proposed stretch task, not required for the base gate.

Sources and remediation​

Use SICP for environments, Types and Programming Languages for typing and soundness, and the author's Crafting Interpreters repository for implementation comparison. Cornell's self-guided CS 6120 is a later route into compiler passes. These sources have different scope; do not begin all simultaneously.

If your transformation fails under shadowing, draw binding identities and repair substitution before adding more optimizations. Defend a rejected optimization under the rubric.