Appendix D: Glossary

Terms that get heavy use in this book, defined for quick reference.

Affine type. A type whose values can be used at most once. Stronger than ordinary types (which allow unbounded use), weaker than linear types (which require exactly once). Rust’s borrow checker is built on affine types. CML uses affine-in-practice / linear-in-theory.

Algebraic data type (ADT). A type built from products (records, tuples) and sums (tagged unions). The “algebra” refers to the fact that the type operators obey arithmetic identities (distribution, currying, etc.) that follow from cardinality.

Arena. A region of memory with a single, simple allocation strategy (typically bump allocation) and a single free operation that releases the whole arena. Used in the kernel for per-process or per-request memory management. See Region.

Boundary tagged. A representation strategy where values carry type information only at structural boundaries (function calls, message-passing), not while resident in registers. An alternative to verified tagged not chosen for this ISA.

Bottom handler. The outermost handler in a tower, responsible for terminating an effect’s bubble-up search. The kernel’s bottom handlers define what happens to effects that no inner handler caught.

Bump allocation. An allocation strategy where memory is allocated by incrementing a pointer through a contiguous region. Deallocation is bulk-only (release the whole region). Used by the kernel’s local arena handler.

CAM (content-addressable memory). A hardware data structure that returns matches for a given key in parallel. The handler CAM in this ISA holds the most-recently-installed handlers, allowing single-cycle handler lookup for the common case.

Capability. A first-class value representing permission to do something — read from a device, allocate from a region, invoke a continuation. Capabilities are typically linear, so they cannot be forged or copied.

Cardinality. The count of distinct values of a type. bool has cardinality 2; int32 has cardinality 2^32; a product type’s cardinality is the product of its components’. The unifying principle behind ML’s type algebra.

CML. “Concrete ML” — the language designed in this book. A small ML with effect handlers, linear types, and a tight relationship with the ISA it compiles to.

Concretization. Gilbert Simondon’s notion of how a technical object becomes more “itself” over time, as its parts come to fit each other rather than fitting an idealized abstract function. The animating philosophy behind this book’s co-design approach.

Continuation. The rest of the computation, reified as a value. A continuation k represents “what would happen next if the value v were supplied”; invoke k v runs that next thing with that value.

Continuation passing style (CPS). A program transformation where every function takes its continuation as an explicit argument. The continuation is the function that consumes the function’s result. CML programs are transformed to a CPS-adjacent form during compilation, though most of the CPS structure is reified into the runtime continuation values rather than being explicit in the IR.

Effect (formal). A typed operation that user code can perform, dispatched to some surrounding handler. Distinct from “side effect” in the casual sense; an effect in this book’s vocabulary is a specific, declared operation.

Effect handler. Code that catches one or more effects, runs in response to a perform, and decides whether to resume the continuation. The kernel’s scheduler is an effect handler. The TCP stack is a stack of effect handlers.

Effect row. A type-level set of effects that a function may perform. Written as () / {IO, Mem} in CML: “returns unit, performs effects from IO and Mem.” Tracked by the type system to ensure handlers are installed where needed.

Effect table. A hardware-managed table (256 entries in this ISA) mapping effect IDs to default handlers or device destinations. The fallback when the handler CAM misses.

Family-and-op. The 8-bit effect ID in this ISA, structured as 4 bits of family plus 4 bits of op. Allows 16 families × 16 ops = 256 distinct effect IDs.

Frame. A unit of execution state — locals, a return address, a partial computation. Multiple frames form a frame tree. The kernel’s hybrid frame allocation puts most frames on a contiguous stack and PERF-captured frames on the heap.

Free theorem. A property of a polymorphic function deducible from its type alone, without reading its implementation. From parametricity. The classical example: a function of type 'a list -> 'a list cannot invent new elements; it can only rearrange or drop existing ones.

Handler CAM. The 8-entry content-addressable memory in this ISA that caches the most-recently-installed effect handlers. Single-cycle dispatch on hit; spill cost ~12× on miss.

Hindley-Milner. The classical type inference algorithm for ML languages. Infers principal types automatically, without annotations. CML uses a Hindley-Milner extension that includes effect rows.

Install-ID. A counter used by the ISA to disambiguate multiple installations of handlers for the same effect. When handlers nest, the most recently installed must take precedence; the install-ID is how the hardware identifies “most recent.”

