Appendix A Glossary

A reference for the vocabulary used throughout the book. The first section covers Silo's language-level terminology and its system architecture. The second section covers the academic and research background behind Silo's design choices — useful if you want to follow footnotes into the literature.

Silo Concepts

Affine type

A value that can be used at most once. After you consume it, it's gone. If you don't use it, the compiler drops it for you. Most values in Silo are affine. Contrast with linear (must be used exactly once) and unrestricted (use as many times as you want).

Algebraic effect

A typed side effect that composes cleanly. "Algebraic" just means the effects combine according to simple laws (like addition) — +Console +FileSystem is the union, no special interaction. In practice: a function call where the implementation lives outside your program. The VM requests it, the host handles it. See Effects, Totality, and Divergence.

Arity variant

A /N-suffixed variant of a built-in stack shuffler that operates on groups of N values rather than single values. dup/2 duplicates the top pair; swap/2 swaps the top two pairs; and so on. The bare dup/drop/swap/etc. are the arity-1 forms. See Stack and Words.

Aspect

A cross-cutting concern with dynamic scoping. An aspect defines operations with default behaviour that can be overridden via :with. Think logging, tracing, metrics — behaviour you want to inject throughout a program without threading it through every function signature. See Aspects.

Capability

An effect that the host provides. Your code declares +Console, the host either provides a Console handler or doesn't. If it doesn't, compile error. Effects are capabilities — permissions to perform side effects.

Closure

See Quotation. "Closure" is the Rust/ML name for the same construct; Silo calls it a quotation by tradition, but the two terms refer to the same thing: a block of code that captures bindings from its enclosing scope.

Concatenative

A style of language where programs are built by composing words rather than applying named functions to named arguments. Silo, Forth, Factor, and Joy are concatenative. Every word reads from and writes to a shared stack; writing two words next to each other composes their effects. See Welcome and Stack and Words.

Constraint block

The { (Trait Type) } syntax after a signature. Restricts what types a generic function accepts: { (Eq a) (Display a) } means "a must be equatable and displayable."

Dependent type

A type that depends on a value. (Vec Int | 5) is a vector of 5 integers — the 5 is a value that's part of the type. The compiler checks these at compile time. See The Type System.

Derive list

The [Display Eq Ord] syntax on type declarations. Tells the compiler to auto-generate trait implementations for the type. On newtypes, [*] means "derive every trait the wrapped type derives" and -TraitName opts out of a specific one — e.g. [* -Display] inherits everything except Display.

Divergence

The +Div effect, carried by any word whose termination the compiler cannot prove statically. Silo is total by default; marking a word with +Div is how you opt into allowing non-termination. Callers see +Div in the word's signature and propagate it. See Effects, Totality, and Divergence.

Effect annotation

The +Effect syntax after a signature: :fn greet ( Str -> ) +Console. Declares that this function uses the Console capability.

Effect handler

The host-side (typically Rust) implementation of a declared effect. When silo code runs an effectful operation like print, the abstract machine doesn't perform I/O directly — it hands the request to the host, which dispatches to the effect handler registered for that effect. See Welcome and Effects, Totality, and Divergence.

Effect row

The +Foo +Bar … tail on a stack-effect signature, listing the effects the word may perform. Effects are tracked statically and propagate up the call graph: a word that calls a +Console word must itself declare +Console (or handle it). See Effects, Totality, and Divergence.

Exhaustiveness

The compile-time check that every possible value of the scrutinee is covered by some arm of a :match, :if-let, or :let. Missing cases are a compile error. See Control Flow and Pattern Matching.

Existential type

A type where you know the trait but not the concrete type. Display in a type position means "some value that implements Display, but I don't know what type it is." The compiler uses dynamic dispatch (vtable) for these.

Forward propagation

How Silo's type checker works. It starts at the beginning of a function, tracks what's on the stack, and walks forward through each word, updating the stack types as it goes. Contrast with Hindley-Milner inference which solves constraints globally.

Higher-kinded type (HKT)

A type that takes another type as a parameter, where the parameter itself takes parameters. Option is kind * -> * (takes a type, produces a type). HashMap is kind * -> * -> *. Lets you write traits like Mappable that work on any container, not just specific ones.

Higher-order function

A word or method that takes a quotation as one of its arguments. .map, .filter, .fold, .for-each, while, and times are all higher-order. See Quotations and Higher-Order Functions.

