Capstone: designing and implementing a small language · CMPUT-325 Lesson 12

This final lesson puts the course together by designing and implementing a complete small language, which we call Mini. It is a typed functional language with integers, Booleans, first-class functions, local definitions and recursion. Building it end to end uses nearly every idea from the course: a grammar and a parser (lesson 2), operational semantics (lesson 3), environments and closures (lesson 4), the lambda calculus and call-by-value evaluation (lessons 5 and 6), a static type system and its soundness (lesson 7), and testing an implementation against a specification. Each stage is a few dozen lines of Python, and the whole implementation is under 250 lines. The same pipeline, with more stages and a code generator at the end, is the subject of CMPUT-415.

Step 1: write the specification first

A language is easiest to implement, and to get right, if its definition is written down before any code. For Mini that means three things: the concrete syntax as a grammar, the static semantics as typing rules, and the dynamic semantics as evaluation rules. Decisions that look minor at this stage, such as whether comparison associates, whether function parameters carry type annotations, and whether evaluation is call by value, shape every later stage.

\[\begin{aligned} e \;::=\;& n \mid \mathtt{true} \mid \mathtt{false} \mid x \mid e \oplus e \mid \mathtt{if}\ e\ \mathtt{then}\ e\ \mathtt{else}\ e \\ \mid\;& \mathtt{fun}\ (x : \tau) \to e \mid e\ e \mid \mathtt{let}\ x = e\ \mathtt{in}\ e \mid \mathtt{let\ rec}\ f\ (x : \tau) : \tau = e\ \mathtt{in}\ e \\ \tau \;::=\;& \mathtt{int} \mid \mathtt{bool} \mid \tau \to \tau \end{aligned}\]

Precedence and associativity are part of the specification. Application binds tightest and associates to the left, so f x y means (f x) y, as in ML and Haskell. Multiplication binds tighter than addition and subtraction, which associate to the left. Comparison is non-associative, so 1 < 2 < 3 is a syntax error rather than a confusing comparison of a Boolean with an integer. The arrow in types associates to the right, so int -> int -> int means int -> (int -> int), the curried form. Requiring type annotations on function parameters keeps the type checker a simple bottom-up pass; adding the inference of lesson 8 would remove them.

Step 2: lexer and parser

The lexer turns characters into tokens with a single regular expression, recording each token's column for error messages. The parser is recursive descent: one method per grammar level, from expr down to atom, each calling the next level for its operands, exactly as in lesson 2. Loops in sum and product build left-associative trees; the single if in comparison makes it non-associative; the recursive call in type_ makes the arrow right-associative. Every error names the column and what was expected, which matters more to users than any other feature of an implementation.

Mini's lexer and recursive-descent parser

# Mini, part 1: a lexer and a recursive-descent parser producing an abstract syntax tree.
import re
TOKEN = re.compile(r"\s*(?:(\d+)|([A-Za-z_]\w*)|(->|[-+*<=():]))")
KEYWORDS = {"let", "rec", "in", "fun", "if", "then", "else", "true", "false", "int", "bool"}

class MiniError(Exception): pass

def tokenize(src):
    pos, toks = 0, []
    while True:
        m = TOKEN.match(src, pos)
        if not m:
            rest = src[pos:].lstrip()
            if not rest: break
            col = len(src) - len(rest) + 1
            raise MiniError(f"lexical error at column {col}: unexpected {rest[0]!r}")
        pos = m.end()
        num, word, sym = m.groups()
        if num: toks.append(("int", int(num), m.start(1)))
        elif word: toks.append(("kw" if word in KEYWORDS else "id", word, m.start(2)))
        else: toks.append(("sym", sym, m.start(3)))
    toks.append(("eof", None, len(src)))
    return toks

