4. Type Checking

Simple Type Checker

midcompiler-internalstype-systems

A type checker's job is to catch nonsense like "true + 3" before the program ever runs, by walking the AST and computing (or rejecting) the type of every expression. This exercise checks two types, "int" and "bool", over the same kind of AST as the Parser/Constant Folding exercises.

Node shapes:

  • ("num", value) -- an int literal
  • ("bool", value) -- a bool literal
  • ("var", name) -- a variable; look up its type in env
  • ("if", cond, then_branch, else_branch) -- a conditional expression
  • ("binop", op, left, right) -- a binary operation

Literal/variable handling is done for you. Implement:

"if": cond must type-check to "bool". then_branch and else_branch must type-check to the SAME type as each other. The result type is that shared type.

"binop":

  • "+" "-" "*" -- both operands must be "int"; result is "int"
  • "<" ">" "==" -- both operands must be the SAME type; result is "bool"
  • "and" "or" -- both operands must be "bool"; result is "bool"

Raise TypeError (with any descriptive message) when a rule is violated.

Example

type_of(("binop", "+", ("num", 2), ("num", 3)), {})   # -> "int"
type_of(("binop", "+", ("bool", True), ("num", 3)), {})  # raises TypeError
type_of(("if", ("bool", True), ("num", 1), ("bool", False)), {})  # raises TypeError

The missing link: why "if" needs its own type rule at all

You might expect type_of to just recurse into whichever branch runs -- but a type checker runs BEFORE the program runs, so it has no idea which branch actually will. It has to accept or reject the if expression's type WITHOUT knowing cond's runtime value. The only sound thing to do is require both branches to already agree on a type: if then_branch is "int" and else_branch is "bool", then type_of genuinely cannot say what type the whole expression has (it depends on a value only known at runtime), so it must reject it as an error rather than guess. This is exactly the kind of correctness question that only shows up once branching enters the language -- plain straight-line arithmetic never has to answer "what if I don't know which path executes."

Constraints

  • Recurse first: get left_type/right_type (or cond_type/then_type/ else_type) by calling type_of on the children before checking the rule.
  • "==" requires MATCHING types on both sides (not necessarily int) -- int == int and bool == bool are both fine, int == bool is not.
  • cond doesn't have to be a literal ("bool", ...) -- anything that type-checks to "bool" (a comparison, a nested if, ...) is valid.

Real-world grounding

  • TypeScript's type checker (the same job, vastly more elaborate type system, including how it unifies the types of an if/ternary's two branches): src/compiler/checker.ts

Real type checkers add generics, inference, subtyping, and union/intersection types on top of this -- but "recursively compute each subexpression's type, reject combinations that don't fit the rule, and require branches to agree" is the core loop underneath all of it.

hints
type_checker.pysign in to run
Loading...
test result

This is a preview. Sign in to run this exercise against the real tests.

Simple Type Checker — nossletter.tech