Host

The runtime environment Silo runs under. Typically a Rust program that builds a frontend, compiles source, and drives the abstract machine. The host declares which effects it supports; silo code that uses only those effects is portable across any host that provides them. See Welcome.

Inherent impl

Methods defined directly on a type, not associated with any trait: :impl Foo .distance ( Foo -> F64 ) ... :end. These belong to the type itself. Distinct from trait impls (:impl (Eq Foo)) which implement a trait for a type.

Init block

A :init ... :end declaration that runs before :main. Can create named words (module-scoped runtime constants) and register aspect handlers. :deinit runs after main for cleanup.

Kind

The "type of a type." Int has kind * (it's a concrete type). Option has kind * -> * (it's a type constructor that takes one argument). The compiler checks that type constructors are applied to the right number of arguments.

Linear type

A value that must be used exactly once. In Silo, values on the stack are linear by default — each stack slot has exactly one owner. dup introduces sharing (making copies affine). drop explicitly discards.

Local binding

The pop-> and peek-> forms for giving a stack value a name. pop-> name pops the top of the stack and binds it; peek-> name copies the top and leaves it on the stack. Both are lexically scoped to the enclosing word or quotation. See Stack and Words.

Monomorphisation

Compiling a generic function into concrete type-specific versions. When you call sort on integers, the compiler generates a version of sort specialised for integers with direct calls to the integer comparison function. No runtime dispatch overhead.

Never

The bottom type — a primitive with no values. An expression of type Never provably doesn't return, so code downstream is unreachable and the compiler lets it have any type through vacuous coercion. Used by panic, .exit, and any operation that doesn't return. See The Type System and Pattern Matching for the isomorphism rules that make Never useful in return positions.

Newtype

A :type declaration that creates a distinct type wrapping an existing one: :type UserId Int. Zero runtime cost but the compiler treats UserId and Int as different types. The escape hatch for type-level control.

Orphan impl

A trait implementation defined in a package that owns neither the trait nor any of the types involved. Must be explicitly imported via :impl in a :use block. Contrast with type-crate and trait-crate impls, which come automatically when their type or trait is in scope.

Output variadic

A calling convention where a word produces a statically-known number of outputs and pushes that count last so callers can consume it. .collect uses output variadics to turn a quotation that pushes n values into a Vec of exactly n elements — the length ends up in the Vec's type. See Quotations and Higher-Order Functions and Variadics and Reflection.

Perceus

The reference counting algorithm Silo uses (from Koka). The compiler inserts dup/drop operations, then optimises them away via drop specialisation and reuse analysis. The goal: most values are unique (refcount 1) and can be mutated in place.

Predicate

A compile-time-only type constraint with no runtime representation. :pred Positive ( (Int n) ) { (n 0 ">") }. The compiler checks it; the runtime never sees it. Inspired by theorem provers.

Quotation

A block of code as a value: [ 2 * ]. Has a type like [ Int -> Int ]. Can be passed around, stored, and called. Silo's version of anonymous functions / closures. See Quotations and Higher-Order Functions.

Region

A chunk of memory that's allocated and freed as a unit. Each function call gets its own region. When the function returns, the whole region is freed. Faster than individual allocations.

Row variable

A type variable that represents "the rest of the stack." In [ ..s Int -> ..s Int Int ], ..s is a row variable — the quotation works on any stack that has an Int on top, leaving everything below untouched. See Quotations and Higher-Order Functions.

Sans-IO

The VM design principle. The VM never performs I/O. It's a pure state machine: given an input, it produces outputs (including effect requests). The host performs actual I/O. This makes the VM deterministic, testable, and sandboxed. See Welcome.

Scoped impl

The visibility model for trait implementations. Type-crate impls (same package as the type) and trait-crate impls (same package as the trait) come into scope automatically when the type or trait is imported. Orphan impls (from a third package) require explicit :impl import. Silo has no orphan rule — anyone can write any impl — but orphans must be explicitly brought into scope.

Specialisation

When multiple trait impls match (a concrete one and a blanket one), the more specific (concrete) impl wins. (From Thing Widget) beats (From t v) { (v Default) }.

Stack

The single data stack every word reads from and writes to. Typed at compile time: the checker knows the shape of the stack at every point in the source. Displayed by the REPL with floor/ceiling brackets, top on the right: ⌊1 2 3⌉ means the top of the stack is 3. See Stack and Words.