class Parser:
    def __init__(self, src): self.toks, self.i = tokenize(src), 0
    def peek(self): return self.toks[self.i]
    def at(self, *vals): return self.peek()[0] in ("kw", "sym") and self.peek()[1] in vals
    def fail(self, wanted):
        kind, val, pos = self.peek()
        found = "end of input" if kind == "eof" else repr(val)
        raise MiniError(f"syntax error at column {pos + 1}: expected {wanted}, found {found}")
    def eat(self, val=None, kind=None):
        k, v, _ = self.peek()
        if val is not None and not self.at(val): self.fail(repr(val))
        if kind is not None and k != kind: self.fail(kind)
        self.i += 1
        return v

    def program(self):
        e = self.expr()
        if self.peek()[0] != "eof": self.fail("end of input")
        return e
    def expr(self):
        if self.at("let"):
            self.eat("let")
            if self.at("rec"):                    # let rec f (x: t1) : t2 = body in rest
                self.eat("rec"); f = self.eat(kind="id"); self.eat("(")
                x = self.eat(kind="id"); self.eat(":"); tx = self.type_(); self.eat(")")
                self.eat(":"); tr = self.type_(); self.eat("=")
                body = self.expr(); self.eat("in")
                return ("letrec", f, x, tx, tr, body, self.expr())
            x = self.eat(kind="id"); self.eat("="); e1 = self.expr(); self.eat("in")
            return ("let", x, e1, self.expr())
        if self.at("fun"):                        # fun (x: t) -> body
            self.eat("fun"); self.eat("("); x = self.eat(kind="id"); self.eat(":")
            t = self.type_(); self.eat(")"); self.eat("->")
            return ("fun", x, t, self.expr())
        if self.at("if"):
            self.eat("if"); c = self.expr(); self.eat("then"); a = self.expr(); self.eat("else")
            return ("if", c, a, self.expr())
        return self.comparison()
    def comparison(self):                         # non-associative: a < b < c is an error
        e = self.sum()
        if self.at("<", "="):
            op = self.eat(); e = (op, e, self.sum())
        return e
    def sum(self):                                # left-associative + and -
        e = self.product()
        while self.at("+", "-"):
            op = self.eat(); e = (op, e, self.product())
        return e
    def product(self):
        e = self.application()
        while self.at("*"):
            self.eat(); e = ("*", e, self.application())
        return e
    def application(self):                        # juxtaposition binds tightest, to the left
        e = self.atom()
        while self.peek()[0] in ("int", "id") or self.at("(", "true", "false"):
            e = ("app", e, self.atom())
        return e
    def atom(self):
        kind, val, _ = self.peek()
        if kind == "int": self.i += 1; return ("num", val)
        if self.at("true", "false"): self.i += 1; return ("bool", val == "true")
        if kind == "id": self.i += 1; return ("var", val)
        if self.at("("):
            self.eat("("); e = self.expr(); self.eat(")"); return e
        self.fail("an expression")
    def type_(self):                              # t ::= int | bool | t -> t | (t)
        if self.at("("):
            self.eat("("); t = self.type_(); self.eat(")")
        elif self.at("int", "bool"):
            t = self.eat()
        else:
            self.fail("a type")
        if self.at("->"):
            self.eat("->"); return ("->", t, self.type_())   # right-associative
        return t

def parse(src): return Parser(src).program()

Output

$ python3 parse_demo.py
1 + 2 * 3 - 4
    (- (+ 1 (* 2 3)) 4)
f x y + g 2
    (+ (app (app f x) y) (app g 2))
fun (f: int -> int) -> f (f 1)
    (fun f (int -> int) (app f (app f 1)))
let rec fact (n: int) : int = if n < 1 then 1 else n * fact (n - 1) in fact 5
    (letrec fact n int int (if (< n 1) 1 (* n (app fact (- n 1)))) (app fact 5))