Linear type. A type whose values must be used exactly once. Stronger than affine (which allows zero-or-one uses). Continuations in CML are linear: they cannot be invoked twice nor forgotten.

Match expression. Pattern-matching dispatch: match v with | pat1 -> e1 | pat2 -> e2 | .... ML’s primary control-flow primitive. Exhaustive by default — the compiler warns or errors if a case is missing.

Monomorphization. A compilation strategy where each polymorphic function is specialized for every type it is called with. Trades binary size for runtime efficiency. The alternative is uniform representation.

NoC (Network-on-Chip). The on-chip mesh fabric that carries packets between tiles (cores and devices). In this book’s design, the primary communication mechanism — most cross-tile operations are NoC packets, surfaced as effects.

Ontological minimality. A design principle, drawn from Stillwork’s philosophical doctrine: prefer the fewest, truest abstractions a domain genuinely requires. Related to Simondonian concretization.

Parametric polymorphism. A form of polymorphism where a function works for any type, with no information about the type available at runtime. ML’s 'a -> 'a is parametric. Distinct from ad-hoc polymorphism (which dispatches on type) and subtype polymorphism (which dispatches through inheritance).

Pattern matching. See Match expression.

PERF. The ISA instruction that performs an effect. Captures the continuation, searches the handler CAM and effect table, transfers control to a handler or sends a NoC packet.

Polymorphism. “Many shapes.” A function or type is polymorphic if it can be used with different concrete types. ML’s parametric polymorphism is the simplest form: a type variable 'a stands for any type.

Precise preemption. The property that a preempt can occur at any instruction boundary, with the preempted state being a clean state from which execution can resume coherently. This ISA commits to precise preemption.

Process. A unit of execution in the kernel — a continuation, an id, optionally a home core. Distinct from an OS process in conventional systems because there is no separate address space or kernel context.

Reify. Convert something abstract (a function-to-be-run, an effect to be performed later) into a first-class value (a continuation, a token). reify (fun () -> body ()) creates a continuation that, when invoked, runs body.

Region. A memory area with bulk allocation and bulk free. Region handlers manage allocation within their scope; on handler exit, the region is freed. Linear region capabilities make this safe.

Resume. The operation that delivers a value back to a perform site, continuing the computation that was suspended. resume k v invokes the continuation k with value v.

Row polymorphism. A type-system feature allowing functions to abstract over the extension of a row (record or effect set). A function with type 'a / {IO | r} -> 'a / {IO | r} works for any effect row that includes IO, leaving the other effects (r) abstract.

Soundness theorem. A statement that the type system rules out a class of errors. CML’s intended soundness theorem: well-typed programs do not fault on hardware tag checks. (Not yet formally proved; the design is structured to make such a proof tractable.)

Spill. When the handler CAM is full and a new handler must be installed, the least-recently-used CAM entry is spilled to memory. Subsequent dispatch to that effect costs the full memory-walk price (about 12× a CAM hit).

Sum type. A tagged union — a value is one of several alternatives, with a runtime tag indicating which. Pattern matching dispatches on the tag.

Tag (hardware). The 3-bit field carried with each value in this ISA, indicating its primitive type. INT, PTR, CONT, CLOSURE, UNIT, BOOL, and two reserved.

Tower (handler tower). The hierarchical stack of effect handlers in scope at any point. When a perform happens, the search starts at the top of the tower and walks down until it finds a matching handler.

Uniform representation. A compilation strategy where every value is represented as a single machine word, possibly a pointer to a heap-allocated object. Trades runtime efficiency for compactness and simpler compilation. The alternative is monomorphization. CML defaults to uniform representation, with monomorphization as an optimization.

Unit type. A type with exactly one value, (). Cardinality 1. The multiplicative identity in the type algebra. What void should have meant.

Unsafe. A scope marker indicating that the enclosed code may use ISA primitives without the language’s normal guarantees. Tracked as an effect (Unsafe) in the type system, so callers know they’re calling unsafe code. Required for inline assembly, bare pointer operations, etc.

Verified-tagged. The hardware representation strategy chosen for this ISA: values carry tags at runtime, and the ALU checks tags before operating. The tag check is verification (the compiler proves it should pass), not dispatch (no opcode varies based on tag). See chapter 6.

With (with handler in expr). The CML syntax for installing a handler over an expression. The handler is active for the duration of expr, catching any effects expr performs.