Types Before Execution
Part 05 of From Lists to Languages · Act II, Types and Extension ·
(+ 1 "hello")should be a type error before evaluation.
Act I gave the language form, meaning, and an environment. Every error it reports is still found the same way: by running the program until something goes wrong. Part 4 ended on a program that shows the cost:
error: + expects numbers, got a
1 | ((lambda (x) (+ x 1)) (quote a))
| ^The error points inside the function, at x. But the function is fine. The mistake is the argument, (quote a), and finding that took running the program up to the point where the bad value was used. In a bigger program that point can be far away, or only reached on Tuesdays, or reached after the program has already printed, charged, or deleted something.
This post adds a type checker: a second interpretation of the same tree that runs before the evaluator. It computes what kind of value each expression produces, without producing any values. A program that doesn't check never starts.
Our language has no strings yet, so (+ 1 "hello") from the series outline becomes (+ 1 (quote hello)). It's the same mistake: adding something that isn't a number.
Types are data
A type has a shape, so it gets a schema. There are four kinds of type: numbers, quoted data, functions, and type variables, which stand for types the checker hasn't worked out yet.
// A type is data too. `rest`, when present, is the type of any
// number of extra arguments, so `+` can stay variadic.
export const TNum = Schema.TaggedStruct("TNum", {});
export const TData = Schema.TaggedStruct("TData", {});
export const TVar = Schema.TaggedStruct("TVar", {
id: Schema.Number,
});
export interface TFun {
readonly _tag: "TFun";
readonly params: ReadonlyArray<Type>;
readonly rest: Type | null;
readonly result: Type;
}
export type Type =
| typeof TNum.Type
| typeof TData.Type
| typeof TVar.Type
| TFun;
const LazyType = Schema.suspend((): Schema.Codec<Type> => Type);
export const TFun = Schema.TaggedStruct("TFun", {
params: Schema.Array(LazyType),
rest: Schema.NullOr(LazyType),
result: LazyType,
});
export const Type = Schema.Union([TNum, TData, TVar, TFun]);As with the syntax tree in Part 2, describing types as a schema makes them values that can leave the process. The type (Num) -> Num encodes as plain JSON:
{ "_tag": "TFun", "params": [{ "_tag": "TNum" }], "rest": null,
"result": { "_tag": "TNum" } }Decoding a malformed type from outside, such as one written by another tool, fails with a path to the bad part:
Schema.decodeUnknownSync(Type)({
_tag: "TFun",
params: [{ _tag: "Num" }],
rest: null,
result: { _tag: "TNum" },
});
// throws a SchemaError: none of the four shapes match,
// at ["params"][0]That is everything Schema contributes here, and it's worth being exact about. Schema can tell you that a value is a well-formed type. It can't tell you that a program has that type. That's a judgment, and our checker has to make it. A few helpers build and print types:
export const num: Type = { _tag: "TNum" };
export const data: Type = { _tag: "TData" };
export const fun = (
params: ReadonlyArray<Type>,
result: Type,
rest: Type | null = null,
): TFun => ({ _tag: "TFun", params, rest, result });// Print a type, naming its variables 'a, 'b, ... in order of
// appearance. Pass the same map to name several types consistently.
export const showType = (
t: Type,
names = new Map<number, string>(),
): string => {
switch (t._tag) {
case "TNum":
return "Num";
case "TData":
return "Data";
case "TVar": {
const letter = String.fromCharCode(97 + names.size);
if (!names.has(t.id)) names.set(t.id, `'${letter}`);
return names.get(t.id)!;
}
case "TFun": {
const params = t.params.map((p) => showType(p, names));
if (t.rest) params.push(`${showType(t.rest, names)}...`);
const result = showType(t.result, names);
return `(${params.join(", ")}) -> ${result}`;
}
}
};The rules
Before any code, here is the judgment the checker makes, one rule per kind of expression:
- A number has type
Num. - A quotation has type
Data, whatever it quotes. - A name has the type its scope gives it.
(lambda (x ...) body)has type(A ...) -> B, where eachAis the type of a parameter andBis the type of the body, checked in a scope where the parameters have those types.(f arg ...)requiresfto be a function that accepts that many arguments, and each argument to have the matching parameter's type. The call has the function's result type.
The fourth rule hides the hard part. When the checker meets (lambda (x) (+ x 1)), it doesn't know the type of x yet. It only learns it from the body, where x is passed to +.
Unknowns and unification
So each parameter starts as a fresh type variable, an unknown. As the checker walks the body, it collects facts: "this unknown must be Num", "this unknown must be a function from that to something else". The procedure that turns those facts into answers is unification:
// One checking run: a supply of fresh type variables, and what has
// been learned about them so far.
export const makeSolver = () => {
const solved = new Map<number, Type>();
let next = 0;
const fresh = (): Type => ({ _tag: "TVar", id: next++ });
// Replace solved variables, all the way down.
const resolve = (t: Type): Type => {
if (t._tag === "TVar") {
const known = solved.get(t.id);
return known ? resolve(known) : t;
}
if (t._tag !== "TFun") return t;
const rest = t.rest && resolve(t.rest);
return fun(t.params.map(resolve), resolve(t.result), rest);
};
const occurs = (id: number, t: Type): boolean =>
t._tag === "TVar" ? t.id === id
: t._tag !== "TFun" ? false
: [...t.params, t.result, ...(t.rest ? [t.rest] : [])].some(
(inner) => occurs(id, resolve(inner)),
);
const mismatch = (expected: Type, got: Type, span: Span) => {
const names = new Map<number, string>();
return new Mismatch({
expected: showType(resolve(expected), names),
got: showType(resolve(got), names),
span,
});
};
// Learn that variable `id` is `t`, unless `t` contains it.
const bind = (id: number, t: Type, span: Span): Check<void> => {
if (!occurs(id, t)) {
return Effect.sync(() => void solved.set(id, t));
}
const names = new Map<number, string>();
const variable = showType({ _tag: "TVar", id }, names);
const type = showType(resolve(t), names);
return Effect.fail(new CyclicType({ variable, type, span }));
};
// Make two types equal, or explain why they can't be.
const unify = (want: Type, got: Type, span: Span): Check<void> =>
Effect.gen(function* () {
const a = resolve(want);
const b = resolve(got);
if (a._tag === "TVar") {
if (b._tag === "TVar" && a.id === b.id) return;
return yield* bind(a.id, b, span);
}
if (b._tag === "TVar") return yield* bind(b.id, a, span);
if (a._tag !== "TFun" || b._tag !== "TFun") {
if (a._tag === b._tag) return;
return yield* mismatch(a, b, span);
}
// A variadic function can stand in for a fixed one.
const bs = a.rest
? b.rest && b.params.length === a.params.length && b.params
: paramsFor(b, a.params.length);
if (!bs) return yield* mismatch(a, b, span);
if (a.rest && b.rest) yield* unify(a.rest, b.rest, span);
for (const [i, p] of a.params.entries()) {
yield* unify(p, bs[i]!, span);
}
yield* unify(a.result, b.result, span);
});
return { fresh, resolve, unify };
};Three ideas carry the whole thing:
freshmakes a new unknown.unify(want, got)makes two types equal. If one side is an unknown, it records the other side as its answer. If both are functions, it unifies them piece by piece. If they're different concrete types, it reports a mismatch.resolvesubstitutes everything learned so far into a type.
The solver is created inside the checking Effect, so every run of that Effect starts with no unknowns.
+ is variadic, so a function type can have a rest type for extra arguments. One helper decides which parameter types a call with n arguments gets:
// The parameter types for a call with n arguments, if n is allowed.
export const paramsFor = (f: TFun, n: number) =>
n === f.params.length || (f.rest && n > f.params.length)
? Array.from({ length: n }, (_, i) => f.params[i] ?? f.rest!)
: undefined;A scope of types
The checker resolves names exactly as the evaluator does, through lexical scopes. A type scope maps each name to a way of getting its type:
// A type scope maps each name to a way of getting its type. Most
// names always give the same type; a polymorphic primitive gives a
// fresh copy each time it's mentioned.
type TypeOf = (fresh: () => Type) => Type;
export interface TypeScope {
readonly names: ReadonlyMap<string, TypeOf>;
readonly parent: TypeScope | undefined;
}
const find = (
scope: TypeScope | undefined,
name: string,
): TypeOf | undefined =>
scope === undefined ? undefined
: (scope.names.get(name) ?? find(scope.parent, name));
const arithmetic = () => fun([], num, num);
export const globalTypes: TypeScope = {
names: new Map<string, TypeOf>([
["+", arithmetic],
["*", arithmetic],
["/", arithmetic],
["pi", () => num],
["print", (fresh) => {
const a = fresh();
return fun([a], a);
}],
]),
parent: undefined,
};print returns whatever it's given, so its type is ('a) -> 'a, which is polymorphic: it works for any 'a. Each mention of print gets fresh unknowns, so (print 1) and (print (quote hi)) can appear in the same program without forcing 'a to be both Num and Data.
The checker
With unification and scopes, the checker follows the rules:
export const check = (
expr: Expr,
scope = globalTypes,
): Check<Type> =>
Effect.gen(function* () {
// A new solver for every run of this Effect.
const { fresh, resolve, unify } = makeSolver();
const infer = (e: Expr, scope: TypeScope): Check<Type> =>
Effect.gen(function* () {
switch (e._tag) {
case "Num":
return num;
case "Quote":
return data;
case "Ref": {
const typeOf = find(scope, e.name);
if (typeOf) return typeOf(fresh);
const { name: symbol, span } = e;
return yield* new UnboundName({ symbol, span });
}
case "Lambda": {
// Each parameter starts as a fresh, unknown type.
const params = e.params.map(() => fresh());
const names = new Map(
e.params.map((p, i) => [p.name, () => params[i]!]),
);
const body = { names, parent: scope };
return fun(params, yield* infer(e.body, body));
}
case "Call":
return yield* inferCall(e, scope);
}
});
const inferCall = (
e: Extract<Expr, { _tag: "Call" }>,
scope: TypeScope,
): Check<Type> =>
Effect.gen(function* () {
const f = resolve(yield* infer(e.fn, scope));
const args: Type[] = [];
for (const arg of e.args) {
args.push(yield* infer(arg, scope));
}
if (f._tag === "TVar") {
// Calling an unknown: now we know it's a function.
const result = fresh();
yield* unify(f, fun(args, result), e.fn.span);
return result;
}
if (f._tag !== "TFun") {
const expected = "a function";
const got = showType(f);
const { span } = e.fn;
return yield* new Mismatch({ expected, got, span });
}
const params = paramsFor(f, args.length);
if (!params) {
const expected = f.params.length;
const got = args.length;
const { span } = e;
return yield* new ArityError({ expected, got, span });
}
for (const [i, arg] of e.args.entries()) {
yield* unify(params[i]!, args[i]!, arg.span);
}
return f.result;
});
return resolve(yield* infer(expr, scope));
});inferCall covers one more case the rules glossed over. When the function being called is still an unknown, such as a parameter f, calling it is itself a fact: f must be a function from these argument types to some result.
Here's what it infers, without running anything:
(lambda (x) (+ x 1)) : (Num) -> Num
(lambda (x) x) : ('a) -> 'a
(lambda (f x) (f (f x))) : (('a) -> 'a, 'a) -> 'a
(lambda (f g x) (f (g x))) : (('a) -> 'b, ('c) -> 'a, 'c) -> 'b
+ : (Num...) -> Num
(print (quote hi)) : Data
((lambda (f) (f 1 2)) +) : NumThe third line is worth reading slowly. Nobody wrote a type. The checker saw f applied to x, then applied again to the result. It concluded that f must return the same type it takes, and that x must have that type.
Errors before running
Checking fails with typed errors, like evaluation does, and they carry spans:
// Type errors: found before running, pointing at the source.
export class Mismatch extends Schema.TaggedError<Mismatch>()(
"Mismatch",
{ expected: Schema.String, got: Schema.String, span: Span },
) {
override get message() {
return `expected ${this.expected}, got ${this.got}`;
}
}
export class ArityError extends Schema.TaggedError<ArityError>()(
"ArityError",
{ expected: Schema.Number, got: Schema.Number, span: Span },
) {
override get message() {
const { expected, got } = this;
const s = expected === 1 ? "" : "s";
return `expected ${expected} argument${s}, got ${got}`;
}
}
export class CyclicType extends Schema.TaggedError<CyclicType>()(
"CyclicType",
{ variable: Schema.String, type: Schema.String, span: Span },
) {
override get message() {
return `infinite type: ${this.variable} = ${this.type}`;
}
}
export type CheckError =
| UnboundName
| Mismatch
| ArityError
| CyclicType;The pipeline gains one step between parsing and evaluation:
export type Failure = Diagnostic | CheckError | EvalError;
// Parse, then check, then run. A program that fails to check never
// starts, so it can't print anything.
export const run = (
source: string,
): Effect.Effect<Value, Failure, Output> =>
parse(source).pipe(
Effect.tap(check),
Effect.flatMap((expr) => evaluate(expr, globals)),
);
// The type of a program, without running it.
export const typeOf = (source: string) =>
parse(source).pipe(Effect.flatMap(check), Effect.map(showType));
export const report = (source: string, error: Failure) =>
render(source, { message: error.message, span: error.span });Now Part 4's program fails before it runs, and the error points at the argument:
error: expected Num, got Data
1 | ((lambda (x) (+ x 1)) (quote a))
| ^^^^^^^^^The checker inferred (Num) -> Num for the function from its body, then compared that with the argument at the call. The blame moved from where the bad value was used to where it was introduced.
The series' opening example is caught the same way:
error: expected Num, got Data
1 | (+ 1 (quote hello))
| ^^^^^^^^^^^^^And because checking happens first, a program that fails to check has no effects at all. (+ (print 1) (quote x)) used to print 1 and then fail. Now it fails before printing anything.
Calling a number, passing the wrong number of arguments, and using an unbound name are all caught the same way, before running:
error: expected a function, got Num
1 | (5 1)
| ^
error: expected 1 argument, got 2
1 | (print 1 2)
| ^^^^^^^^^^^To try it, put Parts 2, 3, and 4 in directories named 02, 03, and 04, this post's files in 05, install effect version 4, and run this with Node 24 from inside 05:
import { Effect } from "effect";
import { typeOf } from "./run.ts";
console.log(Effect.runSync(typeOf("(lambda (x) (+ x 1))")));
// (Num) -> NumTypes that would have to contain themselves
One program has no sensible type at all:
error: infinite type: 'a = ('a) -> 'b
1 | (lambda (x) (x x))
| ^x is applied to itself, so its type 'a would have to be a function taking 'a, which would have to be a function taking a function taking 'a, and so on forever. The occurs check in bind catches that before it can loop.
What the checker gives up
A type checker that rejects every program that would fail must also reject some programs that wouldn't. This one runs fine under Part 4's evaluator and returns 1:
((lambda (id) ((id id) 1)) (lambda (x) x))The checker rejects it with the same infinite-type error. Inside the lambda, id is a parameter, and parameters get one type each. Applying id to itself needs two different types at once. The same limit rejects (lambda (f) (+ (f 1) (f (quote a)))): f can't take both a Num and a Data.
print doesn't have this problem because it's a global whose type is written down as polymorphic. Parameters only get the single type the checker infers. The classic fix is to generalize names bound by let, which returns as a prelude form in Part 8.
The checker also doesn't make every runtime error impossible. (/ 1 0) has type Num, and it still fails at runtime with division by zero. Types describe what kind of value an expression produces, not which value.
Two passes over one tree
Look at the pipeline again: parse, then Effect.tap(check), then evaluate. The checker computes a type for every expression, and tap throws them all away. Then the evaluator walks the same tree again, resolving every name again, and still checks for unbound names, calls to non-functions, wrong argument counts, and non-numbers passed to +.
For a checked program, those four runtime checks should never fire. That's the claim a soundness argument is supposed to establish, and so far we've only tested it, not argued it. Still, the evaluator doesn't know any of this. It's still interpreting the surface syntax, the language as written, and it re-derives everything the checker already proved.
The fix is to make checking produce something: a smaller, typed core language that the evaluator can trust. That's the step that turns the interpreter into a compiler.
Next: Part 6, The Interpreter Becomes a Compiler. Syntax is what you write. Core is what it means.
The code in this post lives in docs/snippets/blog/in-the-beginning/05 and runs in the site's test suite.