(1 + 2         syntax error at column 7: expected ')', found end of input
let x = in 3   syntax error at column 9: expected an expression, found 'in'
1 < 2 < 3      syntax error at column 7: expected end of input, found '<'
3 $ 4          lexical error at column 3: unexpected '$'

Parsing sample programs to abstract syntax, and four syntax errors with their columns

from mini import *

def sexp(e):
    if isinstance(e, str): return e                      # names and base types
    if e[0] == "->": return f"({sexp(e[1])} -> {sexp(e[2])})"
    if e[0] in ("num", "bool"): return str(e[1]).lower()
    if e[0] == "var": return e[1]
    return "(" + " ".join([e[0]] + [sexp(a) for a in e[1:]]) + ")"

for src in ["1 + 2 * 3 - 4",
            "f x y + g 2",
            "fun (f: int -> int) -> f (f 1)",
            "let rec fact (n: int) : int = if n < 1 then 1 else n * fact (n - 1) in fact 5"]:
    print(f"{src}\n    {sexp(parse(src))}")
for bad in ["(1 + 2", "let x = in 3", "1 < 2 < 3", "3 $ 4"]:
    try: parse(bad)
    except MiniError as err: print(f"{bad:14} {err}")

Output

$ python3 parse_demo.py
1 + 2 * 3 - 4
    (- (+ 1 (* 2 3)) 4)
f x y + g 2
    (+ (app (app f x) y) (app g 2))
fun (f: int -> int) -> f (f 1)
    (fun f (int -> int) (app f (app f 1)))
let rec fact (n: int) : int = if n < 1 then 1 else n * fact (n - 1) in fact 5
    (letrec fact n int int (if (< n 1) 1 (* n (app fact (- n 1)))) (app fact 5))
(1 + 2         syntax error at column 7: expected ')', found end of input
let x = in 3   syntax error at column 9: expected an expression, found 'in'
1 < 2 < 3      syntax error at column 7: expected end of input, found '<'
3 $ 4          lexical error at column 3: unexpected '$'

The trees confirm the precedence rules: 1 + 2 * 3 - 4 groups the multiplication first and the subtraction last, and f x y + g 2 applies f to x and then to y before adding. The four bad inputs are caught at the right places, including the deliberate non-associativity of comparison.

The Mini pipeline: each stage either passes a richer structure on or reports an error

Step 3: the type checker

The type checker implements the typing rules of lesson 7 as one recursive function. It takes an expression and an environment mapping variables to types, and either returns the expression's type or raises a type error. Because parameters are annotated, every rule is syntax directed: the form of the expression determines which rule applies, and the types of the parts determine the type of the whole. The let rec rule is the only subtle one: the body of a recursive function is checked in an environment that already contains the function itself, at its declared type.

Mini's type checker

# Mini, part 2: a type checker. Function parameters carry annotations, so checking is
# one bottom-up pass over the tree (lesson 7), with no inference needed.
def show_type(t):
    if isinstance(t, str): return t
    left = show_type(t[1])
    return f"({left}) -> {show_type(t[2])}" if isinstance(t[1], tuple) else f"{left} -> {show_type(t[2])}"

def expect(actual, wanted, what):
    if actual != wanted:
        raise MiniError(f"type error: {what} has type {show_type(actual)}, expected {show_type(wanted)}")

def check(e, env):
    tag = e[0]
    if tag == "num": return "int"
    if tag == "bool": return "bool"
    if tag == "var":
        if e[1] not in env: raise MiniError(f"type error: unbound variable {e[1]}")
        return env[e[1]]
    if tag in ("+", "-", "*", "<"):
        expect(check(e[1], env), "int", f"left operand of {tag}")
        expect(check(e[2], env), "int", f"right operand of {tag}")
        return "bool" if tag == "<" else "int"
    if tag == "=":
        t1, t2 = check(e[1], env), check(e[2], env)
        if t1 not in ("int", "bool"): raise MiniError(f"type error: cannot compare values of type {show_type(t1)}")
        expect(t2, t1, "right operand of =")
        return "bool"
    if tag == "if":
        expect(check(e[1], env), "bool", "condition of if")
        t1, t2 = check(e[2], env), check(e[3], env)
        expect(t2, t1, "else branch")
        return t1
    if tag == "fun":
        return ("->", e[2], check(e[3], {**env, e[1]: e[2]}))
    if tag == "app":
        tf, ta = check(e[1], env), check(e[2], env)
        if not isinstance(tf, tuple): raise MiniError(f"type error: applying a value of type {show_type(tf)}")
        expect(ta, tf[1], "argument")
        return tf[2]
    if tag == "let":
        return check(e[3], {**env, e[1]: check(e[2], env)})
    if tag == "letrec":
        _, f, x, tx, tr, body, rest = e
        ft = ("->", tx, tr)
        expect(check(body, {**env, f: ft, x: tx}), tr, f"body of {f}")
        return check(rest, {**env, f: ft})
    raise MiniError(f"unknown construct {tag}")

Output

$ python3 check_demo.py
fun (x: int) -> x < 10
    : int -> bool
fun (f: int -> int) -> fun (x: int) -> f (f x)
    : (int -> int) -> int -> int
let rec fact (n: int) : int = if n < 1 then 1 else n * fact (n - 1) in fact
    : int -> int
1 + true
    type error: right operand of + has type bool, expected int
if 1 then 2 else 3
    type error: condition of if has type int, expected bool
let f = fun (x: int) -> x in f true
    type error: argument has type bool, expected int
if true then 1 else false
    type error: else branch has type bool, expected int
let rec loop (n: int) : bool = n + 1 in loop 0
    type error: body of loop has type int, expected bool
3 4
    type error: applying a value of type int
let x = 5 in y
    type error: unbound variable y

The checker assigns types to good programs and explains why bad ones are rejected

from mini import *
for src in ["fun (x: int) -> x < 10",
            "fun (f: int -> int) -> fun (x: int) -> f (f x)",
            "let rec fact (n: int) : int = if n < 1 then 1 else n * fact (n - 1) in fact",
            "1 + true",
            "if 1 then 2 else 3",
            "let f = fun (x: int) -> x in f true",
            "if true then 1 else false",
            "let rec loop (n: int) : bool = n + 1 in loop 0",
            "3 4",
            "let x = 5 in y"]:
    try:
        print(f"{src}\n    : {show_type(check(parse(src), {}))}")
    except MiniError as err:
        print(f"{src}\n    {err}")

Output

$ python3 check_demo.py
fun (x: int) -> x < 10
    : int -> bool
fun (f: int -> int) -> fun (x: int) -> f (f x)
    : (int -> int) -> int -> int
let rec fact (n: int) : int = if n < 1 then 1 else n * fact (n - 1) in fact
    : int -> int
1 + true
    type error: right operand of + has type bool, expected int
if 1 then 2 else 3
    type error: condition of if has type int, expected bool
let f = fun (x: int) -> x in f true
    type error: argument has type bool, expected int
if true then 1 else false
    type error: else branch has type bool, expected int
let rec loop (n: int) : bool = n + 1 in loop 0
    type error: body of loop has type int, expected bool
3 4
    type error: applying a value of type int
let x = 5 in y
    type error: unbound variable y

The rejected program let rec loop (n: int) : bool = n + 1 in loop 0 shows the checker using the declared return type: the body has type int, which does not match bool. If Mini inferred return types instead, recursion would need the unification machinery of lesson 8.

Step 4: the interpreter

The interpreter is a direct transcription of big-step, call-by-value operational semantics with environments. Functions evaluate to closures that capture the environment of their definition, so Mini has lexical scope (lesson 4). The let rec case ties the knot: it creates the closure first, then adds the closure to its own environment, so that the body can call itself. The arithmetic and conditional cases still check the kinds of values they receive and raise Stuck otherwise. If the type system is sound, those checks can never fire on a program that passed the checker, and the testing below confirms that on thousands of programs.

Mini's environment-based interpreter and the full pipeline

# Mini, part 3: an environment-based interpreter (big-step semantics, lesson 3).
import sys
sys.setrecursionlimit(20000)

class Closure:
    def __init__(self, param, body, env): self.param, self.body, self.env = param, body, env

class Stuck(Exception): pass             # raised only if the type checker has let an error through

def evaluate(e, env):
    tag = e[0]
    if tag in ("num", "bool"): return e[1]
    if tag == "var": return env[e[1]]
    if tag in ("+", "-", "*", "<"):
        a, b = evaluate(e[1], env), evaluate(e[2], env)
        if type(a) is not int or type(b) is not int: raise Stuck(f"{tag} applied to {a!r}, {b!r}")
        return {"+": a + b, "-": a - b, "*": a * b, "<": a < b}[tag]
    if tag == "=":
        a, b = evaluate(e[1], env), evaluate(e[2], env)
        if type(a) is not type(b) or isinstance(a, Closure): raise Stuck("bad comparison")
        return a == b
    if tag == "if":
        c = evaluate(e[1], env)
        if type(c) is not bool: raise Stuck(f"if on {c!r}")
        return evaluate(e[2] if c else e[3], env)
    if tag == "fun": return Closure(e[1], e[3], env)
    if tag == "app":
        f, a = evaluate(e[1], env), evaluate(e[2], env)
        if not isinstance(f, Closure): raise Stuck(f"applying {f!r}")
        return evaluate(f.body, {**f.env, f.param: a})
    if tag == "let":
        return evaluate(e[3], {**env, e[1]: evaluate(e[2], env)})
    if tag == "letrec":                  # tie the knot: the closure's environment contains itself
        _, f, x, tx, tr, body, rest = e
        rec_env = dict(env)
        clo = Closure(x, body, rec_env)
        rec_env[f] = clo
        return evaluate(rest, {**env, f: clo})

def show_value(v):
    return "<fun>" if isinstance(v, Closure) else str(v).lower()

def run(src):
    tree = parse(src)                    # 1. syntax
    t = check(tree, {})                  # 2. static semantics: reject before running
    return show_value(evaluate(tree, {})), show_type(t)   # 3. dynamic semantics

Output

$ python3 eval_demo.py
factorial   2432902008176640000 : int
fibonacci                  6765 : int
twice                        63 : int
partial                   <fun> : int -> int
scope                        11 : int
gcd                          21 : int
even                       true : bool

Running Mini programs: recursion, higher-order functions, partial application and lexical scope

from mini import *
programs = {
    "factorial": "let rec fact (n: int) : int = if n < 1 then 1 else n * fact (n - 1) in fact 20",
    "fibonacci": "let rec fib (n: int) : int = if n < 2 then n else fib (n - 1) + fib (n - 2) in fib 20",
    "twice":     "let twice = fun (f: int -> int) -> fun (x: int) -> f (f x) in twice (fun (y: int) -> y * 3) 7",
    "partial":   "let add = fun (a: int) -> fun (b: int) -> a + b in add 2",
    "scope":     "let x = 1 in let f = fun (y: int) -> x + y in let x = 100 in f 10",
    "gcd":       "let rec gcd (a: int) : int -> int = fun (b: int) -> "
                 "if b = 0 then a else if a < b then gcd b a else gcd (a - b) b in gcd 1071 462",
    "even":      "let rec even (n: int) : bool = if n = 0 then true else if n = 1 then false "
                 "else even (n - 2) in even 1000",
}
for name, src in programs.items():
    value, t = run(src)
    print(f"{name:10} {value:>20} : {t}")

Output

$ python3 eval_demo.py
factorial   2432902008176640000 : int
fibonacci                  6765 : int
twice                        63 : int
partial                   <fun> : int -> int
scope                        11 : int
gcd                          21 : int
even                       true : bool

The scope program returns 11, not 110: the function f captured the environment in which x was 1, and the later let x = 100 creates a new binding that f never sees. Under dynamic scope the answer would be 110. The gcd program shows currying through a recursive function whose declared result type is itself a function type.

Step 5: test the implementation against the specification

An implementation is only as trustworthy as its testing. Three techniques from the course combine well. Property-based testing, as in QuickCheck (Koen Claessen and John Hughes, 2000), generates thousands of random inputs and checks a property on each; here the generator builds random well-typed programs directly, and the property is type soundness: progress and preservation (lesson 7) together say that a well-typed program never gets stuck and produces a value of its type. Differential testing compares two independent implementations, here our interpreter and a translation of each program into Python, and was used at scale by the Csmith project, which found hundreds of bugs in GCC and LLVM. Mutation testing breaks programs on purpose to see whether the checker notices.

Property-based, differential and mutation testing of Mini on 3,000 random programs

# Mini, part 4: testing the implementation against its own specification.
#  (a) soundness: well-typed random programs never get stuck and produce values of their type;
#  (b) differential testing: results agree with a translation of the same program into Python;
#  (c) mutation: breaking a program usually makes the checker reject it.
import random
from mini import *

rng = random.Random(325)
FN = ("->", "int", "int")

def gen(t, env, d):
    names = [x for x, tx in env.items() if tx == t]
    if d == 0 or rng.random() < 0.2:
        if names and rng.random() < 0.5: return ("var", rng.choice(names))
        if t == "int": return ("num", rng.randint(0, 9))
        if t == "bool": return ("bool", rng.random() < 0.5)
        x = f"v{len(env)}"
        return ("fun", x, "int", gen("int", {**env, x: "int"}, 0))
    k = rng.randrange(4)
    if k == 0: return ("if", gen("bool", env, d - 1), gen(t, env, d - 1), gen(t, env, d - 1))
    if k == 1:
        tx, x = rng.choice(["int", "bool", FN]), f"v{len(env)}"
        return ("let", x, gen(tx, env, d - 1), gen(t, {**env, x: tx}, d - 1))
    if k == 2 and t == "int": return ("app", gen(FN, env, d - 1), gen("int", env, d - 1))
    if t == "int": return (rng.choice("+-*"), gen("int", env, d - 1), gen("int", env, d - 1))
    if t == "bool": return (rng.choice(["<", "="]), gen("int", env, d - 1), gen("int", env, d - 1))
    x = f"v{len(env)}"
    return ("fun", x, "int", gen("int", {**env, x: "int"}, d - 1))

def to_python(e):                       # a second, independent implementation
    tag = e[0]
    if tag in ("num", "bool"): return repr(e[1])
    if tag == "var": return e[1]
    if tag in ("+", "-", "*", "<"): return f"({to_python(e[1])} {tag} {to_python(e[2])})"
    if tag == "=": return f"({to_python(e[1])} == {to_python(e[2])})"
    if tag == "if": return f"({to_python(e[2])} if {to_python(e[1])} else {to_python(e[3])})"
    if tag == "fun": return f"(lambda {e[1]}: {to_python(e[3])})"
    if tag == "app": return f"({to_python(e[1])})({to_python(e[2])})"
    if tag == "let": return f"(lambda {e[1]}: {to_python(e[3])})({to_python(e[2])})"

def mutate(e):                          # replace one random integer literal with true
    spots = []
    def walk(n, path):
        if isinstance(n, tuple) and n and n[0] == "num": spots.append(path)
        elif isinstance(n, tuple) and n[0] not in ("var", "bool"):
            for i, c in enumerate(n):
                if isinstance(c, tuple) and c and isinstance(c[0], str) and c[0] != "->": walk(c, path + [i])
    walk(e, [])
    if not spots: return None
    path = rng.choice(spots)
    def rebuild(n, p):
        if not p: return ("bool", True)
        return n[:p[0]] + (rebuild(n[p[0]], p[1:]),) + n[p[0] + 1:]
    return rebuild(e, path)

kind = {"int": int, "bool": bool}
checked = stuck = wrong_type = disagree = 0
rejected = rejected_but_would_run = 0
for _ in range(3000):
    t = rng.choice(["int", "bool"])
    prog = gen(t, {}, rng.randint(1, 6))
    assert check(prog, {}) == t
    checked += 1
    try:
        v = evaluate(prog, {})
    except Stuck:
        stuck += 1; continue
    if type(v) is not kind[t]: wrong_type += 1
    if v != eval(to_python(prog)): disagree += 1
    m = mutate(prog)
    if m is None: continue
    try:
        check(m, {})
    except MiniError:
        rejected += 1
        try: evaluate(m, {})
        except Stuck: continue
        rejected_but_would_run += 1

print(f"well-typed programs run     : {checked}")
print(f"stuck / wrong result type   : {stuck} / {wrong_type}")
print(f"disagreements with Python   : {disagree}")
print(f"mutants rejected by checker : {rejected}")
print(f"  of which would have run without getting stuck: {rejected_but_would_run}")

Output

$ python3 tests.py
well-typed programs run     : 3000
stuck / wrong result type   : 0 / 0
disagreements with Python   : 0
mutants rejected by checker : 1965
  of which would have run without getting stuck: 849

No well-typed program got stuck or produced a value of the wrong type, and the interpreter agreed with Python on every one, which is strong evidence (though not proof) that the checker and interpreter match the specification. The last line is just as instructive. Some mutated programs were rejected even though running them would not have got stuck, typically because the mutation landed in a branch that is never taken. That is the price of a sound static type system: since whether a branch runs is undecidable in general (CMPUT-474), any sound checker must reject some programs that would in fact run safely.

Step 6: extending the language

A good design leaves room to grow, and each extension touches every stage in a predictable way. Adding pairs means a new production in the grammar, a product type t1 * t2 with introduction and elimination rules, and a new kind of value. Adding lists or other algebraic data types adds pattern matching, with the exhaustiveness checking seen in Rust in lesson 7. Removing the parameter annotations means replacing the checker with Hindley–Milner inference from lesson 8. Adding mutable references needs a store in the semantics, and with polymorphism, the value restriction. Adding exceptions or generators is easiest if the interpreter is first converted to continuation-passing style, as in lesson 6. Replacing the interpreter with a compiler to the stack machine of lesson 10 gives a real, if tiny, compiler.

Design principles, revisited

Lesson 1 listed the criteria by which languages are judged: readability, writability, reliability and cost. Building Mini shows how they trade off in practice. Mandatory annotations cost writability but make error messages local and the checker simple. Non-associative comparison costs a little expressiveness and prevents a class of mistakes. Static typing rejects some safe programs in exchange for ruling out all stuck ones. Tony Hoare's 1973 advice, 'Hints on programming language design', still applies: a language should be simple, secure, fast to translate and efficient at run time, and a designer should consolidate known ideas rather than invent untried ones. Most of the influential languages of the last twenty years, from Rust and Swift to Kotlin and TypeScript, did exactly that, combining ideas from this course that were first worked out decades earlier.

Worked examples

Worked problem

Parsing with precedence

Give Mini's abstract syntax for f 2 * 3 + 4.

Show solution

Application binds tightest, so f 2 is ("app", f, 2).
Multiplication binds next: ("*", ("app", f, 2), 3).
Addition is outermost.

Answer: ("+", ("*", ("app", ("var", "f"), ("num", 2)), ("num", 3)), ("num", 4)).

Worked problem

Checking a recursive function

Type check let rec sum (n: int) : int = if n = 0 then 0 else n + sum (n - 1) in sum 4.

Show solution

Check the body with sum : int -> int and n : int.
n = 0 is bool; the then branch 0 is int.
sum (n - 1) : int, so n + sum (n - 1) : int; both branches are int, matching the declared result.
Then sum 4 in an environment with sum : int -> int has type int.

Answer: The program is well typed with type int, and evaluates to 10.

Worked problem

Closures and scope in the interpreter

What does let a = 2 in let g = fun (b: int) -> a * b in let a = 5 in g a evaluate to?

Show solution

g's closure captures the environment where a = 2.
The inner let rebinds a to 5 in the outer environment only.
g a passes 5 as b, and the body computes 2 * 5 using the captured a.

Answer: 10.

Common mistakes

MistakeWriting the interpreter first and the specification afterwards.
InsteadWrite the grammar and rules first; they decide every design question the code meets.
MistakeLetting the parser accept a < b < c and sorting it out later.
InsteadDecide associativity in the grammar; making comparison non-associative rules the case out.
MistakePutting the recursive function into its own environment after creating the closure's copy.
InsteadThe closure must capture an environment that already contains (or will be patched to contain) the function itself.
MistakeRemoving run-time checks because the type checker exists.
InsteadKeep them while testing; they are how the soundness tests detect a checker bug.
MistakeTreating passing tests as a proof of soundness.
InsteadRandom testing gives evidence; a proof needs progress and preservation over all programs.

Summary and key terms

A language implementation starts from a specification: grammar, typing rules and evaluation rules.
Precedence and associativity are design decisions recorded in the grammar.
A recursive-descent parser has one method per grammar level and reports errors with positions.
With annotated parameters, type checking is one syntax-directed pass; let rec checks the body with the function in scope.
An environment interpreter with closures gives lexical scope; let rec ties the knot.
Property-based, differential and mutation testing check soundness and agreement with the specification.
Sound static checking must reject some safe programs; extensions touch every stage in predictable ways.

Specification: A precise definition of a language's syntax, typing and evaluation.
Lexer: The stage that turns characters into tokens.
Recursive descent: Parsing with one function per grammar rule, calling each other recursively.
Non-associative operator: An operator that cannot be chained without parentheses.
Syntax-directed rule: A typing rule chosen by the form of the expression alone.
Tying the knot: Making a recursive closure's environment contain the closure itself.
Stuck state: A point where evaluation cannot proceed and no value has been reached.
Property-based testing: Checking a property on many randomly generated inputs.
Differential testing: Comparing the outputs of independent implementations on the same inputs.
Mutation testing: Deliberately altering inputs or code to check that faults are detected.

Practice problems

Work each problem on paper first, then reveal the answer to check.

Why is comparison non-associative in Mini?
Show answer
So that 1 < 2 < 3, which would compare a Boolean with an integer, is a syntax error.
What does the type int -> int -> int mean?
Show answer
int -> (int -> int): a curried function of two integers.
Why does Mini require parameter annotations?
Show answer
So type checking is a single bottom-up pass with no inference.
What environment is used to check a let rec body?
Show answer
The outer environment plus the function at its declared type and the parameter at its type.
Why does the scope program return 11?
Show answer
f captured x = 1 at its definition; the later x = 100 is a different binding.
What property does the soundness test check?
Show answer
Well-typed programs never get stuck and produce values of their declared type.
What is the second implementation in the differential test?
Show answer
A translation of each program into a Python expression evaluated by Python.
Why were some mutants rejected even though they would run?
Show answer
The mutation fell in code that never runs, and a sound checker cannot know that.
Which lessons would you need to add type inference to Mini?
Show answer
Lesson 8: unification and Hindley–Milner.
Name two changes needed to add mutable references.
Show answer
A store threaded through evaluation and a reference type, plus the value restriction if polymorphism is added.