The Prelude Is the Language
Part 08 of From Lists to Languages · Act II, Types and Extension ·
A small kernel, many languages.
Part 7 ended with a macro that the checker couldn't speak for. The user wrote (twice (lambda (a b) a) 1), and the error pointed inside twice's template, at a call the user never wrote. A macro is a rewrite that runs before checking, so the checker only ever sees what the macro produced.
This post adds the other kind of extension: a form, which runs during checking. A form gets its piece of syntax and the checker's tools, and it decides what its parts must be, which names it binds, what type the whole thing has, and what core it becomes. Forms live in a prelude, and the compiler shrinks to a kernel that knows almost nothing on its own. By the end, lambda is a form, let does something no macro can, and a second language runs on the same kernel.
The kernel
Part 6's elaborator had a case for each of Part 4's node types: Num, Ref, Quote, Lambda, and Call. Part 4's parser had already decided which lists were which. The kernel works on the s-expression itself and knows three things: numbers, names, and calls.
// Numbers, names, and calls. Everything else is a form.
const go = (x: Sexp, frame: Frame): Elab =>
Effect.gen(function* () {
const { span } = x;
if (x._tag === "Num") {
return { _tag: "Lit", value: x.value, type: num, span };
}
if (x._tag === "Sym") {
return yield* ref(x.name, span, frame);
}
const [head, ...rest] = x.items;
if (!head) {
return yield* fail("() is not an expression", span);
}
// A form's name means the form, unless a local shadows it.
if (head._tag === "Sym" && !bound(head.name, frame)) {
const form = prelude.forms.get(head.name);
if (form) return yield* form(x, kernel(frame));
}
const fn = yield* go(head, frame);
const args: Core[] = [];
for (const arg of rest) args.push(yield* go(arg, frame));
return yield* apply(fn, args, span);
});
const kernel = (frame: Frame): Kernel => ({
elaborate: (x) => go(x, frame),
check: (x, type) =>
Effect.tap(go(x, frame), (c) =>
unify(type, c.type, x.span),
),
within: (names, schemes, inside) =>
inside(kernel({ names, schemes, parent: frame })),
prelude: (name, span) => {
let depth = 0;
for (let f = frame.parent; f; f = f.parent) depth++;
return ref(name, span, root, depth);
},
apply,
fresh,
generalize: (type) => generalize(type, frame),
});A list whose head names a form is handed to the form. Everything else is a number, a name, or a call, which are elaborated as in Part 6.
The check for locals matters. Part 7's expander didn't know about scopes, so a parameter named square still expanded as the macro. The kernel does know, because it's the thing that builds frames. A local that shadows a form's name wins:
((lambda (if) (if 7)) (lambda (n) (* n 2))) ; => 14kernel(frame) is everything a form can ask for:
// A form gets the whole list it heads, and a kernel for the frame
// it appears in. It returns core, or a diagnostic about its syntax.
export type Form = (form: List, k: Kernel) => Elab;
export interface Kernel {
// Elaborate a part of the form, or check it has a type.
readonly elaborate: (x: Sexp) => Elab;
readonly check: (x: Sexp, type: Type) => Elab;
// Run `inside` in a new frame that binds `names`.
readonly within: <A, E>(
names: ReadonlyArray<string>,
schemes: ReadonlyArray<Scheme>,
inside: (k: Kernel) => Effect.Effect<A, E>,
) => Effect.Effect<A, E>;
// A name from the prelude, even where a local shadows it.
readonly prelude: (name: string, span: Span) => Elab;
// The kernel's rule for calls, and two tools for typing rules.
readonly apply: (fn: Core, args: Core[], span: Span) => Elab;
readonly fresh: () => Type;
readonly generalize: (type: Type) => Scheme;
}The kernel elaborates and checks a form's parts, opens frames for the names a form binds, and applies the call rule. fresh and generalize are for writing typing rules. A form never sees the solver itself, and it can't make a frame that the kernel doesn't know about.
A language is then a value, a prelude:
// A language is a prelude: its forms, and the values its programs
// start with, each with a type scheme.
export interface Prelude {
readonly forms: ReadonlyMap<string, Form>;
readonly values: ReadonlyMap<string, PreludeValue>;
}
export interface PreludeValue {
readonly scheme: Scheme;
readonly value: Value;
}
// The prelude's values are the outermost frame of every program.
export const rootEnv = (prelude: Prelude): Env => ({
slots: [...prelude.values.values()].map((v) => v.value),
parent: undefined,
});Built-in functions now live in the program's outermost frame, so a reference to + is a Local like any other. Core still has Part 6's six node types, and Part 6's executor runs the result unchanged:
// Part 7's pipeline, minus Part 4's parser: the kernel elaborates
// the expanded s-expression directly, with a prelude's forms.
export const compile = (prelude: Prelude, source: string) =>
expanded(source).pipe(
Effect.flatMap((sexp) => elaborate(prelude, sexp)),
);
// Part 6's executor runs the result, in the prelude's frame.
export const run = (
prelude: Prelude,
source: string,
): Effect.Effect<Value, Failure, Output> =>
compile(prelude, source).pipe(
Effect.flatMap((core) => execute(core, rootEnv(prelude))),
);lambda and quote are forms
quote and lambda used to be cases in Part 4's parser. Now they're entries in a prelude:
// Part 4's parser handled quote and lambda. Now they're forms.
const quote: Form = ({ items, span }) => {
const [, datum, ...extra] = items;
if (!datum || extra.length > 0) {
return fail("quote takes exactly one argument", span);
}
return Effect.succeed({ _tag: "Datum", datum, type: data, span });
};const lambda: Form = ({ items, span }, k) =>
Effect.gen(function* () {
const [, list, body, ...extra] = items;
if (list?._tag !== "List" || !body || extra.length > 0) {
const message = "lambda takes a parameter list and one body";
return yield* fail(message, span);
}
const params: string[] = [];
for (const param of list.items) {
if (param._tag !== "Sym") {
const message = "a parameter must be a symbol";
return yield* fail(message, param.span);
}
if (params.includes(param.name)) {
const message = `${param.name} is already a parameter`;
return yield* fail(message, param.span);
}
params.push(param.name);
}
// Parameters get one type each: a scheme with no variables.
const types = params.map(() => k.fresh());
const schemes = types.map((type) => ({ vars: [], type }));
const inner = yield* k.within(params, schemes, (k) =>
k.elaborate(body),
);
const type = fun(types, inner.type);
return { _tag: "Lambda", params, body: inner, type, span };
});The syntax rules and messages are Part 4's. The typing rule is Part 5's: a fresh unknown for each parameter, and a function type from those to the body's type. Notice the inner (k) =>: inside within, the form gets a kernel for the new frame, and the body is elaborated there.
let, and a promise from Part 5
Part 5 rejected this program, even though it runs fine:
((lambda (id) ((id id) 1)) (lambda (x) x))id is a parameter, and a parameter gets one type. Applying id to itself needs two. Part 5 said the fix was to generalize names bound by let, and that let would come back as a prelude form.
A macro can't do it. Here's let as a Part 7 macro:
(defmacro my-let
((((name value)) body) `((lambda (,name) ,body) ,value)))
(my-let ((id (lambda (x) x))) ((id id) 1))It expands into exactly the program above, and fails the same way:
error: infinite type: 'a = ('a) -> 'b
4 | (my-let ((id (lambda (x) x))) ((id id) 1))
| ^^The rewrite is right, but the typing rule is the one for lambda. A form gets to bring its own rule. Here's what the rule needs. A type scheme is a type plus the variables that each use may choose for itself:
// A type scheme is a type plus the variables in it that each use
// may choose afresh. The identity function's scheme has vars [0]
// and type ('a) -> 'a, where 'a is variable 0.
export const Scheme = Schema.Struct({
vars: Schema.Array(Schema.Number),
type: Type,
});
export type Scheme = typeof Scheme.Type;Generalizing turns a type into a scheme, and using a name turns its scheme back into a type with fresh variables:
// The unknowns in a type, except the scheme's own variables.
// Own variables are skipped before anything is resolved: a
// prelude's variable 0 is not this run's variable 0.
const unknowns = (t: Type, own: ReadonlyArray<number>) => {
const found = new Set<number>();
const walk = (t: Type, own: ReadonlyArray<number>): void => {
if (t._tag === "TFun") {
const inner = [...t.params, t.result];
if (t.rest) inner.push(t.rest);
return inner.forEach((i) => walk(i, own));
}
if (t._tag !== "TVar" || own.includes(t.id)) return;
const r = resolve(t);
// A solved variable's answer uses only this run's numbers.
if (r._tag === "TVar") found.add(r.id);
else walk(r, []);
};
walk(t, own);
return found;
};
// Every unknown in `type` that no enclosing name mentions can
// be chosen afresh at each use.
const generalize = (type: Type, frame: Frame): Scheme => {
const outside = new Set<number>();
for (let f: Frame | undefined = frame; f; f = f.parent) {
for (const { vars, type } of f.schemes) {
unknowns(type, vars).forEach((v) => outside.add(v));
}
}
const free = [...unknowns(type, [])];
const vars = free.filter((v) => !outside.has(v));
return { vars, type: resolve(type) };
};
// A use gets fresh copies of the scheme's variables.
const instantiate = ({ vars, type }: Scheme): Type => {
const copies = new Map(vars.map((v) => [v, fresh()]));
const copy = (t: Type): Type =>
t._tag === "TVar" ? (copies.get(t.id) ?? t)
: t._tag !== "TFun" ? t
: fun(
t.params.map(copy),
copy(t.result),
t.rest && copy(t.rest),
);
// Copy first: a prelude's own variable numbers mean nothing
// to this run's solver.
return resolve(copy(type));
};The key line is vars = free.filter(...). An unknown that a name in an enclosing frame also mentions isn't the value's to give away; something outside may still decide it. Here z's type is y's type, so it stays one type, and + settles it:
(lambda (y) (let ((z y)) (+ z 1))) ; : (Num) -> NumWith those two tools, let is a form like any other:
// (let ((name value) ...) body). Each value is elaborated, then its
// type is generalized before the next binding or the body sees it.
const let_: Form = ({ items, span }, k) => {
const [, bindings, body, ...extra] = items;
if (bindings?._tag !== "List" || !body || extra.length > 0) {
return fail("let takes a binding list and one body", span);
}
return bind(bindings.items, body, span, k);
};
const bind = (
bindings: ReadonlyArray<Sexp>,
body: Sexp,
span: Span,
k: Kernel,
): Elab =>
Effect.gen(function* () {
const [first, ...more] = bindings;
if (!first) return yield* k.elaborate(body);
const [name, value, ...extra] =
first._tag === "List" ? first.items : [];
if (name?._tag !== "Sym" || !value || extra.length > 0) {
return yield* fail("a binding is (name value)", first.span);
}
const bound = yield* k.elaborate(value);
const scheme = k.generalize(bound.type);
const params = [name.name];
const rest = yield* k.within(params, [scheme], (k) =>
bind(more, body, span, k),
);
// The same core as ((lambda (name) rest) value).
const fn: Core = {
_tag: "Lambda",
params,
body: rest,
type: fun([bound.type], rest.type),
span,
};
const { type } = rest;
return { _tag: "Call", fn, args: [bound], type, span };
});Each binding is elaborated, generalized, and then bound for the rest. The core is the same ((lambda (id) ...) ...) that the macro produced; only the typing differs.
(let ((id (lambda (x) x)))
((id id) 1))
; => 1id has the scheme ('a) -> 'a, and each mention gets its own 'a. lambda parameters still get one type each. That's the classic Hindley–Milner arrangement: a let knows the value it's generalizing, and a parameter doesn't know which argument it will get.
twice, at the call
With a generalizing let, twice doesn't need to be a macro. It's a function, and its type is inferred:
(let ((twice (lambda (f x) (f (f x)))))
twice)
; : (('a) -> 'a, 'a) -> 'aThat type is the rule Part 7 wanted: twice takes a one-argument function and a value. Nobody wrote it down, and the checker enforces it at the user's call:
error: expected ('a) -> 'a, got ('b, 'c) -> 'b
2 | (twice (lambda (a b) a) 1))
| ^^^^^^^^^^^^^^^^Most of Part 7's macros were functions waiting for this. A macro is still the right tool for new syntax, which a function can't provide. let itself is an example: its bindings aren't expressions.
if, without a new core node
Core has no conditional. It doesn't need one, because it already has a way to delay work: a function with no parameters runs nothing until it's called. A conditional can pick one of two such functions and call it:
((choose test (lambda () yes) (lambda () no)))choose is an ordinary function in the prelude with the type (Num, 'a, 'a) -> 'a. A form calls prelude functions through k.prelude:
// Call a prelude function from inside a form.
export const call = (
k: Kernel,
name: string,
args: Core[],
span: Span,
): Elab =>
Effect.flatMap(k.prelude(name, span), (fn) =>
k.apply(fn, args, span),
);// Core has no conditional, and doesn't need one. choose picks one
// of two functions with no parameters, and calling it runs only
// that branch: ((choose test (lambda () yes) (lambda () no))).
type Inside = (k: Kernel) => Elab;
export const branch = (
k: Kernel,
test: Core,
yes: Inside,
no: Inside,
span: Span,
): Elab =>
Effect.gen(function* () {
const thunk = (inside: Inside) =>
Effect.map(k.within([], [], inside), (body): Core => {
const type = fun([], body.type);
return { _tag: "Lambda", params: [], body, type, span };
});
const args = [test, yield* thunk(yes), yield* thunk(no)];
const picked = yield* call(k, "choose", args, span);
return yield* k.apply(picked, [], span);
});if adds the typing rule: the test is a number, and both branches have one type.
// (if test yes no): the test is a number, 0 meaning false, and the
// branches have one type between them.
const if_: Form = ({ items, span }, k) =>
Effect.gen(function* () {
const [, test, yes, no, ...extra] = items;
if (!test || !yes || !no || extra.length > 0) {
return yield* fail("if takes a test and two branches", span);
}
const checked = yield* k.check(test, num);
const type = k.fresh();
return yield* branch(
k,
checked,
(k) => k.check(yes, type),
(k) => k.check(no, type),
span,
);
});(if 1 2 3) elaborates to plain core, the same six node types:
call : Num
call : () -> Num
local choose @0.8 : (Num, () -> Num, () -> Num) -> () -> Num
lit 1 : Num
lambda () : () -> Num
lit 2 : Num
lambda () : () -> Num
lit 3 : NumOnly the chosen branch runs, so (if 0 (print 1) (print 2)) prints 2 and nothing else. The diagnostics are about if, at the user's source, not about choose or thunks:
error: expected Num, got Data
1 | (if 1 2 'a)
| ^^error: expected Num, got Data
1 | (if 'a 1 2)
| ^^k.prelude also closes the other gap Part 7 left open. Part 7's macros looked up a template's free names, like * in scale, wherever the macro was used. A form looks up choose in the prelude, wherever it's used, so a user's own choose can't change what if means:
((lambda (choose) (if 1 2 3)) 5) ; => 2match
match compares a number with literal cases, in order:
(let ((size (lambda (n)
(match n (0 'none) (1 'one) (_ 'many)))))
(size 1))
; => one// (match n (0 a) (1 b) (_ c)): compare a number with literal cases,
// in order. The last case must be _, so every number has an answer.
interface Case {
readonly pattern: Sexp;
readonly result: Sexp;
}
const match: Form = ({ items, span }, k) =>
Effect.gen(function* () {
const [, subject, ...rest] = items;
if (!subject) return yield* fail("match needs a subject", span);
const cases: Case[] = [];
for (const c of rest) {
const [pattern, result, ...extra] =
c._tag === "List" ? c.items : [];
const wild = pattern?._tag === "Sym" && pattern.name === "_";
const literal = pattern?._tag === "Num";
if (!result || extra.length > 0 || !(wild || literal)) {
const message = "a case is (number result) or (_ result)";
return yield* fail(message, c.span);
}
if (cases.at(-1)?.pattern._tag === "Sym") {
return yield* fail("nothing can follow the _ case", c.span);
}
cases.push({ pattern, result });
}
if (cases.at(-1)?.pattern._tag !== "Sym") {
const message = "match needs a last (_ result) case";
return yield* fail(message, span);
}
// Bind the subject once, to a name no program can write.
const value = yield* k.check(subject, num);
const type = k.fresh();
const name: Sexp = { _tag: "Sym", name: "#match", span };
const scheme = { vars: [], type: num };
const body = yield* k.within(["#match"], [scheme], (k) =>
compare(cases, name, type, k),
);
const fn: Core = {
_tag: "Lambda",
params: ["#match"],
body,
type: fun([num], body.type),
span,
};
return yield* k.apply(fn, [value], span);
});
// One case at a time: a branch on (= subject pattern), with the
// remaining cases in the "no" branch.
const compare = (
cases: ReadonlyArray<Case>,
name: Sexp,
type: Type,
k: Kernel,
): Elab =>
Effect.gen(function* () {
const { pattern, result } = cases[0]!;
if (pattern._tag === "Sym") return yield* k.check(result, type);
const { span } = pattern;
const subject = yield* k.elaborate(name);
const literal = yield* k.elaborate(pattern);
const test = yield* call(k, "=", [subject, literal], span);
return yield* branch(
k,
test,
(k) => k.check(result, type),
(k) => compare(cases.slice(1), name, type, k),
span,
);
});Its rules are its own. Every case is a number or _ with one result, and the last case must be _, so every number has an answer:
error: match needs a last (_ result) case
1 | (match 2 (0 'none) (1 'one))
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^Every result is checked against one shared type, case by case, so a mismatch is reported at the case that's different:
error: expected Data, got Num
1 | (match 2 (0 'none) (1 2) (_ 'many))
| ^match binds its subject once, to #match. The reader rejects #, so no program can write that name, and no user name can capture it.
The prelude doesn't have when yet. (when test body) does nothing when the test fails, and in a language where every expression has a value and a type, "nothing" needs a type of its own. That's part of what effects bring, in the next post.
The prelude's values
The rest of the standard prelude is its values:
// The values every program starts with. Part 6's built-ins keep
// their implementations; the prelude adds -, =, <, and choose.
const a: Type = { _tag: "TVar", id: 0 };
const mono = (type: Type) => ({ vars: [], type });
const poly = (type: Type) => ({ vars: [0], type });
const value = (name: string, scheme: Scheme, value: Value) =>
[name, { scheme, value }] as const;
const builtin = (name: string, scheme: Scheme) =>
value(name, scheme, globals.get(name)!);
// A new primitive on two numbers. The checker already proved that
// both arguments are numbers.
type Binary = (x: number, y: number) => number;
const binary = (name: string, f: Binary) =>
value(name, mono(fun([num, num], num)), {
_tag: "Primitive",
name,
apply: ([x, y]) =>
Effect.succeed(f(Number(x?.value), Number(y?.value))),
});
export const arithmetic = new Map([
builtin("+", mono(fun([], num, num))),
builtin("*", mono(fun([], num, num))),
builtin("/", mono(fun([], num, num))),
binary("-", (x, y) => x - y),
]);
export const standard: Prelude = {
forms: new Map([
["quote", quote],
["lambda", lambda],
["let", let_],
["if", if_],
["match", match],
]),
values: new Map([
...arithmetic,
builtin("pi", mono(num)),
builtin("print", poly(fun([a], a))),
binary("=", (x, y) => (x === y ? 1 : 0)),
binary("<", (x, y) => (x < y ? 1 : 0)),
// choose: (Num, 'a, 'a) -> 'a returns one of its arguments.
value("choose", poly(fun([num, a, a], a)), {
_tag: "Primitive",
name: "choose",
apply: ([test, yes, no]) =>
Effect.succeed((test?.value === 0 ? no : yes)!.value),
}),
]),
};Conditions are numbers, with 0 meaning false, because Part 5's types are Num, Data, and functions. A Bool would be one more tagged struct in that schema.
Another language on the same kernel
The kernel doesn't know lambda, so a prelude without it describes a language without functions. Here is a language for prices. Its forms check what a price means, not only its shape. A percentage has to be between 0 and 100, and that's a Schema:
// A percentage is a number between 0 and 100. A literal one is
// checked when the program compiles.
const Percent = Schema.Number.check(
Schema.isBetween(
{ minimum: 0, maximum: 100 },
{ message: "a percentage is between 0 and 100" },
),
);
const percentage = (x: Sexp, k: Kernel): Elab =>
Effect.gen(function* () {
if (x._tag === "Num") {
const decoded = Schema.decodeUnknownEffect(Percent)(x.value);
yield* Effect.mapError(decoded, (e) => ({
message: e.message,
span: x.span,
}));
}
return yield* k.check(x, num);
});// (price base (discount n) (tax n) ...): adjust a base amount by
// percentages, in order.
const adjustments = new Map([
["discount", "-"],
["tax", "+"],
]);
const price: Form = ({ items, span }, k) =>
Effect.gen(function* () {
const [, base, ...steps] = items;
if (!base) {
return yield* fail("price needs a base amount", span);
}
let total = yield* k.check(base, num);
for (const step of steps) {
const [head, amount, ...extra] =
step._tag === "List" ? step.items : [];
const op = head?._tag === "Sym" && adjustments.get(head.name);
if (!op || !amount || extra.length > 0) {
const message = "expected (discount n) or (tax n)";
return yield* fail(message, step.span);
}
// total * (100 - n) / 100 for a discount, + for a tax.
const { span } = step;
const n = yield* percentage(amount, k);
const hundred: Core = {
_tag: "Lit",
value: 100,
type: num,
span,
};
const factor = yield* call(k, op, [hundred, n], span);
const scaled = yield* call(k, "*", [total, factor], span);
total = yield* call(k, "/", [scaled, hundred], span);
}
return total;
});
// discount and tax mean something only inside a price.
const inside =
(name: string): Form =>
({ span }) =>
fail(`${name} only makes sense inside price`, span);// A language for prices: three forms and four functions, on the
// same kernel. No lambda, no let, no if.
export const pricing: Prelude = {
forms: new Map([
["price", price],
["discount", inside("discount")],
["tax", inside("tax")],
]),
values: arithmetic,
};
// Or both languages at once.
export const combined: Prelude = {
forms: new Map([...standard.forms, ...pricing.forms]),
values: new Map([...standard.values, ...pricing.values]),
};(price 200
(discount 25)
(tax 10))
; => 165Its errors are in its own terms, at the author's source:
error: a percentage is between 0 and 100
1 | (price 200 (discount 120))
| ^^^error: expected (discount n) or (tax n)
1 | (price 200 (coupon 5))
| ^^^^^^^^^^error: tax only makes sense inside price
1 | (tax 8)
| ^^^^^^^Everything it doesn't define is out of the language. (lambda (x) x) fails with lambda is not defined. So does quoting: (price 'a (tax 1)) fails with quote is not defined, pointing at the '.
Preludes are maps, so languages combine. With both, a function can compute prices:
(let ((sale (lambda (amount) (price amount (discount 25)))))
(sale 80))
; => 60A literal percentage is checked when the program compiles; a computed one, like (tax rate), is only checked to be a number. The kernel, the core, the executor, and Part 6's compiled artifacts are the same for all three languages. Only the prelude changed.
What forms bought
Go back to the Lisp Curse. Part 7's macros made new words cheap, and nothing about a word told the checker how to use it. A form is still cheap, but it comes with a rule. The kernel enforces it, the errors use the form's terms, and they point at the user's source. A tool can list the words a language has by reading its prelude.
There's a limit to that last sentence. A tool can list a prelude's forms, but each form's rule is a TypeScript function, so the only way to find out what price accepts is to run it. In Forma, a form declares its syntax and the types of its parts as data, and the rule is built from that declaration; see Writing a form. This series keeps forms as functions, but Part 10 comes back to programs that tools can read.
To try it, put Parts 2 through 7 in directories named 02 to 07, this post's files in 08, install effect version 4, and run this with Node 24 from inside 08:
import { Effect } from "effect";
import { pricing } from "./pricing.ts";
import { standard } from "./prelude.ts";
import { typeOf } from "./run.ts";
const id = "(let ((id (lambda (x) x))) id)";
console.log(Effect.runSync(typeOf(standard, id))); // ('a) -> 'a
const price = "(price 200 (discount 25) (tax 10))";
console.log(Effect.runSync(typeOf(pricing, price))); // NumWhat's next
That's the end of Act II. The language has syntax with a schema, types checked before it runs, a compiler to a small typed core, macros for new syntax, and forms for new rules.
One thing in it still isn't honest. print has the type ('a) -> 'a, the same as id. Nothing in the type says that it prints, or that it needs an Output service to run. The checker knows what every expression returns, and nothing about what it does.
Next: Part 9, Effects Are Part of the Type. The type describes not only the result, but what a computation demands.
The code in this post lives in docs/snippets/blog/in-the-beginning/08 and runs in the site's test suite.