Stack effect

The type of a word: ( inputs -> outputs ). Describes what a word consumes from the stack and what it produces. ( Int Int -> Int ) means "pop two ints, push one int." See Stack and Words.

Stack shuffler

A built-in polymorphic word for rearranging the top few values on the stack without touching their types: dup, drop, swap, over, rot, nip. Useful in short pipelines; for anything longer, reach for pop-> or peek-> because named bindings read better. See Stack and Words.

Total

A word is total if the compiler can prove it terminates on every input. Silo words are total by default — non-total words must carry the +Div effect. Totality is preserved through composition: calling a total word doesn't make your word non-total, but calling a +Div word does. See Control Flow and Effects, Totality, and Divergence.

Trait

An interface definition. Declares a set of operations that types can implement: :trait Eq self .eq ( self self -> Bool ) :end. A trait impl (:impl (Eq Point) ...) implements a trait for a specific type. Not to be confused with an inherent impl (:impl Point ...) which adds methods to a type without a trait. See Traits.

Unit

A primitive type with exactly one value, written unit. The intrinsic word unit has signature ( -> Unit ) and pushes that value onto the stack. Distinct from an empty output side in a stack effect — ( Str -> ) produces zero slots; ( Str -> Unit ) produces one slot holding unit. Useful in generic contexts like (Result Unit err) where you need a type parameter but have no meaningful value to carry. See The Type System.

Word

A function, in the Forth tradition. Silo calls them words mostly because "function" already means something in algebraic terms and "word" is the name the concatenative family has used for fifty years. Declared with :fn. See Welcome and Stack and Words.

Academic and Research Background

Algorithm W

The classic type inference algorithm for Hindley-Milner type systems (Milner 1978). Walks the syntax tree, generates fresh type variables, unifies constraints. Produces principal types. λ◦ uses a variant of this for concatenative type inference.

De Bruijn index

A way to represent variable binding without names. Instead of λx. λy. x, you write λ. λ. 1 (the variable bound 1 level up). Avoids naming conflicts. Used internally by Reliquary's core calculus.

Drop specialisation

A Perceus optimisation. Instead of a generic drop(x) that checks the type at runtime, the compiler generates a drop specialised for each constructor: "if unique, free the Cons node and drop its children; otherwise just decrement." Eliminates most RC operations on the fast path.

Evidence passing

Koka's compilation technique for effects. Instead of capturing continuations, handlers in scope are passed down the call chain as an "evidence vector." Each function receives the evidence it needs to dispatch effect operations. Compiles to efficient C without a runtime.

FBIP (Functional But In-Place)

A programming paradigm from Koka/Perceus. If your data is unique (refcount 1), purely functional operations like map execute via in-place mutation. The compiler guarantees this through reuse analysis. You write functional code; it runs imperatively.

Hindley-Milner (HM)

The standard type system for ML-family languages. Key properties: parametric polymorphism (generics), let-polymorphism (generalisation at let-bindings), complete type inference (you never need to write type annotations). λ◦ adapts HM for concatenative languages.

Infinitary unification

When unifying two type sequences that both contain sequence variables in arbitrary positions, there may be infinitely many solutions. λ◦ avoids this by restricting sequence variables to the leftmost position, making unification unitary (exactly one most general solution).

Lambda-circle (λ◦)

Kleffner's formal calculus for typed concatenative languages. Expressions are lists of words. Types are stack effects i → o with sequence variables. Proved sound with a complete inference algorithm.

Linear resource calculus (λ₁)

The formal system used to prove Perceus correct. Based on linear logic — every resource (reference) must be consumed exactly once. Perceus is proved sound (never drops a live reference) and garbage-free (never retains a dead one) in this calculus.

Mechanisation

Encoding a formal proof in a machine-checked theorem prover (Isabelle, Coq, Lean). If the prover accepts it, the proof is correct by construction. Watt mechanised WebAssembly's type soundness, finding real bugs the paper proofs missed.

Modular implicits

OCaml's approach to scoped typeclass instances. Instead of global resolution (Haskell) or explicit dictionary passing (ML functors), instances are resolved from what's in scope. Directly influenced Silo's scoped impl design.

Pi type (Π)

