Source guide/A1-glossary.simd

1
2# Glossary
3
4A reference for the vocabulary used throughout the book. The first
5section covers Silo's language-level terminology and its system
6architecture. The second section covers the academic and research
7background behind Silo's design choices — useful if you want to
8follow footnotes into the literature.
9
10## Silo Concepts
11
12### Affine type
13
14A value that can be used at most once. After you consume it, it's
15gone. If you don't use it, the compiler drops it for you. Most
16values in Silo are affine. Contrast with *linear* (must be used
17exactly once) and *unrestricted* (use as many times as you want).
18
19### Algebraic effect
20
21A typed side effect that composes cleanly. "Algebraic" just means
22the effects combine according to simple laws (like addition) —
23`+Console +FileSystem` is the union, no special interaction. In
24practice: a function call where the implementation lives outside
25your program. The VM requests it, the host handles it. See
26[Effects, Totality, and Divergence](./10-effects.simd).
27
28### Arity variant
29
30A `/N`-suffixed variant of a built-in stack shuffler that operates
31on groups of `N` values rather than single values. `dup/2`
32duplicates the top pair; `swap/2` swaps the top two pairs; and so
33on. The bare `dup`/`drop`/`swap`/etc. are the arity-1 forms. See
34[Stack and Words](./02-stack-and-words.simd).
35
36### Aspect
37
38A cross-cutting concern with dynamic scoping. An aspect defines
39operations with default behaviour that can be overridden via
40`:with`. Think logging, tracing, metrics — behaviour you want to
41inject throughout a program without threading it through every
42function signature. See [Aspects](./11-aspects.simd).
43
44### Capability
45
46An effect that the host provides. Your code declares `+Console`,
47the host either provides a Console handler or doesn't. If it
48doesn't, compile error. Effects are capabilities — permissions to
49perform side effects.
50
51### Closure
52
53See [Quotation](#quotation). "Closure" is the Rust/ML name for the
54same construct; Silo calls it a quotation by tradition, but the
55two terms refer to the same thing: a block of code that captures
56bindings from its enclosing scope.
57
58### Concatenative
59
60A style of language where programs are built by *composing* words
61rather than applying named functions to named arguments. Silo,
62Forth, Factor, and Joy are concatenative. Every word reads from
63and writes to a shared stack; writing two words next to each
64other composes their effects. See [Welcome](./01-welcome.simd) and
65[Stack and Words](./02-stack-and-words.simd).
66
67### Constraint block
68
69The `{ (Trait Type) }` syntax after a signature. Restricts what
70types a generic function accepts: `{ (Eq a) (Display a) }` means
71"a must be equatable and displayable."
72
73### Dependent type
74
75A type that depends on a value. `(Vec Int | 5)` is a vector of 5
76integers — the `5` is a value that's part of the type. The
77compiler checks these at compile time. See
78[The Type System](./06-types.simd).
79
80### Derive list
81
82The `[Display Eq Ord]` syntax on type declarations. Tells the
83compiler to auto-generate trait implementations for the type.
84On newtypes, `[*]` means "derive every trait the wrapped type
85derives" and `-TraitName` opts out of a specific one — e.g.
86`[* -Display]` inherits everything except `Display`.
87
88### Divergence
89
90The `+Div` effect, carried by any word whose termination the
91compiler cannot prove statically. Silo is total by default;
92marking a word with `+Div` is how you opt into allowing
93non-termination. Callers see `+Div` in the word's signature and
94propagate it. See
95[Effects, Totality, and Divergence](./10-effects.simd).
96
97### Effect annotation
98
99The `+Effect` syntax after a signature:
100`:fn greet ( Str -> ) +Console`. Declares that this function
101uses the Console capability.
102
103### Effect handler
104
105The host-side (typically Rust) implementation of a declared
106effect. When silo code runs an effectful operation like `print`,
107the abstract machine doesn't perform I/O directly — it hands the
108request to the host, which dispatches to the effect handler
109registered for that effect. See [Welcome](./01-welcome.simd) and
110[Effects, Totality, and Divergence](./10-effects.simd).
111
112### Effect row
113
114The `+Foo +Bar …` tail on a stack-effect signature, listing the
115effects the word may perform. Effects are tracked statically and
116propagate up the call graph: a word that calls a `+Console` word
117must itself declare `+Console` (or handle it). See
118[Effects, Totality, and Divergence](./10-effects.simd).
119
120### Exhaustiveness
121
122The compile-time check that every possible value of the scrutinee
123is covered by some arm of a `:match`, `:if-let`, or `:let`.
124Missing cases are a compile error. See
125[Control Flow](./03-control-flow.simd) and
126[Pattern Matching](./08-pattern-matching.simd).
127
128### Existential type
129
130A type where you know the trait but not the concrete type.
131`Display` in a type position means "some value that implements
132Display, but I don't know what type it is." The compiler uses
133dynamic dispatch (vtable) for these.
134
135### Forward propagation
136
137How Silo's type checker works. It starts at the beginning of a
138function, tracks what's on the stack, and walks forward through
139each word, updating the stack types as it goes. Contrast with
140Hindley-Milner inference which solves constraints globally.
141
142### Higher-kinded type (HKT)
143
144A type that takes another type as a parameter, where the
145parameter itself takes parameters. `Option` is kind `* -> *`
146(takes a type, produces a type). `HashMap` is kind `* -> * -> *`.
147Lets you write traits like `Mappable` that work on any container,
148not just specific ones.
149
150### Higher-order function
151
152A word or method that takes a [quotation](#quotation) as one of
153its arguments. `.map`, `.filter`, `.fold`, `.for-each`, `while`,
154and `times` are all higher-order. See
155[Quotations and Higher-Order Functions](./04-quotations.simd).
156
157### Host
158
159The runtime environment Silo runs under. Typically a Rust program
160that builds a frontend, compiles source, and drives the abstract
161machine. The host declares which effects it supports; silo code
162that uses only those effects is portable across any host that
163provides them. See [Welcome](./01-welcome.simd).
164
165### Inherent impl
166
167Methods defined directly on a type, not associated with any
168trait: `:impl Foo .distance ( Foo -> F64 ) ... :end`. These
169belong to the type itself. Distinct from *trait impls*
170(`:impl (Eq Foo)`) which implement a trait for a type.
171
172### Init block
173
174A `:init ... :end` declaration that runs before `:main`. Can
175create named words (module-scoped runtime constants) and register
176aspect handlers. `:deinit` runs after main for cleanup.
177
178### Kind
179
180The "type of a type." `Int` has kind `*` (it's a concrete type).
181`Option` has kind `* -> *` (it's a type constructor that takes
182one argument). The compiler checks that type constructors are
183applied to the right number of arguments.
184
185### Linear type
186
187A value that must be used exactly once. In Silo, values on the
188stack are linear by default — each stack slot has exactly one
189owner. `dup` introduces sharing (making copies affine). `drop`
190explicitly discards.
191
192### Local binding
193
194The `pop->` and `peek->` forms for giving a stack value a name.
195`pop-> name` pops the top of the stack and binds it; `peek->
196name` copies the top and leaves it on the stack. Both are
197lexically scoped to the enclosing word or quotation. See
198[Stack and Words](./02-stack-and-words.simd).
199
200### Monomorphisation
201
202Compiling a generic function into concrete type-specific
203versions. When you call `sort` on integers, the compiler
204generates a version of `sort` specialised for integers with
205direct calls to the integer comparison function. No runtime
206dispatch overhead.
207
208### Never
209
210The **bottom type** — a primitive with no values. An
211expression of type `Never` provably doesn't return, so code
212downstream is unreachable and the compiler lets it have any
213type through vacuous coercion. Used by `panic`, `.exit`, and
214any operation that doesn't return. See
215[The Type System](./06-types.simd#unit-and-never) and
216[Pattern Matching](./08-pattern-matching.simd) for the
217isomorphism rules that make `Never` useful in return
218positions.
219
220### Newtype
221
222A `:type` declaration that creates a distinct type wrapping an
223existing one: `:type UserId Int`. Zero runtime cost but the
224compiler treats `UserId` and `Int` as different types. The
225escape hatch for type-level control.
226
227### Orphan impl
228
229A trait implementation defined in a package that owns neither
230the trait nor any of the types involved. Must be explicitly
231imported via `:impl` in a `:use` block. Contrast with type-crate
232and trait-crate impls, which come automatically when their type
233or trait is in scope.
234
235### Output variadic
236
237A calling convention where a word produces a statically-known
238*number* of outputs and pushes that count last so callers can
239consume it. `.collect` uses output variadics to turn a quotation
240that pushes `n` values into a `Vec` of exactly `n` elements —
241the length ends up in the Vec's type. See
242[Quotations and Higher-Order Functions](./04-quotations.simd)
243and
244[Variadics and Reflection](./19-variadic-and-reflection.simd).
245
246### Perceus
247
248The reference counting algorithm Silo uses (from Koka). The
249compiler inserts dup/drop operations, then optimises them away
250via drop specialisation and reuse analysis. The goal: most
251values are unique (refcount 1) and can be mutated in place.
252
253### Predicate
254
255A compile-time-only type constraint with no runtime
256representation. `:pred Positive ( (Int n) ) { (n 0 ">") }`. The
257compiler checks it; the runtime never sees it. Inspired by
258theorem provers.
259
260### Quotation
261
262A block of code as a value: `[ 2 * ]`. Has a type like
263`[ Int -> Int ]`. Can be passed around, stored, and called.
264Silo's version of anonymous functions / closures. See
265[Quotations and Higher-Order Functions](./04-quotations.simd).
266
267### Region
268
269A chunk of memory that's allocated and freed as a unit. Each
270function call gets its own region. When the function returns,
271the whole region is freed. Faster than individual allocations.
272
273### Row variable
274
275A type variable that represents "the rest of the stack." In
276`[ ..s Int -> ..s Int Int ]`, `..s` is a row variable — the
277quotation works on any stack that has an `Int` on top, leaving
278everything below untouched. See
279[Quotations and Higher-Order Functions](./04-quotations.simd).
280
281### Sans-IO
282
283The VM design principle. The VM never performs I/O. It's a pure
284state machine: given an input, it produces outputs (including
285effect requests). The host performs actual I/O. This makes the
286VM deterministic, testable, and sandboxed. See
287[Welcome](./01-welcome.simd).
288
289### Scoped impl
290
291The visibility model for trait implementations. Type-crate impls
292(same package as the type) and trait-crate impls (same package
293as the trait) come into scope automatically when the type or
294trait is imported. Orphan impls (from a third package) require
295explicit `:impl` import. Silo has no orphan rule — anyone can
296write any impl — but orphans must be explicitly brought into
297scope.
298
299### Specialisation
300
301When multiple trait impls match (a concrete one and a blanket
302one), the more specific (concrete) impl wins.
303`(From Thing Widget)` beats `(From t v) { (v Default) }`.
304
305### Stack
306
307The single data stack every word reads from and writes to. Typed
308at compile time: the checker knows the shape of the stack at
309every point in the source. Displayed by the REPL with
310floor/ceiling brackets, top on the right: `⌊1 2 3⌉` means the
311top of the stack is `3`. See
312[Stack and Words](./02-stack-and-words.simd).
313
314### Stack effect
315
316The type of a word: `( inputs -> outputs )`. Describes what a
317word consumes from the stack and what it produces.
318`( Int Int -> Int )` means "pop two ints, push one int." See
319[Stack and Words](./02-stack-and-words.simd).
320
321### Stack shuffler
322
323A built-in polymorphic word for rearranging the top few values
324on the stack without touching their types: `dup`, `drop`,
325`swap`, `over`, `rot`, `nip`. Useful in short pipelines; for
326anything longer, reach for `pop->` or `peek->` because named
327bindings read better. See
328[Stack and Words](./02-stack-and-words.simd).
329
330### Total
331
332A word is total if the compiler can prove it terminates on
333every input. Silo words are total by default — non-total words
334must carry the `+Div` effect. Totality is preserved through
335composition: calling a total word doesn't make your word
336non-total, but calling a `+Div` word does. See
337[Control Flow](./03-control-flow.simd) and
338[Effects, Totality, and Divergence](./10-effects.simd).
339
340### Trait
341
342An interface definition. Declares a set of operations that
343types can implement:
344`:trait Eq self .eq ( self self -> Bool ) :end`. A *trait impl*
345(`:impl (Eq Point) ...`) implements a trait for a specific
346type. Not to be confused with an *inherent impl*
347(`:impl Point ...`) which adds methods to a type without a
348trait. See [Traits](./09-traits.simd).
349
350### Unit
351
352A primitive type with exactly one value, written `unit`. The
353intrinsic word `unit` has signature `( -> Unit )` and pushes
354that value onto the stack. Distinct from an empty output side
355in a stack effect — `( Str -> )` produces zero slots;
356`( Str -> Unit )` produces one slot holding `unit`. Useful in
357generic contexts like `(Result Unit err)` where you need a
358type parameter but have no meaningful value to carry. See
359[The Type System](./06-types.simd#unit-and-never).
360
361### Word
362
363A function, in the Forth tradition. Silo calls them words
364mostly because "function" already means something in algebraic
365terms and "word" is the name the concatenative family has used
366for fifty years. Declared with `:fn`. See
367[Welcome](./01-welcome.simd) and
368[Stack and Words](./02-stack-and-words.simd).
369
370## Academic and Research Background
371
372### Algorithm W
373
374The classic type inference algorithm for Hindley-Milner type
375systems (Milner 1978). Walks the syntax tree, generates fresh
376type variables, unifies constraints. Produces principal types.
377λ◦ uses a variant of this for concatenative type inference.
378
379### De Bruijn index
380
381A way to represent variable binding without names. Instead of
382`λx. λy. x`, you write `λ. λ. 1` (the variable bound 1 level
383up). Avoids naming conflicts. Used internally by Reliquary's
384core calculus.
385
386### Drop specialisation
387
388A Perceus optimisation. Instead of a generic `drop(x)` that
389checks the type at runtime, the compiler generates a `drop`
390specialised for each constructor: "if unique, free the Cons
391node and drop its children; otherwise just decrement."
392Eliminates most RC operations on the fast path.
393
394### Evidence passing
395
396Koka's compilation technique for effects. Instead of capturing
397continuations, handlers in scope are passed down the call chain
398as an "evidence vector." Each function receives the evidence it
399needs to dispatch effect operations. Compiles to efficient C
400without a runtime.
401
402### FBIP (Functional But In-Place)
403
404A programming paradigm from Koka/Perceus. If your data is
405unique (refcount 1), purely functional operations like `map`
406execute via in-place mutation. The compiler guarantees this
407through reuse analysis. You write functional code; it runs
408imperatively.
409
410### Hindley-Milner (HM)
411
412The standard type system for ML-family languages. Key
413properties: parametric polymorphism (generics),
414let-polymorphism (generalisation at let-bindings), complete
415type inference (you never need to write type annotations). λ◦
416adapts HM for concatenative languages.
417
418### Infinitary unification
419
420When unifying two type sequences that both contain sequence
421variables in arbitrary positions, there may be infinitely many
422solutions. λ◦ avoids this by restricting sequence variables to
423the leftmost position, making unification unitary (exactly one
424most general solution).
425
426### Lambda-circle (λ◦)
427
428Kleffner's formal calculus for typed concatenative languages.
429Expressions are lists of words. Types are stack effects `i → o`
430with sequence variables. Proved sound with a complete
431inference algorithm.
432
433### Linear resource calculus (λ₁)
434
435The formal system used to prove Perceus correct. Based on
436linear logic — every resource (reference) must be consumed
437exactly once. Perceus is proved sound (never drops a live
438reference) and garbage-free (never retains a dead one) in this
439calculus.
440
441### Mechanisation
442
443Encoding a formal proof in a machine-checked theorem prover
444(Isabelle, Coq, Lean). If the prover accepts it, the proof is
445correct by construction. Watt mechanised WebAssembly's type
446soundness, finding real bugs the paper proofs missed.
447
448### Modular implicits
449
450OCaml's approach to scoped typeclass instances. Instead of
451global resolution (Haskell) or explicit dictionary passing (ML
452functors), instances are resolved from what's in scope.
453Directly influenced Silo's scoped impl design.
454
455### Pi type (Π)
456
457Dependent function type. `Π(x:A). B(x)` means "a function that
458takes an `x` of type `A` and returns a value whose type depends
459on `x`." The dependent version of `A → B`. Used by Reliquary's
460core calculus.
461
462### Polycyclic monoid
463
464The algebraic structure that Pöial's stack effects form. A
465monoid (has identity and associative composition) with inverses
466(swap inputs and outputs) and a zero element (type error).
467Proved isomorphic to stack effects by Nivat & Perrot (1970).
468
469### Principal type
470
471The most general type that can be assigned to an expression.
472If an expression has principal type `∀a. a → a`, then every
473other valid type for it (like `Int → Int`) is an instance of
474the principal type. HM inference guarantees principal types.
475
476### Progress
477
478Half of type soundness. "A well-typed program is never stuck."
479Either it's finished (a value), it's an error (Trap), or it
480can take a step. If progress holds, well-typed programs always
481do something — they don't silently freeze.
482
483### Preservation
484
485The other half of type soundness. "If a well-typed program
486takes a step, the result is still well-typed." Types are
487preserved across evaluation steps. Together with progress:
488well-typed programs don't go wrong.
489
490### Rank-n polymorphism
491
492The ability to have polymorphic types nested inside other
493types. Rank-1: `∀a. a → a` (the ∀ is at the outside). Rank-2:
494`(∀a. a → a) → Int` (a function that takes a polymorphic
495function). Typing `call` in a concatenative language needs at
496least rank-2. Silo sidesteps this via forward propagation
497instead of full HM inference.
498
499### Refinement type
500
501A type plus a predicate: `{ x:Int | x ">" 0 }`. The type checker
502(or an SMT solver) verifies the predicate holds. Helmholtz
503uses refinement types on Michelson stacks. Silo's predicates
504are a restricted form of refinement types.
505
506### Resurrection hypothesis
507
508From Lean 4's "Counting Immutable Beans." When you want to
509construct a value, there's usually a recently deconstructed
510value of the same size available for reuse. In concatenative
511code, this is even more true — "pop old, push new" is the
512dominant pattern.
513
514### Reuse analysis
515
516A Perceus optimisation. When a `match` destructures a value
517and the branch constructs a new value of the same size, the
518compiler pairs them. If the original is unique at runtime, its
519memory is reused directly without allocation.
520
521### Row polymorphism (academic)
522
523A form of polymorphism over extensible records or rows.
524`⟨exn, div | μ⟩` means "a row containing exn and div, plus
525whatever else μ contains." Used by Koka for effects and
526conceptually by Silo for stack effects (row variables = "rest
527of the stack").
528
529### Sequence variable
530
531λ◦'s term for a type variable that ranges over sequences of
532types, not just single types. Written `ᾱ` (with an overline).
533The stack-polymorphism mechanism: `ᾱ Int → ᾱ Int Int` means
534"whatever's on the stack, plus an Int on top."
535
536### Sigma type (Σ)
537
538Dependent pair type. `Σ(x:A). B(x)` means "a pair where the
539type of the second element depends on the value of the first."
540The dependent version of `A × B`. Reliquary encodes stacks as
541nested Σ-types.
542
543### Soundness
544
545A type system is sound if well-typed programs never "go wrong"
546— never reach an undefined state. Formally: progress +
547preservation. If a type system is sound, the types are
548trustworthy. If unsound, the types can lie.
549
550### SpecTec
551
552WebAssembly's DSL for authoring the formal specification. A
553single source generates the spec document, a reference
554interpreter, and (planned) theorem prover mechanisations.
555Adopted by the Wasm Community Group in 2025.
556
557### Stack-polymorphic
558
559An instruction whose entire stack effect is unconstrained. In
560WebAssembly, `unreachable` and `br` are stack-polymorphic —
561after an unconditional branch, the dead code can have any
562type. Different from value-polymorphic (like `drop`, which
563works on any single value but has a fixed stack shape).
564
565### Substructural type system
566
567A type system that restricts how values can be used. Linear:
568exactly once. Affine: at most once. Relevant: at least once.
569Ordered: in order. Silo combines ordered (stack discipline)
570with affine (compiler-managed dup/drop).
571
572### Unification
573
574Finding a substitution that makes two types equal. To unify
575`(List a)` with `(List Int)`, substitute `a = Int`. The core
576operation in type inference. Silo's forward propagation does a
577form of unification at each word boundary.
578
579### Unitary unification
580
581When a unification problem has at most one most general
582solution. λ◦ restricts sequence variables to the leftmost
583position to ensure unification is unitary. Without this
584restriction, sequence unification can have infinitely many
585solutions.
586
587### Value-polymorphic
588
589An instruction that works on any single value type but has a
590fixed stack shape. WebAssembly's `drop` is value-polymorphic:
591it pops one value of any type. Different from stack-polymorphic
592(where the entire stack effect is unconstrained).
593
594### Vtable
595
596A table of function pointers used for dynamic dispatch. When
597you have an existential type (you know the trait but not the
598concrete type), the vtable maps trait operations to the correct
599implementation for the hidden concrete type. Created at the
600point where a concrete value is coerced to an existential.