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 inenv("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(orcond_type/then_type/else_type) by callingtype_ofon the children before checking the rule. "=="requires MATCHING types on both sides (not necessarilyint) --int == intandbool == boolare both fine,int == boolis not.conddoesn't have to be a literal("bool", ...)-- anything that type-checks to"bool"(a comparison, a nestedif, ...) 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.