Dependent function type. Π(x:A). B(x) means "a function that takes an x of type A and returns a value whose type depends on x." The dependent version of A → B. Used by Reliquary's core calculus.

Polycyclic monoid

The algebraic structure that Pöial's stack effects form. A monoid (has identity and associative composition) with inverses (swap inputs and outputs) and a zero element (type error). Proved isomorphic to stack effects by Nivat & Perrot (1970).

Principal type

The most general type that can be assigned to an expression. If an expression has principal type ∀a. a → a, then every other valid type for it (like Int → Int) is an instance of the principal type. HM inference guarantees principal types.

Progress

Half of type soundness. "A well-typed program is never stuck." Either it's finished (a value), it's an error (Trap), or it can take a step. If progress holds, well-typed programs always do something — they don't silently freeze.

Preservation

The other half of type soundness. "If a well-typed program takes a step, the result is still well-typed." Types are preserved across evaluation steps. Together with progress: well-typed programs don't go wrong.

Rank-n polymorphism

The ability to have polymorphic types nested inside other types. Rank-1: ∀a. a → a (the ∀ is at the outside). Rank-2: (∀a. a → a) → Int (a function that takes a polymorphic function). Typing call in a concatenative language needs at least rank-2. Silo sidesteps this via forward propagation instead of full HM inference.

Refinement type

A type plus a predicate: { x:Int | x ">" 0 }. The type checker (or an SMT solver) verifies the predicate holds. Helmholtz uses refinement types on Michelson stacks. Silo's predicates are a restricted form of refinement types.

Resurrection hypothesis

From Lean 4's "Counting Immutable Beans." When you want to construct a value, there's usually a recently deconstructed value of the same size available for reuse. In concatenative code, this is even more true — "pop old, push new" is the dominant pattern.

Reuse analysis

A Perceus optimisation. When a match destructures a value and the branch constructs a new value of the same size, the compiler pairs them. If the original is unique at runtime, its memory is reused directly without allocation.

Row polymorphism (academic)

A form of polymorphism over extensible records or rows. ⟨exn, div | μ⟩ means "a row containing exn and div, plus whatever else μ contains." Used by Koka for effects and conceptually by Silo for stack effects (row variables = "rest of the stack").

Sequence variable

λ◦'s term for a type variable that ranges over sequences of types, not just single types. Written ᾱ (with an overline). The stack-polymorphism mechanism: ᾱ Int → ᾱ Int Int means "whatever's on the stack, plus an Int on top."

Sigma type (Σ)

Dependent pair type. Σ(x:A). B(x) means "a pair where the type of the second element depends on the value of the first." The dependent version of A × B. Reliquary encodes stacks as nested Σ-types.

Soundness

A type system is sound if well-typed programs never "go wrong" — never reach an undefined state. Formally: progress + preservation. If a type system is sound, the types are trustworthy. If unsound, the types can lie.

SpecTec

WebAssembly's DSL for authoring the formal specification. A single source generates the spec document, a reference interpreter, and (planned) theorem prover mechanisations. Adopted by the Wasm Community Group in 2025.

Stack-polymorphic

An instruction whose entire stack effect is unconstrained. In WebAssembly, unreachable and br are stack-polymorphic — after an unconditional branch, the dead code can have any type. Different from value-polymorphic (like drop, which works on any single value but has a fixed stack shape).

Substructural type system

A type system that restricts how values can be used. Linear: exactly once. Affine: at most once. Relevant: at least once. Ordered: in order. Silo combines ordered (stack discipline) with affine (compiler-managed dup/drop).

Unification

Finding a substitution that makes two types equal. To unify (List a) with (List Int), substitute a = Int. The core operation in type inference. Silo's forward propagation does a form of unification at each word boundary.

Unitary unification

When a unification problem has at most one most general solution. λ◦ restricts sequence variables to the leftmost position to ensure unification is unitary. Without this restriction, sequence unification can have infinitely many solutions.

Value-polymorphic

An instruction that works on any single value type but has a fixed stack shape. WebAssembly's drop is value-polymorphic: it pops one value of any type. Different from stack-polymorphic (where the entire stack effect is unconstrained).

Vtable

A table of function pointers used for dynamic dispatch. When you have an existential type (you know the trait but not the concrete type), the vtable maps trait operations to the correct implementation for the hidden concrete type. Created at the point where a concrete value is coerced to an existential.