Prism

Prism is a small, strict, impure functional language in the ML family whose type system tracks side effects. Effects are inferred, extensible rows that combine structurally as functions call one another, and they track observability: an effect handled inside a function vanishes from its type. The core is a call-by-push-value calculus in A-normal form that compiles to native code through LLVM, with memory managed by deterministic reference counting and fully-in-place update rather than a garbage collector.

This book has four parts:

• Language Specification defines the surface language: lexical structure, grammar, types, effects, and evaluation.
• Compiler documents the implementation: the pipeline, the core calculus, effect lowering, reference counting, the backends, and the verification harness.
• Standard Library is the API reference for the prelude and the standard modules, generated from their source by prism docs.
• Semantics is an unverified sketch of the Core terms and types.

Use the Playground to edit, run, and inspect Prism code via an interpreter run in the browser.

The Prism Language Specification

Prism is a strict, impure functional language in the ML family whose type system tracks side effects. This document is a Modest Proposal of the language as the prism compiler accepts it: its lexical structure, grammar, type system, and evaluation.

0. Goals

1. Take deterministic simulation testing down to the language level: a deterministic core, typed effects, content-addressed identity, and replayable observations make every output an accountable artifact that can be mechanically rebuilt, moved, cached, diffed, audited, and explained using modern type-system methods.
2. Lineage is the user-facing form of determinism: given an output, Prism should be able to precisely describe and check what code, packages, inputs, effects, handlers, and compiler artifacts produced it.
3. The so-called “real world” meets Prism only at effect boundaries: every nondeterministic observation is named, typed, handled, and therefore available to record, replay, sandbox, or audit. The unfortunate existence of the physical world should be constrained by types.
4. Obtain pure functional language nirvana by being completely inaccessible, utterly useless, completely divorced from the real world, and having zero users.

1. Introduction

A Prism program is a set of modules, each a file of declarations. The surface language elaborates to a strict, call-by-push-value core (Levy, 2004) in A-normal form (the companion Compiler document), compiles to native code through LLVM, and is managed by deterministic reference counting rather than a garbage collector.

Three things distinguish Prism from its ML and Haskell ancestors. It is strict, with laziness opt-in through thunks over a call-by-push-value core, so evaluation and effect order are left to right and explicit. Side effects are inferred as extensible effect rows (effects and handlers) that combine structurally across calls instead of through monads and track both observability and capability effects (capability effects and IO): an operation handled inside a function does not appear in its type, so internally effectful code is reused as pure, and a function that reads the outside world names the part it reads (Console, FileSystem, Random, Env) rather than a blanket IO. The same reference-count discipline both frees memory and performs fully-in-place (FBIP) update (declarations and programs), compiling record updates and derived setters to in-place writes on uniquely owned values (those that a reference count proves have no other live reference; see reference counting and FBIP reuse). Beyond these, the language provides isolated fibers through handlers, failure as ordinary typed control flow, record and replay of a program’s interaction with the world over the capability effects (record and replay), derived lenses and use-site optic paths for deeply nested structure traversal and update (optic paths), fusing stream combinators (streams), unboxed types (unboxed products), and checked usage contracts on closures (coeffects).

The deterministic core gives programs a stable identity: a definition is named by the hash of its canonical Core form, after alpha-normalizing binders so alpha-equivalent definitions share an identity and behavior-visible Core changes do not (content-addressed core).¹ The same rule extends to execution: a suspended continuation is a kont envelope whose bundle digest names the code it may resume against (the kont envelope), and replayability supplies the byte-identical observable contract (suspend and resume).

This specification proceeds in dependency order: notation, lexical structure, grammar, types, then the constructs the grammar describes.

2. Notation

Grammar is given in the following EBNF. A terminal is a literal token written in double quotes; a nonterminal is a lower-case name. The character classes are the ASCII letters (letter), the two cases (lower, upper), the decimal digits (digit), any printable character (graphic), and any character other than ", \, or a newline (strchar). These are primitives, not grammar nonterminals.

x  y      juxtaposition: x followed by y
x | y     alternative: x or y
[ x ]     option: zero or one x
{ x }     repetition: zero or more x
( x )     grouping
"fn"      a terminal (literal token), in double quotes
varid     a nonterminal, in lower case
x , ...   a comma-separated list of one or more x

Identifiers in productions name the tokens defined in the lexical structure (varid, conid, qualid, integer, float, char, string) and the character classes defined just above. The layout algorithm inserts block delimiters that the grammar then treats as ordinary terminals.

3. Lexical Structure

Source text is UTF-8. Tokens are lexed by longest match, then the stream is rewritten by the layout algorithm. Whitespace and comments separate tokens and are otherwise insignificant except as layout boundaries.

varid    ->  (lower | "_") { idchar }
conid    ->  upper { idchar }
qualid   ->  conid "." ident { "." ident }
ident    ->  varid | conid
idchar   ->  letter | digit | "_"

integer  ->  digits [ "i64" | "u64" ]
float    ->  digits "." digits [ exponent ]
          |  digits exponent
exponent ->  ( "e" | "E" ) [ "+" | "-" ] digits
-- A digit separator "_" is admissible only flanked by two digits, so leading,
-- trailing, doubled, and adjacent-to-"."/"e" separators are rejected. Exponent
-- notation always denotes a float; the exponent sign lives in the lexer and does
-- not collide with the unary-minus operator.
digits   ->  digit { [ "_" ] digit }
char     ->  "'" ( graphic | escape | "\\'" ) "'"
string   ->  "\"" { strchar | escape | interp } "\""
interp   ->  "{" expr "}"
escape   ->  "\\" ( "n" | "t" | "r" | "\\" | "{" | "}" | "\"" )
comment  ->  "--" { any character other than newline }

-- An interpolated string "a{e}b{e}c" is lexed into the pieces below, each
-- carrying its literal segment; the holes are re-lexed as expressions.
istart   ->  "\"" { strchar } "{"
imid     ->  "}" { strchar } "{"
iend     ->  "}" { strchar } "\""

-- Virtual layout tokens, synthesized by the offside pass; no source spelling.
vopen    ->  "v{"   -- start of an indented block
vclose   ->  "v}"   -- end of an indented block
vsep     ->  "v;"   -- a newline at the same column (item / statement separator)

3.1 Identifiers

Prism distinguishes identifiers by initial case. A varid begins with a lower-case letter or underscore and names a variable, function, parameter, or record field. A conid begins with an upper-case letter and names a type, data constructor, type class, or effect. A qualid is a dotted path such as Data.Map or Map.insert; it is lexed as a single token so that a module path never collides with field access.

3.2 Keywords

The following are reserved and may not be used as identifiers.

A second set of words is contextual: each names a construct only in one grammatical position and stays a valid identifier everywhere else, so no program is broken by one becoming meaningful. They are never reserved.

The built-in type names Int, I64, U64, Bool, Unit, Float, Char, and String are also reserved. The prelude effect names Console, FileSystem, Random, and Env, the capability effects, are reserved as well.

3.3 Operators and Punctuation

The operator set is fixed; the language has no user-defined operators. Arithmetic and comparison use one plain spelling per operation across the numeric lanes; the older floating-point dot forms remain as deprecated aliases during the migration window. Exponentiation ^ is a single operator over both Int and Float (exponentiation).

3.4 Literals

An integer is a run of decimal digits, optionally grouped by underscore separators (1_000_000) that are cosmetic and carry no value. A value that fits in a machine word is an immediate; a larger literal is an arbitrary-precision integer (bignum). The suffix i64 or u64 selects a fixed-width 64-bit lane that wraps on overflow. A float is an IEEE-754 double, written with a fractional part (1.5), an exponent (1e25, 1.5e3), or both; the exponent may be signed (1e-25, 1E25) and separators are admitted in its mantissa and exponent on the same rule. Exponent notation always denotes a Float. A separator is valid only between two digits, so a leading, trailing, doubled, or ./e-adjacent underscore is a lexical error. A char is a single Unicode scalar in single quotes. A string is double-quoted UTF-8.

There are no negative literals at the lexical level: a leading minus is the unary-minus operator (operator precedence), so -5, -5i64, and -1.5 are - applied to the literal. -5u64 is rejected because negation is undefined on the unsigned lane, and the exponent sign lives inside the float token, so it never collides with that operator.² The formatter preserves a writer’s separator grouping verbatim.

The escape sequences \n, \t, \r, \\, \", \{, and \} are recognized in both character and string literals; a character literal additionally accepts \'.

3.5 String Interpolation

Within a string, an unescaped { expr } is an interpolation hole. The hole text is re-lexed at its source position and elaborated as an expression whose type-directed display is spliced into the string; a top-level string is spliced in raw, not quoted the way the Show method renders it. A hole runs to its matching }, balancing nested braces and string literals, so a hole may itself contain a string with braces. A literal brace outside a hole is written \{ or \}. An empty hole, an unterminated hole, and an unterminated string are each lexical errors. The catch arms of the error example under errors and failure use interpolation, as in "no such key: {k}".

3.6 Comments

A comment runs from -- to the end of the line; there is no block-comment form. Comments are trivia: they separate tokens and are otherwise insignificant, except that a -- inside a string or character literal is ordinary text rather than a comment, and the formatter preserves a comment and re-emits it attached to the token it preceded. A doc comment is the ordinary line form spelled -- |; the API doc generator harvests it, but the lexer treats it as any other comment.

3.7 Layout

Prism uses the offside rule: indentation, not explicit braces, delimits a block. A layout block opens after any of the keywords or symbols =, then, else, =>, of, with, handler, do, where, try, catch, transact, loop, and after fn (a while block opens at its do). A class, instance, or effect body opens the same way, but after the head rather than a keyword: the head ends the line and the members follow as its indented block. The first token after such an opener sets the block’s indentation column; a later line at that column starts a new item in the block, and a line indented less closes the block. Explicit { } override layout for expression blocks and may be used in place of an implicit one, as in the brace-delimited handler arms of the masking example. The three declaration bodies are the exception: they are layout-only, and a brace opening one is a parse error that names the layout rewrite.

3.8 Declarations

A program is a layout-delimited sequence of top-level declarations, each introduced by a reserved word that fixes its shape. The table names the introducer and where the construct is specified; the formal grammar is in Surface Grammar.

A head may carry modifiers. pub exports the declaration to importers; opaque on a type exports the name but not its constructors (modules); the fip and fbip prefixes on fn assert an allocation discipline and replayable bounds its effects; a deprecated "..." line marks the following declaration superseded (deprecation). The let and var binding forms (the latter mutable) also appear inside expression bodies, where only the local forms admit var; a top-level binding is let only.

A trailing where block attaches non-recursive local helpers below a function body, each binding scoped over the ones after it and over the body:

fn quadratic(a : Float, b : Float, c : Float) : (Float, Float) =
    ((0.0 - b + d) / two_a, (0.0 - b - d) / two_a)
  where
    d = sqrt(b * b - 4.0 * a * c)
    two_a = 2.0 * a

3.9 Modules and Imports

A file is a module and a dotted path names one in the source tree: import Data.Map loads Data/Map.pr. The surface forms are below; visibility, opaque exports, and project layout are specified in modules.

A qualid such as Map.insert is a single token (identifiers), so a qualified name never lexes as field projection. The pub modifier on any declaration makes it visible to importers; a declaration without it is private to its module.

Bringing a name into bare scope offers it; it does not commit to it. Two imports may offer the same short name, and an import never fails on that account: the clash is reported only where a bare use actually has to choose between them, and qualifying that one use resolves it. Modules gives the full order in which a bare name is looked up.

4. Surface Grammar

A program is a layout-delimited sequence of top-level declarations.

program   ->  { topdecl }                       -- separated by layout

topdecl   ->  [ deprecated ] [ "pub" | "opaque" ] item
deprecated -> "deprecated" string               -- annotation line: marks the next item superseded ("deprecated" is contextual, not reserved)
item      ->  import | datatype | newtype | synonym | rowalias
           |  classdecl | instancedecl | canonicaldecl | effectdecl
           |  errordecl | patterndecl | stabledecl | constdecl | fundecl

import    ->  "import" modpath [ "as" conid ] [ "(" name , ... ")" ]
           |  "pub" "import" modpath [ "(" name , ... ")" ]
modpath   ->  conid { "." conid }
name      ->  varid | conid

datatype  ->  "type" conid [ kindedvars ] "=" ctor { "|" ctor } [ deriving ]
newtype   ->  "newtype" conid [ tyvars ] "=" ctor [ deriving ]
synonym   ->  "alias" conid [ tyvars ] "=" type
rowalias  ->  "alias" conid "=" "{" [ label , ... ] "}"
tyvars    ->  "(" varid , ... ")"
kindedvars -> "(" tyvar , ... ")"               -- a data-type parameter may carry a kind
tyvar     ->  varid [ ":" kind ]
kind      ->  "Type" | "Row" | "Nat"            -- "Row" ranges over an effect row, "Nat" over a dimension
ctor      ->  conid [ "(" type , ... ")" ]
           |  conid "{" field , ... "}"
field     ->  varid ":" type
deriving  ->  "deriving" "(" conid , ... ")"

constdecl ->  "let" varid [ ":" type ] "=" expr
fundecl   ->  [ "logic" ] [ "test" ] [ [ "assume" ] "total" ] [ "replayable" ] [ "fip" | "fbip" ]
                "fn" varid "(" [ param , ... ] ")"
                [ retann ] [ given ] { requires } { ensures } "=" expr [ wheres ]
                -- a usage row spelling exactly "@ noalloc" at the root of the
                -- return annotation is the declaration's allocation certificate;
                -- "logic fn" is a proof-level (SMT) declaration, never a runtime fn;
                -- "test" and "total"/"assume" are contextual
                -- declaration modifiers, not reserved words, so all three stay
                -- usable as ordinary identifiers everywhere else
param     ->  [ "borrow" ] pattern [ ":" type ] [ ":=" expr ]
                -- a bare varid (or "_") is the ordinary named parameter and binds
                -- without testing; any other pattern is matched around the body and
                -- must be irrefutable, so it has no name to pass by keyword
retann    ->  ":" type [ decleff ]              -- result first, e.g. `: Int ! {State}`
decleff   ->  "!" "{" [ label , ... ] "}"       -- the declaration's effect row (closed)
           |  "!"                                -- an explicit empty effect row
given     ->  "given" constraint , ...
requires  ->  "requires" expr                    -- an SMT precondition clause
ensures   ->  "ensures" "|" varid "|" expr       -- an SMT postcondition over the result binder
constraint -> conid "(" type ")"
wheres    ->  "where" "{" { varid "=" expr } "}"

-- Class, instance, and effect bodies are layout blocks (no `where`, no braces):
-- the head ends the line and the members follow on indented lines. A brace here
-- is a parse error. A marker class or its instance has no members, so the body is
-- absent and the declaration is its bare head.
classdecl    ->  "class" conid "(" varid ")" [ given ] [ vopen sig { vsep sig } vclose ]
instancedecl ->  "instance" varid ":" conid "(" type ")" [ given ]
                   [ vopen fundecl { vsep fundecl } vclose ]
canonicaldecl -> "canonical" conid "(" type ")" "=" varid
sig          ->  varid ":" type

effectdecl   ->  "effect" conid [ tyvars ] vopen effop { vsep effop } vclose
effop        ->  grade varid "(" [ type , ... ] ")" ":" type
grade        ->  "ctl" | "fun" | "final" "ctl"  -- resumption multiplicity: many | once | never
errordecl    ->  "error" conid [ "(" type , ... ")" ]

patterndecl  ->  "pattern" conid "(" [ varid , ... ] ")" "for" conid "="
                   "view" expr [ "make" expr ]

-- A `stable` block declares a serializable type's frozen version history:
-- the rungs, then the hand-written converters for the
-- type mutations the compiler cannot generate. Real braces, so entries are
-- comma-separated. "frozen", "upgrade", "downgrade", and "drop_loss" are
-- contextual, recognized positionally inside the block rather than reserved.
stabledecl   ->  "stable" conid "{" stableitem , ... "}"
stableitem   ->  rung | converter
rung         ->  conid "=" "{" [ ".." conid "," ] rungfield , ... "}" [ "frozen" string ]
rungfield    ->  varid ":" type [ "=" expr ]     -- an additive field carries a default
converter    ->  ( "upgrade" | "downgrade" ) conid "->" conid "="
                   "{" ".." expr { "," varid "=" expr } "}" [ "drop_loss" "(" varid , ... ")" ]

Type syntax. A function type carries an optional effect row on its codomain (effects and handlers); the row binds to a function type only.

type    ->  "forall" varid { varid } "." type
         |  arrow [ row ]                       -- row applies to a function type
arrow   ->  "(" [ type , ... ] ")" "->" arrow   -- n-ary domain
         |  utype "->" arrow                     -- single domain
         |  utype
utype   ->  atype [ "@" usagerow ]              -- usage (coeffect) row on an atomic type
usagerow -> varid                               -- single-fact sugar: T @ noalloc
         |  "{" varid , ... "}"                 -- fact set, canonical order alphabetical
atype   ->  scalar
         |  "[" type "]"                          -- List(type)
         |  conid [ "(" typearg , ... ")" ]       -- type constructor
         |  varid [ "(" typearg , ... ")" ]       -- variable, possibly applied
         |  "(" type ")"
         |  "(" type "," type , ... ")"           -- tuple
typearg ->  type
         |  rowlit                                -- argument for a Row-kinded parameter
         |  digits                                 -- dimension literal for a Nat-kinded parameter, e.g. Vec(Int, 3)
rowlit  ->  "{" [ label , ... ] [ "|" varid ] "}" -- effect-row literal, e.g. Cmd(Int, {IO})
scalar  ->  "Int" | "I64" | "U64" | "Bool" | "Unit" | "Float" | "Char" | "String"

row     ->  "!" "{" [ label , ... ] [ "|" varid ] "}"
         |  "!"                                   -- empty row, effectful position
label   ->  conid [ "(" type , ... ")" ]

Expressions, patterns, and the handler block of handle/try (used in effects and handlers).

expr    ->  "if" expr "then" expr { "elif" expr "then" expr } "else" expr
         |  "let" ( varid | letpat ) "=" expr  expr -- bind, then continue
         |  "var" varid ":=" expr  expr             -- local mutable, then continue
         |  "\\" "(" [ param , ... ] ")" "->" expr  -- lambda
         |  "match" expr "of" { arm }
         |  "handle" expr "with" handler
         |  "with" [ varid "<-" ] "handler" handler  expr  -- scoped handler (named if `x <-`), then continue
         |  "with" [ varid "<-" ] appexpr  expr            -- scoped resource from a call, then continue
         |  "throw" conid [ "(" expr , ... ")" ]
         |  "try" expr "catch" { catcharm }
         |  "transact" expr "else" expr
         |  "for" gen { "," qual } "do" expr
         |  "while" expr "do" expr                    -- while loop
         |  "loop" expr                               -- unconditional loop
         |  "probe" string "do" expr                  -- named instrumentation; body runs only when enabled
         |  "return" expr                             -- early return
         |  varid ":=" expr                          -- assignment
         |  varid ( "+=" | "-=" | "*=" | "%=" ) expr  -- compound assignment
         |  opexpr

opexpr  ->  opexpr binop opexpr                      -- binop and binding per 4.1
         |  negexpr
negexpr ->  "-" negexpr                              -- unary minus, "tight prefix":
                                                     -- looser than application and
                                                     -- projection, tighter than every
                                                     -- binop, so `-f(x)` is `-(f(x))`
                                                     -- and `-x * y` is `(-x) * y`
         |  appexpr
appexpr ->  appexpr "(" [ arg , ... ] [ "using" iname , ... ] ")"
                                                     -- application; `using` selects instances
arg     ->  [ varid ":=" ] expr                      -- an argument may be passed by name
         |  appexpr "[" expr "]"                      -- indexed read a[i]
         |  appexpr "." varid                         -- field access
         |  appexpr "." varid "(" [ expr , ... ] ")" -- method call (UFCS)
         |  appexpr "?." varid                        -- optional chaining
         |  appexpr "?"                               -- try marker
         |  atom
atom    ->  integer | float | char | string | "true" | "false" | "(" ")"
         |  "break" | "continue"                      -- loop control
         |  "?" varid                                  -- named typed hole
         |  varid | conid | qualid
         |  "(" expr ")" | "(" expr ":" type ")"
         |  "(" expr "," expr , ... ")"               -- tuple
         |  "[" [ expr , ... ] "]"                    -- list
         |  "[" expr ".." expr "]"                    -- range
         |  "[" expr "for" gen { "," qual } "]"       -- comprehension
         |  conid "{" fieldval , ... "}"              -- record
         |  conid "{" ".." expr "," fieldval , ... "}" -- record update
         |  "{" expr "|" path "=" expr , ... "}"      -- path update
         |  "mask" "<" conid ">" "(" expr ")"

arm      ->  pattern [ "if" expr ] "=>" expr
gen      ->  varid "in" expr
qual     ->  "if" expr | "let" varid "=" expr
iname    ->  varid | qualid                          -- an instance name
fieldval ->  varid "=" expr                          -- a record field binding
path     ->  pathseg { "." pathseg }                 -- a nested field path
pathseg  ->  varid | "each" | "?" conid              -- field step, bulk map over a collection, or case-narrowing step
          |  pathseg "[" expr "]"                      -- indexed step
          |  "(" path "where" expr ")"                 -- filtered traversal
binop    ->  "??" | "|>" | ">>" | "<<" | "||" | "&&" -- binding given in 4.1
         |  "==" | "/=" | "<" | "<=" | ">" | ">="
         |  "+" | "-" | "*" | "/" | "%" | "^"
         |  "==." | "/=." | "<." | "<=." | ">." | ">=."
         |  "+." | "-." | "*." | "/."

pattern  ->  patalt { "|" patalt }                   -- alternation: any alternative matches
patalt   ->  conid [ "(" pattern , ... ")" ]         -- constructor
          |  conid "{" fieldpat , ... "}"            -- record, ".." allowed
          |  varid                                    -- variable binding
          |  "_"                                      -- wildcard
          |  integer | float | char | "true" | "false"
          |  "-" ( integer | float )                  -- negative literal

          |  "[" [ pattern , ... ] "]"                -- list
          |  "(" pattern "," pattern , ... ")"        -- tuple
fieldpat ->  varid "=" pattern  |  ".."
letpat   ->  conid [ "(" pattern , ... ")" ]         -- a `let` destructures with a
          |  "(" pattern "," pattern , ... ")"       -- constructor or tuple pattern only,
                                                     -- and admits no alternation

handler   ->  "{" hclause , ... "}"  |  hclause { hclause }   -- braces or layout

hclause   ->  "return" varid "=>" expr                 -- result transform
           |  varid "(" [ varid , ... ] ")" "resume" varid "=>" expr  -- multishot op: continuation after `resume`
           |  "fun" varid "(" [ varid , ... ] ")" "=>" expr      -- tail-resumptive sugar
           |  "final" "ctl" varid "(" [ varid , ... ] ")" "=>" expr  -- non-resumable
           |  "val" varid "=" expr                     -- install-time constant

catcharm  ->  conid [ "(" varid , ... ")" ] "=>" expr

4.1 Operator Precedence

The table gives the binding of each operator, loosest to tightest. Levels 1 to 9 are the binop operators of the grammar; level 10 is the prefix unary minus; level 11 is application, field access, and the postfix failure operators, which bind tighter than every binop. Unary minus is a tight prefix: it binds looser than application and projection but tighter than every binary operator, so -f(x) is -(f(x)), -x * y is (-x) * y, -x ^ y is (-x) ^ y, and a leading f -x is the binary f - x (there is no juxtaposition application; write f(-x)).

4.2 Syntax Stability

The surface has grown a broad vocabulary: handlers and named handlers, try/catch, throw, failure fallback, optional chaining, comprehensions, transactions, imperative loops, pattern synonyms, stable blocks, coeffects, allocation annotations, record paths, and source probes. Most are pure desugar onto the constructs described elsewhere in this document, but taken together they enlarge the language a reader must hold in mind, so new syntax is admitted under a single rule:

Add syntax only when it exposes a semantic invariant, eliminates recurring structural boilerplate, or materially improves diagnostics.

By that test effect rows, handlers, try/catch, var and the loop forms, and record update earn their place; so do pattern alternation and patterns in parameter position, which remove arms and wrapper matches a reader would otherwise write out by hand and which are expanded away before the checker, adding nothing to the language below the surface. Further aliases for forms that already exist do not. The stable surface freezes at roughly this point: the approachable ML-like character (no user-defined operators, no macros, no do-notation, no drift toward a more symbolic calculus) is a property to preserve, not a stage to move past. The design rule is to deepen what the existing syntax means rather than widen the syntax itself.

5. Types and Kinds

Prism infers types by the bidirectional, higher-rank inference algorithm of Dunfield & Krishnaswami (2013). An unannotated declaration infers its principal type; an annotated one is checked against the annotation. Annotations are required for rank-N polymorphism, since a nested forall cannot be inferred.

Quantification is predicative: a type-constructor argument and an inferred type variable range over monomorphic types, so a forall may not be written directly as a type argument (List(forall a. (a) -> a) is rejected as impredicative). Higher-rank types are allowed wherever they are not a type argument, namely as a function parameter, a function result, and a declared data field; a polymorphic value can be carried through a generic container by wrapping it in a data type with a polymorphic field.

5.1 Three Posets

A poset (partially ordered set) is a set equipped with a reflexive, antisymmetric, and transitive order. A lattice is a poset in which every pair has both a least upper bound (a join) and a greatest lower bound (a meet). A Prism signature carries three posets: what a computation may do (the effect row, after !), how its values may be used (the usage row, after @), and how a handler may consume a continuation (the operation grade). Effect rows and operation grades are lattices: effect rows have union and intersection, while grades form a total chain. Coeffect axes are not lattices in general because some conflicting facts have no meet.

Effect rows: joins always exist. The carrier is a set of effect names, the order is inclusion, the join is union:

Sequencing takes the join; handling subtracts back toward the pure bottom:

effect Ask
  once ask() : Int

fn f() : Unit ! {IO} = println("f")

fn g() : Int ! {Ask} = ask()

fn foo() : Int ! {IO, Ask} =
  f()
  g()

fn bar() : Int ! {IO} =
  handle foo() with
    once ask() => 7

fn main() = println(bar())

foo sequences f and g, so its row is their join; bar handles Ask, so its row steps back down to {IO}.

Coeffect axes: meets sometimes missing. Each axis (coeffects) has silence at the top, the mode of all unannotated code. An exclusive axis has no meet below its points; the fip axis is a product of chains, so its meet exists:

Descending is a strengthening someone must prove; ascending, forgetting a claim, is always free; and holding two claims at once is exactly having a point below both:

fn f() : Int @ noalloc = 1  -- a proven claim: f's call tree allocates nothing

fn g() : Int = f()          -- ok: forgetting the claim moves up, always free

-- fn foo() : Int @ noalloc = g()
--   rejected, descent needs proof: in `foo`, call to `g` may
--   allocate (`g` has no zero-allocation certificate)

-- h : ((Int) -> Int) @ {linear, bounded_stack}
--   a legal row shape: the meet exists and the reserved claims compose

-- h : ((Int) -> Int) @ {once, many}
--   never parses: usage facts `once` and `many` contradict each other (same axis)

fn main() = println(g())

Operation grades: a total chain. Continuation use is a quantity, so its lattice is a total order:

The whole discipline is one comparison at one boundary: a clause’s grade at most its operation’s declared grade (effects and handlers):

effect E
  never quit() : Int  -- never: a clause must drop the continuation
  once ask() : Int    -- once:  a clause resumes exactly once, in tail
  coin() : Bool       -- many:  a clause may capture k, resume freely (default)

fn foo() : Int ! {E} =
  let x = ask()
  if coin() then x else quit()

fn run() : Int =
  handle foo() with
    never quit() => 0        -- never <= never  ok
    once ask() => 42         -- once  <= once   ok
    coin() resume k => k(true)     -- once  <= many   ok: below the grade is allowed

-- ask() resume k => k(1) + k(2) would be rejected: the clause for `ask`
-- exceeds its declared grade `once`, resuming more than once

fn main() = println(run())

One signature exercises all three at once:

fn spawn(f : (() -> a ! e) @ {once, portable}) : Fiber(a) ! {Async(a), e}

spawn takes a portable thunk f that it may call at most once, starts it as a fiber producing an a, and may perform both the thunk’s effects e and the asynchronous effect Async(a).

• Row, joined: whatever f performs is unioned into the caller’s row alongside Async; the handler that later runs the fiber subtracts Async back out.
• Axes, met: @ {once, portable} is one point on each of two axes, their meet in the product: spawn promises to call the thunk at most once and may carry it to another fiber.
• Grade, bounded: the Async operations are many, the top of the chain, so a scheduler may hold the continuation and resume it later; once would have pinned every handler to immediate single resumption.

The design is the three properties side by side. Effects always have joins: doing more must always be expressible. Coeffects sometimes lack meets: some promises genuinely contradict. Continuation use is a total order: it is a quantity, not a set.

An effect is a coeffect on its own continuation: operation grades constrain how the handler may use the captured continuation.³

5.2 Types

The scalar types are Int (arbitrary precision), I64, U64, Float, Bool, Char, String, and Unit. A type constructor applied to arguments is written Con(t, ...); the list type has the sugar [t] for List(t). A tuple type is (t, ...). A function type is (t, ...) -> u, optionally carrying an effect row on u. A universally quantified type is forall a. t. Type variables are varids.

5.3 Kinds

A type has kind * (a type of values) or * -> * (a type constructor awaiting one argument), and so on; List has kind * -> *, since List(Int) is a type only once Int is supplied. A class parameter may range over a constructor of kind * -> *, applied as f(a) in method signatures; see type classes. Each constructor’s parameter kinds form an arrow k1 -> ... -> *, and an applied head is checked argument by argument against that arrow: too many arguments, or an argument whose kind does not match the parameter’s, is a kind mismatch reported at the annotation. There is no separate global kind-checking phase; the remaining well-kindedness obligations are discharged during unification, which requires a constructor and its arguments to agree in arity.

Besides * and its arrows there is one further kind, Row, inhabited by effect rows rather than types. A type parameter annotated : Row ranges over rows, so a data type can carry an effect row as a parameter and thereby store an effectful computation in a field: in type Cmd(a, e : Row) a field may name e as ! {e} (or in a tail, ! {IO | e}), the constructor quantifies e with a row-level forall, and the applied head Cmd(a, e) carries the row in that position. A Row-kinded argument is an effect row, written either as a row variable (Cmd(a, e)) or a { .. } row literal (Cmd(Int, {IO})); supplying a type where a row is expected, or a row where a type is expected, is a kind mismatch reported at the annotation. An unannotated parameter still defaults to *, so Row is opt-in and existing types are unchanged. This is the type-system support for storing an effect-polymorphic reified handler, such as the concurrency scheduler of effects and handlers.

The third non-* kind is Nat, inhabited by type-level natural numbers, the dimensions of a shape-indexed type. A type parameter annotated : Nat ranges over dimensions, so in type Vec(a, n : Nat) the length n is a compile-time index rather than a stored field; an argument in that position is either a bare natural literal (Vec(Int, 3)) or a Nat-kinded variable (Vec(a, n)). As with Row, supplying a type where a dimension is expected, or a dimension literal where a type is expected, is a kind mismatch reported at the annotation.

Dimensions unify by equality only: two literals unify when they are equal (3 with 3), a variable unifies with whatever dimension it meets, and a clash is a compile error naming both lengths (zipping a Vec(Int, 3) with a Vec(Int, 4) reports expected length 3, but got length 4). There is deliberately no successor structure and no arithmetic on dimensions: n + m and n + 1 in a dimension position are declined at the parser with a pointed message, and this is a decision, not a gap.

The consequence is stated honestly rather than worked around: an operation whose correctness needs an arithmetic relation between dimensions cannot be given a length-precise type. A length-changing cons of type (a, Vec(a, n)) -> Vec(a, n + 1) is therefore not expressible, and a head over Vec(a, n) cannot statically exclude the empty vector (which would require n to be a successor m + 1); such a head accepts any length and faults, or ranges over Fail, on the empty case. Equality-only dimension unification is exactly the reach that shape indexing needs (fixed-length containers, matching-length zips) without importing a dependent-arithmetic decision procedure into the frozen core.

Dimensions are erased before the Core IR and never reach code generation, so a Nat index is a purely static fact: it constrains what type-checks but is invisible to every backend and to the determinism contract, exactly like a phantom parameter. An unannotated parameter still defaults to *, so Nat is opt-in.

5.4 Inference, Generalization, and Defaulting

A row is built from labels, the effect names of effects and handlers (a parametric effect’s label carries type arguments). It is closed when it ends in a fixed set of labels and open when it ends in a row variable (! {L | r}), which stands for further labels the caller may add. An unannotated binding is generalized over its free type and row variables not fixed by the surrounding scope. A bare type variable written in a top-level function’s signature is an implicit forall: it is universally quantified and rigid, so the body is checked to hold for every instantiation and may neither narrow it to a concrete type nor equate two distinct signature variables (a body that does is a type error), and the declaration exports exactly the polymorphic scheme it wrote. Two cases default rather than generalize, both resolved in one pass at generalization. A numeric operand of an arithmetic or comparison operator left otherwise unconstrained defaults to Int; because the default is deferred to that pass rather than applied at the operator, a later use that fixes the operand to a fixed-width lane (I64/U64) takes precedence, so x + y followed by an i64 use of x is fixed-width, not Int. An open row left unconstrained at a monomorphic declaration (one with no remaining free row variable) defaults to empty (pure); an effect-polymorphic declaration keeps its row variable, as traverse does in the prelude (the standard prelude).

5.5 Subsumption and Row Equivalence

Checking a value against an expected type uses subsumption, not equality. A more polymorphic type is accepted where a less polymorphic one is expected: a forall on the expected side introduces a rigid variable the value must satisfy for all instances, and a forall on the value side is instantiated to meet the expectation. Function subtyping is contravariant in the arguments and covariant in the result, so a function accepting more and returning less may stand in for one accepting less and returning more.

Effect rows are checked by unification over scoped labels, not by covariant widening. Two rows are compared up to reordering: ! {A, B} and ! {B, A} are the same row, because unification hoists a demanded label to the head of the other row before matching the tails. An open row ! {A | r} unifies with any row that provides A by binding r to the remainder; for instance ! {A | r} unifies with ! {A, B} by binding r to {B}. This is how a caller’s row absorbs a callee’s. A unification that would make a row contain itself is rejected, so recursive effect rows do not arise.

At a function arrow the value’s effect row is made equal to the expected one by this same unification, so a narrower row fits a wider context only by solving a row variable, never by silent widening. A pure function still fits an effectful context, because its own latent row is a quantified variable (effect polymorphism) that unification solves to the demanded effects. Where a function carries an explicit return row, that annotation is the row its body is unified against: a body that performs an effect the annotation omits does not unify and is rejected with a diagnostic naming the effect the annotation must declare, and the annotation’s row variables are rigid, so an annotation may not silently narrow to fewer effects than the body performs.

5.6 Fixed-Width Integers

Int is arbitrary precision. I64 and U64 are the signed two’s-complement and unsigned 64-bit lanes; they wrap on overflow rather than promoting to a bignum. Their arithmetic and comparisons are the plain operators through the numerical tower, one spelling across every lane. The bit-level operations have no operator spelling and remain named builtins, each taking two operands of the lane type.

and, or, and xor share a single bit pattern across both lanes; i64_shr is an arithmetic (sign-extending) shift while u64_shr is logical; a shift count is taken modulo 64. to_i64/to_u64 and int_of_i64/int_of_u64 convert between Int and the fixed-width lanes.

5.7 Integer Arithmetic and Division

The arithmetic operators +, -, *, /, and % spell integer arithmetic here through the numerical tower’s Int, I64, and U64 instances; ^ is exponentiation. On Int they are arbitrary precision: a sum, product, or difference is exact and never overflows, promoting a machine-word result to a bignum on demand.⁴ This section states the two facts that arithmetic on Int cannot state by its type alone: how division rounds, and what division by zero does. Both are identical on the interpreter and native backends, a corollary of the determinism contract and pinned by the parity corpus.

Division truncates toward zero and remainder takes the sign of the dividend. That is, / discards the fractional part by rounding toward zero rather than toward negative infinity, and a % b has the sign of a (or is zero), so the identity a == (a / b) * b + (a % b) holds for every non-zero b.⁵ This is truncated division, the semantics of C99, Rust, and the hardware division instruction both backends emit.

-- Integer `/` truncates toward zero; `%` takes the dividend's sign.
-- `Int` is arbitrary precision, so the same laws hold past the machine word.
-- `^` binds tighter than unary minus, and a negative exponent is
-- `1 / base ^ (-exp)` under the same truncating division.
fn main() =
  println(7 / 2)
  println((0 - 7) / 2)
  println(7 / (0 - 2))
  println((0 - 7) / (0 - 2))
  println(7 % 3)
  println((0 - 7) % 3)
  println(7 % (0 - 3))
  println((0 - 7) % (0 - 3))
  println(1000000000000000000000 / 7)
  println((0 - 1000000000000000000000) % 7)
  println(-2 ^ 2)
  println((-2) ^ 2)
  println(2 ^ -1)
  println(1 ^ -5)
  println((-1) ^ -5)

Floored division, where / rounds toward negative infinity and % (the Euclidean-adjacent modulus) takes the sign of the divisor, was considered and declined. Two reasons decide it. The fixed-width lanes are the constraint: / and % on I64 and U64 are the machine’s truncating division, and an Int operator whose meaning diverged from the lane it shares a spelling with would split the integer family into two rounding rules a reader must track by type. And the determinism contract wants one rule across every lane and both backends rather than a surface convenience that the hardware does not compute; a caller who wants a floored or Euclidean modulus writes it once over these primitives (((a % b) + b) % b for a non-negative residue) rather than having the language pick a second, silently different %.

Division or remainder by zero is the one partial case of integer arithmetic. It is a runtime fault: the program halts immediately with exit status 1 and exactly fatal: division by zero on standard error, byte-identical on the interpreter and the native backend, on both Int and the fixed-width lanes. It is not a value, and unlike the recoverable fail() of errors and failure it is not routed through an effect and cannot be caught; it aborts the run the way an unrecoverable error(code) does. Every other integer operation is total.

The fixed-width lanes wrap rather than fault or promote (fixed-width integers): +, -, and * on I64 and U64 are two’s-complement modular arithmetic, so adding one to I64_MAX wraps to I64_MIN and adding one to U64_MAX yields 0.⁶ Unary minus follows the same wrap on the fixed-width lane, so -x on I64 is the two’s-complement negation and -I64_MIN is I64_MIN. Int, being a bignum, has no such edge: negation and division there are always exact.⁷

-- Fixed-width I64/U64 arithmetic wraps two's-complement: no promotion to a
-- bignum, and no fault on the signed-minimum edge (`I64_MIN / -1` wraps).
fn main() =
  let maxi = 9223372036854775807i64
  let mini = 0i64 - maxi
  let mn = mini - 1i64
  let neg1 = 0i64 - 1i64
  println(show(maxi + 1i64))
  println(show(maxi * 2i64))
  println(show(mn / neg1))
  println(show(mn % neg1))
  println(show(18446744073709551615u64 + 1u64))
  println(show((0i64 - 7i64) % 3i64))

5.7.1 Safe Arithmetic Families

The wrapping and faulting defaults above are the primitives; a program that wants overflow to be visible rather than silent reaches for the safe families in the Data.Checked library, which layer four disciplines over those primitives through one class, Checked(a).

Instances cover I64, U64, and Int; the checked narrowings int_to_i64 and int_to_u64 sit beside the class as free functions returning Option, the partial inverses of the total widenings int_of_i64/int_of_u64.

Checked sits beside the arithmetic classes rather than inheriting from them: it carries no superclass and no raw operators, so it stays meaningful for any integer lane independently of what algebraic structure that lane also has. The connection runs the other way, as a law. The wrapping_* methods agree exactly, value for value, with the lane’s raw arithmetic, wrapping_add/wrapping_sub/wrapping_mul with the two’s-complement +/-/* and wrapping_neg with unary negation.⁸ Because the agreement is with the raw operators, it is stable under any later refactor that gives those operators a class of their own: the wrapping_* methods and the lane’s ring operations remain the same function by construction.

The families are not independent definitions that happen to line up; each fixed-width operation is computed once in the exact Int lane and then narrowed three ways, so the laws hold by construction and are pinned on both backends. For a lane bounded by [lo, hi], checked_op(x, y) is Some(wrapping_op(x, y)) when the exact result lies in range and None otherwise; overflowing_op(x, y) is (wrapping_op(x, y), flag) with flag true iff checked_op(x, y) is None; and saturating_op(x, y) is that same wrapped value when it is in range, and otherwise the crossed bound, hi on overflow above (I64 max or U64 max) and lo below (I64 min or 0).⁹ Division and remainder inside a checked_* follow the truncating rule of integer arithmetic. The Int instance is the degenerate case that keeps the class total rather than vacuous: unbounded, so wrapping_* and saturating_* are the identity, overflowing_* always flags false, and only a zero divisor turns a checked_* into None.

-- The safe-arithmetic families of `Data.Checked` over the lane boundaries. The
-- raw wrap/truncate/fault semantics they build on are pinned by fixed-width
-- integers and integer arithmetic; here every printed line is a law that must
-- hold identically on both backends. `checked` is `None` exactly on overflow or
-- a zero divisor, `saturating` clamps to the crossed bound, `wrapping` matches
-- the raw operator, and `overflowing` pairs the wrapped result with that flag.
import Data.Checked (..)

fn main() =
  let i_max = to_i64(2 ^ 63 - 1)
  let i_min = to_i64(0 - 2 ^ 63)
  let u_max = to_u64(2 ^ 64 - 1)
  let one = to_i64(1)
  -- I64: the three families agree with each other at the upper edge.
  println(show(checked_add(i_max, one) == None))
  println(show(saturating_add(i_max, one) == i_max))
  println(show(snd(overflowing_add(i_max, one))))
  println(show(fst(overflowing_add(i_max, one)) == i_min))
  println(show(checked_add(i_max, to_i64(0)) == Some(i_max)))
  -- I64: lower edge, negation, and the two division edges.
  println(show(saturating_sub(i_min, one) == i_min))
  println(show(checked_neg(i_min) == None))
  println(show(wrapping_neg(i_min) == i_min))
  println(show(checked_div(i_min, 0i64 - one) == None))
  println(show(checked_div(to_i64(7), to_i64(2)) == Some(to_i64(3))))
  println(show(checked_mod(to_i64(0 - 7), to_i64(2)) == Some(to_i64(0 - 1))))
  -- U64: unsigned underflow clamps to zero and wraps to the max.
  println(show(checked_sub(to_u64(0), to_u64(1)) == None))
  println(show(saturating_sub(to_u64(0), to_u64(1)) == to_u64(0)))
  println(show(fst(overflowing_sub(to_u64(0), to_u64(1))) == u_max))
  println(show(checked_add(u_max, to_u64(1)) == None))
  println(show(checked_neg(to_u64(0)) == Some(to_u64(0))))
  -- Int: unbounded, so checked is total except division, overflow never fires.
  println(show(checked_add(2 ^ 100, 2 ^ 100) == Some(2 ^ 100 + 2 ^ 100)))
  println(show(saturating_mul(2 ^ 100, 2) == 2 ^ 100 * 2))
  println(show(not(snd(overflowing_add(2 ^ 100, 1)))))
  println(show(checked_div(5, 0) == None))
  -- Checked Int narrowing agrees with the lane bounds.
  println(show(int_to_i64(2 ^ 100) == None))
  println(show(int_to_u64(0 - 1) == None))
  println(show(int_to_i64(42) == Some(to_i64(42))))

5.8 Floating-Point Arithmetic

Float is an IEEE-754 double. Its arithmetic and comparison operators are the plain +, -, *, /, %, ==, /=, <, <=, >, and >= through the numerical tower. There is no implicit coercion between Int and Float, so a mixed expression is a type error resolved by an explicit to_float (exponentiation). Floating-point arithmetic is where a language most often becomes tier-dependent, because a fused multiply-add, an extended-precision register, or a differently rounded library call changes a low bit. Prism forbids that: every float operation follows one rounding rule and one set of special-value rules, and the interpreter and both native backends agree bit for bit, pinned by the parity corpus and, for the printer, by a dedicated formatter oracle.

The rounding contract is round to nearest, ties to even, the IEEE-754 default, applied to every arithmetic operation with no fused or wider-than-double intermediate. This is the single rule the language commits to, and it is why 0.1 + 0.2 is 0.30000000000000004 and 1.0 / 3.0 is 0.3333333333333333 identically everywhere: the result is the correctly rounded double, not an artifact of an evaluation order or a backend.

Float division never faults. Where integer / by zero aborts, /. by zero is an ordinary IEEE result: x / 0.0 is inf or -inf according to the sign of the numerator and of the zero, and 0.0 / 0.0 is nan. A nan then propagates through every arithmetic operation it touches, so nan + 1.0 and nan * 0.0 are both nan; there is no arithmetic that turns a nan back into a finite number.¹⁰ Because no float operation faults, a floating-point pipeline never introduces a failure edge into a function’s effect row the way integer division by zero conceptually could.

Signed zero is observable. 0.0 and -0.0 are distinct values that compare equal (0.0 == -0.0 is true) yet are distinguished by any operation that reads the sign bit: 1.0 / 0.0 is inf while dividing by negative zero is -inf.¹¹ Comparisons follow IEEE unordered semantics for nan: nan is equal to nothing including itself, so nan == nan is false and nan /= nan is true, and every ordering against nan (nan < x, nan > x) is false. The program below exercises each of these on both backends.

-- IEEE 754 float arithmetic: division yields inf/-inf/nan with no fault, NaN
-- propagates, signed zero is preserved, and comparisons follow the standard.
fn main() =
  let one = 1.0
  let z = 0.0
  let negz = (0.0 - 1.0) * 0.0
  let inf = one / z
  let ninf = (0.0 - 1.0) / z
  let nan = z / z
  println(0.1 + 0.2)
  println(1.0 / 3.0)
  println(inf)
  println(ninf)
  println(nan)
  println(negz)
  println(one / negz)
  println(nan + one)
  println(nan * z)
  println(if nan == nan then "nan==nan is true" else "nan==nan is false")
  println(if nan /= nan then "nan/=nan is true" else "nan/=nan is false")
  println(if z == negz then "0.0==-0.0 is true" else "0.0==-0.0 is false")
  println(if nan < one then "nan<1 is true" else "nan<1 is false")

Printing is owned by the canonical Float formatter and not respecified here; this section fixes only the tokens the special values render as, since a claim about nan or -0.0 is a claim about output. show (and therefore print and string interpolation, type classes) renders a nan as nan, positive and negative infinity as inf and -inf, and negative zero as -0, distinct from 0 for positive zero; the shortest round-tripping form the formatter chooses for finite values is the formatter’s contract, not this chapter’s.

5.8.1 Elementary Functions and Conversions

The elementary functions are owned the same way the arithmetic is. Rather than call whatever libm the platform links, Prism vendors one implementation of the double-precision math library and routes every function through it on every backend: the native code calls it, and the interpreter calls the identical compiled symbols, so a transcendental is a consequence of in-repo code, not of a system library’s rounding.¹²

The accuracy statement is deliberately modest and honest: the contract is determinism, not correct rounding. Each function is a deterministic faithful approximation, bit-for-bit identical on the interpreter and both native backends and across platforms, but it is not guaranteed to be the correctly rounded double of the true real result. Correctly-rounded transcendentals (the table-maker’s-dilemma problem) are an explicit non-goal; what the language guarantees is that whatever value a function produces, it produces the same value everywhere, pinned by the conformance corpus over the hard cases (subnormals, the extremes, argument reduction near multiples of pi/2, signed zero, nan, and the infinities) and a deterministic bulk sweep.

The functions divide into two classes. The exact operations are correctly rounded or integer-valued by IEEE-754 and therefore identical on every conforming platform regardless of implementation: sqrt (correctly rounded), abs_float, and the roundings floor, ceil, trunc (toward zero), and round (ties away from zero, so round(2.5) is 3.0 and round(-2.5) is -3.0, distinct from the ties-to-even of arithmetic). The approximate transcendentals are the owned-library functions: sin, cos, tan; the inverses asin, acos, atan, and the two-argument atan2(y, x); the hyperbolics sinh, cosh, tanh; the exponentials exp, exp2, expm1; the logarithms ln (natural), log2, log10, log1p; pow, cbrt, and hypot. fmod(x, y) is the exact IEEE remainder.¹³

The Int/Float conversions pin their rounding once, identically on both backends. to_float rounds an Int to the nearest Float, ties to even. The three float-to-Int conversions differ only in how they round to an integer before converting: truncate toward zero, floor_to_int down, ceil_to_int up.¹⁴

5.8.2 The Numerical Tower

The arithmetic and comparison operators are one spelling per operation across every lane, with the lane chosen by the operand’s type and resolved entirely at compile time. Three classes carry them. Num(a) provides +, -, *, and unary minus; Div(a) provides / and %; Ord(a) provides <, <=, >, and >= through its cmp method for non-primitive ordered types. Num and Div have instances for Int, I64, U64, and Float, so + reads on any of them and the earlier per-lane semantics of this chapter (the exact Int, the wrapping fixed-width lanes, the IEEE Float) are the instances’ behavior, unchanged. Div is split from Num so a type with addition but no sensible division stays representable without a vacuous method.

Resolution has no runtime cost.¹⁵ A monomorphic operand keeps the lane’s direct primitive, exactly the code the operator emitted before the tower, so the class dictionary never survives specialization and the generated core is byte-identical, pinned by the allocation gate. Only genuinely polymorphic code, a function written given Num(a) or given Div(a), dispatches through a dictionary, and that dictionary too is erased wherever the function is specialized to a concrete lane. Unary minus follows the same rule: -x on a concrete lane is the sign flip or two’s-complement negation of floating-point and integer arithmetic, and -x on a Num(a) operand dispatches through the class with the same value. Unsigned U64 has no surface negation (-x on a U64 is a type error naming the signed lanes), but the Num(U64) instance’s negation is the two’s-complement wrap, reachable through generic Num code and agreeing with wrapping_neg (safe arithmetic).

Integer literals are polymorphic. A literal with no width suffix adopts whatever numeric lane its context expects: 1 is a Float where a Float is wanted (so a Float-typed binding or argument needs no .0), an I64 in an I64 position, and so on, with the lane’s constant placed directly in the elaborated core and no runtime conversion. A decimal or exponent literal denotes a fractional lane, of which Float is currently the only one. The defaulting rule fixes the ambiguous case: an integer literal with no constraining context defaults to Int, and a fractional literal to Float. The default always fires, so a program that never mentions the numeric classes never sees a class-constraint error; let n = 5 is an Int exactly as before the tower. A width-suffixed literal (5i64, 5u64) is monomorphic, its suffix a type ascription rather than a hint, and a literal out of range for the lane it resolves to is a compile error at resolution time.

There is no implicit coercion, ever. The lane a value carries is fixed by its type, and only literals adapt; a variable never does. x + 2.5 where x : Int is a type error naming both lanes, not a promotion of x to Float, and the same holds across any two distinct lanes (I64 and U64, Int and Float). Cross-lane movement is always an explicit, named conversion (to_float, the checked narrowings and exact widenings of fixed-width integers and safe arithmetic). This is the line between a numeric surface that stays predictable and one whose every operator hides a possible conversion.

5.9 Algebraic Data Types

A type declaration introduces an algebraic data type: a sum of constructors, each a product of fields. A constructor is named with an upper-case identifier and applied like a function to build a value; a match (patterns) destructures a value by constructor. A type may take type parameters and may be recursive, including mutually so. A type parameter may be annotated : Row to range over an effect row rather than a type (kinds), so a field can store an effectful computation, as in type Cmd(a, e : Row) whose field is a () -> a ! {e}, or : Nat to range over a compile-time dimension, as in type Vec(a, n : Nat) whose length index is erased rather than stored.

-- A sum type: a value is exactly one of the listed constructors, each with its
-- own fields. Construction names a constructor; destruction matches on it.
type Shape = Circle(Int) | Rect(Int, Int)

fn area(s) =
  match s of
    Circle(r) => 3 * r * r
    Rect(w, h) => w * h

-- A recursive sum type, the canonical binary tree.
type Tree = Leaf | Node(Tree, Int, Tree)

fn sum_tree(t) =
  match t of
    Leaf => 0
    Node(l, v, r) => sum_tree(l) + v + sum_tree(r)

fn main() =
  println(area(Circle(10)))
  println(area(Rect(3, 4)))
  println(sum_tree(Node(Node(Leaf, 1, Leaf), 2, Node(Leaf, 3, Leaf))))

A newtype is a data type with exactly one single-field constructor: a type distinct from its payload, with no runtime wrapper. An alias on a type expression is a transparent synonym, interchangeable with its definition. An alias whose body is a row literal is a row alias, the same transparency for a set of effect labels: usable wherever a row is written, expanded before checking, and composable with other aliases (composing rows); a row alias takes no parameters.

A deriving (C, ...) clause generates the named instances structurally (type classes). Eq, Ord, Show, Hash, Lens, and Plate are derivable everywhere: derived Ord compares fields lexicographically in declaration order and orders constructors by declaration, and derived Hash folds the value through the same blake3 Merkle construction that content-addresses code (content-addressed core), so structurally equal values carry one canonical digest on every backend.

Derived Plate yields one layer of structure, taken apart and put back. children(x) is the list of x’s immediate subvalues of x’s own type, in constructor-declaration and field order, and nothing else; rebuild(x, ks) is x with exactly those positions replaced, left to right, by the elements of ks. A whole-tree traversal or rewrite (every subterm, a fold, a count, a bottom-up rewrite) is written once against that one pair rather than once per constructor, and a fifty-constructor syntax tree costs the same to walk as a two-constructor one. The derivation looks through list, optional, tuple, and record fields, and through the other data types declared in the program, to find the occurrences a field can lead to; that is what lets a traversal see through the carrier records a tree holds its nodes in (a match arm, a spanned wrapper, a qualifier) with no second match written for them.

The two methods are inverse on one layer, and that law is what every combinator above them relies on: rebuild(x, children(x)) is x, and the list handed to rebuild must have the same length and order as the one children returned. children is pure and total, returning structurally smaller values, so a recursion driven by it terminates on a finite value. rebuild carries Fail in its row for exactly one reason: a list of any other length is a programming error, not an input to be repaired, so it raises Fail rather than padding the missing positions or dropping the extra ones, either of which would silently hand back a value that is not the one asked for. On a correctly shaped list it performs no effect. Both methods come from one walk of the declaration, read forwards and backwards, so a derived pair satisfies the law by construction; a hand-written instance owes it.

Being structural rather than compositional, this derivation differs from the others in two visible ways. It puts no constraint on the type’s own parameters, because a Plate(T(a)) yields T occurrences and never an a; and it asks nothing of a component’s own instances, taking the component apart by its declaration rather than by dispatch, so a component with no Plate instance is traversed all the same. What it cannot take apart it refuses: a field that could still lead back to the derived type through something opaque (a function, a container with no declaration in the program) is an error at the deriving clause naming the field and the type it reached, never a silently dropped subterm. Nothing in the class is unforgeable, so a hand-written instance is an ordinary instance and is accepted, which is the escape hatch for an abstract type whose children the compiler cannot see.

Five more classes derive against opt-in modules: Serialize and Stable (import Wire) for the wire codec, where Stable derives only when every component is itself Stable and a non-stable field is a compile error at the derive site; Arbitrary (import Test) for property-test generators built from the type’s structure (stable blocks); and ToJson with FromJson (import Json) for conversion to and from the dynamic JSON tree.

The JSON pair is for a type whose schema is its own declaration, and is derived as a pair, since a type that encodes but cannot decode is a document nobody can read back. One constructor becomes one object: a record constructor’s keys are its declared field names, a positional one’s are its argument positions (_0, _1), and a sum additionally names the variant it holds under the key $, which no field name can spell, so a document names its constructor rather than an index that quietly changes meaning when a constructor is inserted. A single-constructor type has nothing to discriminate and carries no tag. Constructor and field order are the declaration’s, so a value has one tree, and the encoder sorts keys, so it has one string on every backend. Unlike Plate this derivation is compositional: each field is converted through its own instance, so a component with no instance is a compile error at the field. A decode that does not fit, a tree that is not an object, a $ naming no constructor of the type, a missing key, or a field that will not itself decode, is one ordinary Fail, caught with optional or default; that failure carries no payload, so it reports that the document did not fit and not where, because Fail is nullary and a positioned failure would mean a different effect on the class signature and so on every hand-written instance too. None of this is the wire codec: a Serialize byte format is frozen and versioned by Stable, while a JSON document is read by something not compiled against this program, so the encoding is self-describing rather than compact and promises nothing across a change to the declaration.

deriving (Identifiable) is shorthand for the identity starter pack, expanding to exactly Eq, Ord, Hash, and Show so an ID newtype is comparable, hashable, and printable from one keyword with no imports; a class listed alongside it is derived once, not twice, and Arbitrary is deliberately excluded (it lives behind import Test and is a testing concern), so a value that also wants a generator writes deriving (Identifiable, Arbitrary).

5.10 Records

A constructor may instead take named fields, C { f : T, ... }, making the type a record. A field is read with e.f; records are built and updated by the record expressions. deriving (Lens) synthesizes a getter f_of and a setter with_f per field.

-- A record is a single-constructor product type with named fields. Fields are
-- read with `.f`, built with `C { f = e, ... }`, and updated functionally.
type Point = Point { x: Int, y: Int }

fn main() =
  let p = Point { x = 3, y = 4 }
  let q = Point { ..p, y = 9 }
  println(p.x)
  println(q.y)

5.11 Unboxed Products

A product may be written unboxed so its fields are carried inline rather than behind a heap cell: #(a, b) is an unboxed tuple and #{ x : a, y : b } an unboxed record, whose field is read with e.#field. A record lowers positionally to the same product representation, so projection reuses the tuple machinery and reference counting is balanced by construction. A product built and consumed within one function scalarizes away entirely, creating no cell at all; one that escapes across a boundary the optimizer cannot see through is boxed by the native backend, value-identical to the interpreter. Whether a given product is boxed is therefore a cost fact decided by the backend, never a difference an observer can name.

fn norm2() : Float =
  let v = #{ re = 1.0, im = 2.0 }
  v.#re * v.#re + v.#im * v.#im

fn main() = println(norm2())

5.12 Non-Allocating Nullables

OrNull(a) is a nullable that costs no heap cell: Null is the empty word and This(v) carries a present element in the element’s own representation. Because the two share one word of storage, the element type must be one whose values can never collide with the null word: a concrete, single-word, non-zero type. Unit (the zero word), a nested OrNull, an unboxed product, and an element type inference never pins are all rejected at compile time (E1019), on written annotations and on nullables inference discovers on its own alike. Null and This behave as ordinary constructors under match, exhaustiveness, and reference counting, so a nullable is byte-identical across backends and its representation stays a storage choice.

fn find(hit : Bool) : OrNull(String) =
  match hit of
    true => This("found")
    false => Null

fn main() =
  match find(true) of
    Null => println("none")
    This(s) => println(s)

6. Type Classes

A class declares a single-parameter constraint and a set of method signatures. An instance is a named value providing those methods for one head type. A function states its constraints with a given clause after the return annotation, as announce below does, and receives its dictionaries as hidden arguments resolved at each call site, one per constraint. The following program declares two Describe(Temp) instances, designates one canonical, and selects the other explicitly with using.

A class, instance, or effect body is a layout block: the head ends its line and the members follow on indented lines, one per line, with no braces and no where. Each instance method is written in expression form, fn m(x) = e. Because the body is layout-delimited, it admits the same layout-sequenced statements as a top-level fn body, as well as let .. in chains. A brace opening one of these bodies is a parse error that names the layout rewrite. A marker class with no methods, and its instance, are written as the bare head with no body.

-- Typeclasses. A class is an interface: a named bundle of methods a type
-- implements. An instance provides those methods for one type, and a function
-- that says `given Shape(a)` works for every type with an instance, receiving
-- the instance as a hidden argument resolved at each call site.

type Circle = MkCircle(Float)

type Rect = MkRect(Float, Float)

class Shape(a)
  area : (a) -> Float
  name : (a) -> String

instance shapeCircle : Shape(Circle)
  fn area(c) =
    match c of
      MkCircle(r) => 3.14159265 * r * r
  fn name(_c) = "circle"

instance shapeRect : Shape(Rect)
  fn area(s) =
    match s of
      MkRect(w, h) => w * h
  fn name(_s) = "rectangle"

fn summary(x : a) : String given Shape(a) =
  concat(name(x), concat(" of area ", show_float(area(x))))

-- Instances are named values (Lean-style), which is what the knobs below hang
-- off. A second instance for the same head type is legal; designating one
-- canonical keeps implicit resolution deterministic (coherence: a program's
-- meaning never depends on a silent tie-break), and the other instance is
-- selected explicitly with `f(args, using instName)`.

instance shapeBox : Shape(Rect)
  fn area(s) =
    match s of
      MkRect(w, h) => w * h
  fn name(_s) = "box"

canonical Shape(Rect) = shapeRect

fn main() =
  println(summary(MkCircle(1.0)))
  println(summary(MkRect(2.0, 3.0)))
  println(summary(MkRect(2.0, 3.0), using shapeBox))

6.1 Coherence and Resolution

An instance is selected by the head constructor of the constraint type (the outermost constructor, for example List in List(Int)). Resolution is coherent: a program’s meaning never silently depends on which instance the resolver happened to pick. For each (class, type-head) there is exactly one canonical instance, and implicit resolution always selects it, so resolution is deterministic.

With a single instance for a head, that instance is canonical automatically. When two or more instances share a head, one must be designated canonical with a top-level declaration:

canonical Class(Head) = instanceName

Having two instances for one head without a designation is a coherence error reported at definition, not a silent ambiguity deferred to the use site. The designated instance is what implicit resolution selects; the others remain reachable only through an explicit override.

An explicit override is visible at the use site and changes nothing else’s resolution: pass the chosen instance as a trailing using argument, f(args, using instanceName), as sort_by_ord(xs, using ordDesc) does above. (This is the same using form reserved for first-class dictionary passing.) There is no ambient, scoped instance mechanism: an override is always written where it is used.

The preferred way to obtain a different instance for a type is a newtype with its own canonical instance (newtype Down = Down(Int) for reverse order, a folded-case wrapper for case-insensitive comparison) rather than a non-canonical instance of the base type. This changes the type, not the instance-for-a-type, so coherence is preserved exactly and the difference is visible in the signature; an explicit using override is the second-line tool when a newtype is too heavy.

Resolution recurses through instance contexts up to a fixed depth.

A consequence worth naming: equality, ordering, and hashing are ordinary methods of coherent classes (Eq, Ord, Hash), never built-ins that work on any value by inspecting its representation. Prism has no polymorphic structural ==, compare, or hash. A structural default is a known hazard: it typechecks on functions, abstract types, and cyclic values where it has no principled meaning, and it silently overrides whatever notion of equality an abstraction intended. OCaml’s Base goes so far as to shadow the polymorphic versions to keep them out of reach; in Prism the hazard never arises, because the only equality in scope is the one an Eq instance supplies and coherence makes that instance unique.

Printing follows the same discipline. print and println display a concrete argument by its structure (a top-level string prints raw, exactly as interpolation splices it), but a polymorphic argument requires Show: a generic function that prints declares given Show(a), the display dispatches through the instance (a generic Bool prints true, never a representation tag), and printing a rigid type variable without the constraint is a type error naming the missing given Show(a). What is never consulted is the runtime representation; the tag check that guards the raw printer is defense in depth against compiler bugs, not a semantics.

6.2 Superclasses

A class may require another as a superclass with given, the way an interface extends another. Each instance then stores a resolved superclass dictionary as the leading field of its dictionary cell, so one written constraint carries both capabilities: below, a given Greet(a) function calls the superclass method name_of with no Nameable constraint written, discharging it by projecting that field. The superclass witness is found automatically from the instances in scope, so the instance declaration never repeats it, and unlike inheritance nothing is overridden: the two dictionaries stay separate values.

-- Superclasses. A class may require another with `given`: every `Greet` type
-- must already be `Nameable`, the way an interface extends another. Each
-- instance then carries its superclass dictionary as a hidden leading field of
-- its own, so a `given Greet(a)` function may call `name_of` (a `Nameable`
-- method) with no `Nameable` constraint written: `Greet` entails it. Unlike
-- inheritance, nothing is overridden or re-implemented; the `Greet` instance
-- simply points at whichever `Nameable` witness is in scope, and the two kinds
-- of evidence stay separate values.

type Robot = MkRobot(Int)

class Nameable(a)
  name_of : (a) -> String

class Greet(a) given Nameable(a)
  greeting : (a) -> String

instance nameRobot : Nameable(Robot)
  fn name_of(r) =
    match r of
      MkRobot(n) => concat("unit-", show_int(n))

instance greetRobot : Greet(Robot)
  fn greeting(_r) = "beep boop"

-- One constraint, two capabilities: `greeting` is Greet's own method, and
-- `name_of` is projected from the superclass field of the same dictionary.
fn hail(x : a) : String given Greet(a) =
  concat(name_of(x), concat(" says ", greeting(x)))

fn main() = println(hail(MkRobot(7)))

6.3 Higher-Kinded Classes

A class parameter may be a type constructor of kind * -> *, applied as f(a) in method signatures and resolved on the head constructor of each instance. The prelude’s Functor/Applicative/Monad/Foldable/Traversable tower is built this way. The example below builds that tower explicitly over a custom container, each level naming its predecessor as a superclass with given, so an instance high in the tower can exist only where the ones below it do.

-- The Functor/Applicative/Monad tower built explicitly, the same shape the
-- prelude ships for List and Option. The class parameter `f` has kind * -> *,
-- applied as `f(a)` in each method signature, and every level names its
-- predecessor as a superclass with `given`, so an instance high in the tower
-- can exist only where the ones below it do. (The names carry a `B`/`_` suffix
-- only to sit beside the prelude's own Functor/Applicative/Monad and fmap/pure/bind.)

type Box(a) = Box(a)

fn open(b : Box(a)) : a =
  match b of
    Box(x) => x

class FunctorB(f)
  fmap_ : ((a) -> b ! {| e}, f(a)) -> f(b) ! {| e}

class ApplicativeB(f) given FunctorB(f)
  pure_ : (a) -> f(a)

class MonadB(f) given ApplicativeB(f)
  bind_ : (f(a), (a) -> f(b) ! {| e}) -> f(b) ! {| e}

instance functorBox : FunctorB(Box)
  fn fmap_(g, b) = Box(g(open(b)))

instance applicativeBox : ApplicativeB(Box)
  fn pure_(x) = Box(x)

instance monadBox : MonadB(Box)
  fn bind_(b, g) = g(open(b))

fn main() : Unit ! {IO} =
  println(open(pure_(7)))  -- Applicative: lift a value in
  let c = fmap_(\(x) -> x + 1, Box(20))  -- Functor: map under the structure
  let d = bind_(c, \(x) -> Box(x * 2))  -- Monad: sequence (needs the two below)
  println(open(d))

The prelude provides the same tower for List and Option. Its methods are effect-polymorphic (defined under effect polymorphism): a per-element effect row threads through in place of an Applicative wrapper, so effectful traversal needs no monad and no do-notation. Using it, one fmap/ap/bind/traverse works across either container.

-- Higher-kinded type classes: the class parameter ranges over a type
-- constructor (kind * -> *), applied as `f(a)` in the method signatures. The
-- Functor/Applicative/Monad/Foldable/Traversable tower is in the prelude with
-- instances for List and Option, resolved by the head constructor of each
-- instance. `fmap`/`traverse` are effect-polymorphic: the per-element effect
-- row threads through instead of an Applicative wrapper, so effectful
-- traversal needs no monad and no do-notation.
--
-- Prints:
--   [2, 3, 4]
--   Some(42)
--   10
--   [2, 3, 10, 20]
--   Some(15)
--   [1, 1, 2, 2, 3, 3]
--   Some(9)
--   [10, 20, 30]

-- Functor: one `fmap` maps over either container.
fn functor_demo() =
  println(show(fmap(\(x) -> x + 1, [1, 2, 3])))
  println(show(fmap(\(x) -> x * 2, Some(21))))

-- Foldable: an effect-polymorphic right fold.
fn foldable_demo() =
  println(show(fold_r(\(x, acc) -> x + acc, 0, [1, 2, 3, 4])))

-- Applicative: `ap` is cartesian on List, positional on Option.
fn applicative_demo() =
  println(show(ap([\(x) -> x + 1, \(x) -> x * 10], [1, 2])))
  println(show(ap(Some(\(x) -> x + 5), Some(10))))

-- Monad: structural `bind`, where List is nondeterminism and Option failure.
fn monad_demo() =
  println(show(bind([1, 2, 3], \(x) -> [x, x])))
  println(show(bind(Some(3), \(x) -> Some(x * x))))

-- Traversable: effectful map, with an empty effect row here.
fn traversable_demo() = println(show(traverse(\(x) -> x * 10, [1, 2, 3])))

fn main() =
  functor_demo()
  foldable_demo()
  applicative_demo()
  monad_demo()
  traversable_demo()

So Monad here is just another class, structure for List-style nondeterminism and Option-style failure, with none of the language integration it carries elsewhere: no do-notation, no privileged status, no return, no burritos,¹⁶ no Kleisli categories.¹⁷ Sequencing side effects is the effect system’s job, not the monad’s.

The two systems meet in Traversable. The example below defines a recursive Tree, gives it the Functor/Foldable/Traversable instances, then runs a single generic traverse over it four ways. Nothing about the traversal changes between them; the behaviour is chosen entirely by the effect the per-element function performs, since traverse’s signature carries that row straight through. State numbers the leaves, Fail short-circuits, Choice (resumed multishot) enumerates every assignment, and {State, Fail} does the first two at once under two stacked handlers. Each is a job a monadic language hands to a different Applicative instance (State, Maybe, the list monad) or, for the last, a StateT s Maybe transformer stack; here it is one traversal and the effect rows supply the rest. This is the whole type system in one program: higher-kinded classes with a superclass chain, principal effect rows that compose, and handlers (including multishot resumption) discharging them.

-- The synthesis: one generic, effect-polymorphic `traverse` over a custom
-- recursive `Tree`, run four ways. Nothing about the traversal changes between
-- them; the behaviour is chosen entirely by the effect the per-element function
-- performs, and the effect system supplies what a monadic language would reach
-- for an Applicative instance (or a transformer stack) to get. The signature
-- `traverse : ((a) -> b ! {| e}, t(a)) -> t(b) ! {| e}` carries the per-element
-- row `e` straight through, so each leaf's effects sequence in tree order and a
-- handler discharges them at the boundary. No Applicative, no do-notation.

type Tree(a) = Leaf(a) | Branch(Tree(a), Tree(a)) deriving (Show)

-- The higher-kinded tower for Tree. Traversable names Functor and Foldable as
-- superclasses, so this instance trio is what lets the prelude's generic
-- `traverse`/`fmap`/`fold_r` resolve on the `Tree` head. Each delegates to a
-- top-level recursive walker; `twalk` is itself effect-polymorphic.
fn tmap(g, t) =
  match t of
    Leaf(x) => Leaf(g(x))
    Branch(l, r) => Branch(tmap(g, l), tmap(g, r))

fn tfold(g, z, t) =
  match t of
    Leaf(x) => g(x, z)
    Branch(l, r) => tfold(g, tfold(g, z, r), l)

fn tfoldl(g, z, t) =
  match t of
    Leaf(x) => g(z, x)
    Branch(l, r) => tfoldl(g, tfoldl(g, z, l), r)

fn twalk(g, t) =
  match t of
    Leaf(x) => Leaf(g(x))
    Branch(l, r) => Branch(twalk(g, l), twalk(g, r))

instance functorTree : Functor(Tree)
  fn fmap(g, t) = tmap(g, t)

instance foldableTree : Foldable(Tree)
  fn fold_r(g, z, t) = tfold(g, z, t)
  fn fold_l(g, z, t) = tfoldl(g, z, t)

instance traversableTree : Traversable(Tree)
  fn traverse(g, t) = twalk(g, t)

effect State
  get() : Int
  put(Int) : Unit

effect Choice
  pick() : Bool

-- A parameter-passing State handler: the handled block becomes a state
-- transformer, run with an initial counter. The action's row is written
-- `! {State | e}` so the handler subtracts State concretely and leaves `e`
-- (any other effects the action performs) untouched for an outer handler.
fn run_state(s0, action : () -> a ! {State | e}) =
  let f =
    handle action() with
      get() resume k => \(s) -> k(s)(s)
      put(v) resume k => \(_s) -> k(())(v)
      return r => \(_s) -> r
  f(s0)

-- A Fail handler, likewise annotated `! {Fail | e}`: annotating the action row is
-- what lets a reusable handler-wrapper discharge its effect in the type (so it
-- drops out of `main`'s row), not merely at runtime.
fn attempt(action : () -> a ! {Fail | e}) =
  handle action() with
    never fail() => None
    return r => Some(r)

-- Per-leaf functions, each performing a different effect. Their rows are what
-- pick the traversal's behaviour; keeping them monomorphic keeps the example
-- about the effects, not inference.
fn number(x : Int) : (Int, Int) ! {State} =
  let n = get()
  put(n + 1)
  (n, x)

fn nonneg(x : Int) : Int ! {Fail} =
  guard(x >= 0)
  x

fn sign(x : Int) : Int ! {Choice} =
  if pick() then
    x
  else
    0 - x

fn audit(x : Int) : (Int, Int) ! {State, Fail} =
  guard(x >= 0)
  number(x)

fn main() : Unit ! {IO} =
  let t = Branch(Branch(Leaf(1), Leaf(2)), Leaf(3))
  -- State: number the leaves left to right (the State applicative elsewhere).
  println(show(run_state(0, \() -> traverse(number, t))))
  -- Fail: short-circuit the whole traversal on a bad leaf (the Maybe applicative).
  println(show(attempt(\() -> traverse(nonneg, t))))
  println(show(attempt(\() -> traverse(nonneg, Branch(Leaf(0 - 9), Leaf(2))))))
  -- Choice, by multishot resumption: one whole tree per sign assignment, all
  -- 2^3 of them collected (the List applicative; here the continuation is reentered).
  let worlds =
    handle traverse(sign, t) with
      pick() resume k => append(k(true), k(false))
      return r => Cons(r, Nil)
  println(show(length(worlds)))
  -- {State, Fail} in a single pass under two stacked handlers: number and
  -- validate at once, the row the monadic world reaches StateT s Maybe for.
  println(show(attempt(\() -> run_state(0, \() -> traverse(audit, t)))))

Because a row is an unordered set, {State, Fail} fixes no layering the way a transformer stack must: whether a failure discards the numbering or keeps it is decided by which handler sits outside the other at the use site, not baked into the type. The monad-transformer ordering question, StateT s Maybe versus MaybeT (State s), moves from the type to the handler site, free to differ from one call to the next without changing a single signature.

Classes remain single-parameter; multi-parameter classes are not supported.

7. Effects and Handlers

An effect declares a set of operations; each operation has an argument list and a result type. Performing an operation is an ordinary call to its name. A function’s effect row is the set of effects whose operations it may perform and has not handled, written ! {L, ...} on its result type, with an optional row variable tail ! {L | r}. A bare ! is an explicit empty row. A row is inferred when omitted.

An operation’s declaration carries a grade, the resumption multiplicity every handler clause for it must respect, written as the contextual prefix never, once, or many. The grades form a three-point lattice ordered never < once < many: never never resumes (the continuation is dropped), once resumes exactly once in tail position (no capture), and many may capture the continuation and resume any number of times. many is the default and the most general grade, so an operation declared with no prefix (or the explicit many) admits every handler; a grade word is written only to claim something stronger. The checking rule is one line: a handler clause’s own multiplicity must be at most its operation’s declared grade. A clause that resumes a never operation, or that captures or re-enters the continuation of a once operation, is rejected at that clause, its caret naming the operation and its declared grade; a clause more restrictive than the grade (handling a many operation tail-resumptively, say) is always allowed. The grade is a static, checked fact only: it constrains which handlers typecheck and lets the compiler keep an unrelated in-place var loop on its fast lowering when some other component resumes multishot, but it never changes the observable behavior of an accepted program.

effect State
  get() : Int
  put(Int) : Unit

-- Algebraic State by parameter passing.
--
-- The handler interprets get/put by parameter passing. Each clause returns a
-- function s -> result, and `k(v)(s)` threads the state forward. The handled
-- block becomes a state transformer that we run with an initial s.
--
-- counter() never mentions a state value, it just performs get and put. The
-- row is inferred and discharged at the handler, so the same ops could be
-- reinterpreted (logging, bounding) without touching counter.

fn tick() : Int ! {State} =
  let n = get()
  put(n + 1)
  n

fn counter() : Int ! {State} =
  tick()
  tick()
  tick()
  get()

fn run_counter(init) =
  let f =
    handle counter() with
      get() resume k => \(s) -> k(s)(s)
      put(s2) resume k => \(_s) -> k(())(s2)
      return r => \(_s) -> r
  f(init)

fn main() = println(run_counter(0))

A handle e with block discharges operations; its grammar is the handler nonterminal of the surface grammar. Each operation clause names an operation and binds its arguments and the resumption k (the captured continuation, explained below); calling k(v) resumes the suspended computation with v, and k may be called zero times (abort), once (the common case), or many times (multishot). A return r clause transforms the final value. The handler in eff_state.pr interprets get/put by threading a state parameter, so counter, which only performs the operations, never mentions a state value.

Operations and handlers are delimited control: the handle block is the delimiter (a prompt), and the resumption k is the delimited continuation it captures, the slice of computation between the perform site and the handler. Being first-class, k reinstalls that slice under the same handler when invoked. This is the typed, named generalization of shift/reset: a single prompt with one anonymous continuation becomes a row of named operations, each with its own clause, and the effect row is the static record of which delimiters a computation still requires.

A clause may invoke k any number of times; more than once makes the continuation multishot: each call re-runs the captured slice from the perform site with a different result, so one handler can pursue several futures of the same computation. This is how nondeterminism or search handlers explore alternatives (an amb operation whose clause calls k once per choice and combines the outcomes) and how generators yield and continue. Never invoking k discards the captured slice, which is exactly how raise (observability) and a never clause abort.

7.1 Residual Handlers

A handler is exhaustive by default. If it names an operation of an effect but omits another operation of that same effect, checking fails at the handler. The explicit residual form opts into forwarding those omitted operations:

effect Choice
  choose() : Bool
  commit() : Unit

fn choose_true(body : () -> a ! {Choice}) : a ! {Choice} =
  handle body() with partial {
    choose() resume k => k(true),
    return x => x
  }

The partial marker follows with; it applies to every effect represented by the operation clauses in that handler. Exhaustive handlers retain the existing handle e with { ... } spelling. Consequently an omitted clause is never an accidental forwarding rule: it is either rejected or visible at the handler site.

The typing judgment retains, beside each effect-row label, the set of operations demanded from that effect while an expression is being checked. Write uses(c, E) for that set, handled(h, E) for the operations of E named by handler h, and arms(h) for the union of effects performed directly by its return and operation clauses. For a partial handler,

residual(handle c with partial h, E)
  = (uses(c, E) − handled(h, E)) ∪ uses(arms(h), E)

and its output row contains E exactly when that residual set is non-empty. Labels for effects not named by the handler, every open row tail, and effects performed by the clauses are preserved. Clause bodies run outside the handler they define, so re-performing an operation from a clause is part of arms(h) and reaches an outer handler. An ordinary exhaustive handler uses the same rule after checking that handled(h, E) is the complete declared operation set of every E it names.

Operation coverage is a local refinement of an effect label, not a second public row syntax. The printed row remains ! {Choice} whenever any Choice operation is residual. An explicit or generalized signature containing Choice is conservative and promises no smaller operation subset, so a caller may discharge it only with an exhaustive Choice handler or leave Choice residual. This keeps module interfaces stable while still allowing two adjacent partial handlers to cancel known local subsets before generalization.

If an operation is not named by a partial handler, evaluation performs it outward exactly once with the original operation identity and payload. Its outward resumption is the captured continuation wrapped in the same partial handler, so resuming returns beneath the delimiter and eventual normal completion still runs the return clause exactly once. No clause body runs during forwarding. Grades are unchanged: forwarding neither duplicates nor discards a continuation, while a matching clause must still respect the operation’s declared never, once, or many grade.

For an operation op : (p) -> q, each matching clause is checked with its declared argument types and with

k : (q) -> answer ! residual(handle c with partial h)

The answer type is shared by the return clause and every operation clause. The residual row is the least row satisfying the body-subtraction rule and all clause-effect constraints; this is the same open-row unification used by higher-order handlers, not a default to the empty row.

Forwarding is semantic, not a lowering choice. The interpreter, evidence-passing lowering, and free-monad lowering must emit the same canonical observation trace. In particular, operation emission, outward handling, resumption, and the return clause occur in that order in every tier.

7.2 Observability

The defining property of the row discipline: an operation handled inside a function is discharged, so it does not appear in that function’s inferred row. In the example below, checked carries the row ! {Exn}, but attempt, which handles raise, is pure.

effect Exn
  raise(Int) : Int

-- Exceptions as an effect: raise and catch.
--
-- raise aborts the computation. The handler clause drops the captured
-- continuation k and returns a recovery value, so control never comes back.
-- checked() raises deep inside a helper, far from the catching handler: the
-- effect propagates across calls and is discharged where the handle sits.

fn safe_div(n, d) : Int ! {Exn} =
  if d == 0 then
    raise(0 - 1)
  else
    n / d

fn checked(n) : Int ! {Exn} =
  let a = safe_div(100, n)
  let b = safe_div(a, n - 5)
  a + b

fn attempt(n) =
  handle checked(n) with
    raise(code) resume k => code
    return r => r

fn main() =
  let good = attempt(2)
  let bad = attempt(5)
  println(good * 100 + bad)

The old joke about purity is that a function of type Int -> Int cannot launch the missiles. A single IO type can put it no more precisely than that: somewhere, something happens to the world. Here the international side effect is declared in the language itself, an effect Missiles whose row label follows first_strike through every signature that might perform it, and observability is what disarms it: war_games handles launch and never resumes, so its inferred type is () -> Int, pure. The missiles are unlaunched and absent from the type. joshua adds multishot resumption (effects and handlers): its choose clause resumes the continuation once per side, so every future of the exchange is played out under the treaty handler and their scores summed. Every future is explored, none of them wins, and joshua is still pure. So thermonuclear war doesn’t typecheck, world peace achieved.

-- The row names the missiles. A single IO type can say only that a function
-- does something to the world; here the international side effect is a row
-- label, and the only way to be rid of it is to handle it.
--
-- A handler is a treaty: install one and every launch is intercepted before
-- it reaches the world. war_games discharges Missiles without resuming, so
-- from the outside it is a pure function of type () -> Int. joshua goes
-- further: choose resumes its continuation twice, once per side, so every
-- future of the exchange is played out under the treaty and none of them
-- wins. No missiles were launched in the evaluation of this program.
--
-- Expected output:
--   greetings professor falken
--   winning moves: 0
--   joshua: 0 winning moves across every future

effect Missiles
  launch(Int) : Unit

effect Warplan
  choose() : Bool

fn first_strike() : Int ! {Missiles} =
  launch(100)
  1

fn exchange(us_first : Bool) : Int ! {Missiles} =
  if us_first then
    launch(100)
  else
    launch(99)
  1

-- a strange game. the only winning move is not to play.
fn war_games() : Int =
  handle first_strike() with
    launch(_warheads) resume _k => 0
    return moves => moves

fn played(us_first : Bool) : Int =
  handle exchange(us_first) with
    launch(_warheads) resume _k => 0
    return moves => moves

fn joshua() : Int =
  handle played(choose()) with
    choose() resume k => k(true) + k(false)
    return total => total

fn main() =
  println("greetings professor falken")
  println("winning moves: {war_games()}")
  println("joshua: {joshua()} winning moves across every future")

7.3 Clause Sugar

Two clause forms abbreviate common shapes. once op(x) => e is tail-resumptive sugar for op(x) resume k => k(e), resuming exactly once. val v = e is an install-time constant: e runs once when the handler installs, and every use of v returns it.

-- `once` and `val` handler clauses, pure desugaring sugar.
--
-- `once op(x) => e` is a tail-resumptive clause, identical to
-- `op(x, k) => k(e)`, resuming exactly once with e. `val v = e` is an
-- install-time constant: e runs once when the handler installs (its effects
-- land on the installer, not the handled block) and every v() returns it.
--
-- Expected output:
--   999     (printed once at install, from val tag)
--   prism
--   ready
--   70      (tag 0 + width(3) + width(4), each * 10)

effect App
  name() : String
  tag() : Int
  width(Int) : Int
  log(String) : Unit

fn render() : Int ! {App} =
  log(name())
  log("ready")
  tag() + width(3) + width(4)

fn run_app() : Int ! {IO} =
  handle render() with
    val name = "prism"
    val tag =
      println(999)
      0
    once width(w) => w * 10
    log(s) resume k =>
      println(s)
      k(())
    return r => r

fn main() = println(run_app())

A never op(x) => e clause is non-resumable: it discards the continuation. This is the shape that error, throw, try, and catch desugar to (errors and failure).

7.4 Masking

mask<E>(e) makes every operation of effect E performed in e bypass the innermost enclosing handler of E and reach the next one out. Masks nest, so a double mask skips two handlers. The masked expression still demands an enclosing handler, so E remains in its row.

-- Effect masking. `mask<Eff>(e)` makes every Eff operation in e
-- bypass the innermost enclosing Eff handler and reach the next one out.
-- Masks nest, so a double mask skips two handlers. The row type still injects
-- Eff, so a masked expression demands an enclosing handler. Dispatch skips
-- one matching frame per mask.
--
-- Expected output:
--   12
--   300
--   13

effect Ask
  ask() : Int

-- inner answers 2, outer 10. ask() + mask<Ask>(ask()) = 2 + 10 = 12
fn shadowed() =
  handle (handle ask() + mask<Ask>(ask()) with {
      ask() resume k => k(2),
      return r => r
    }) with
    ask() resume k => k(10)
    return r => r

-- three handlers deep (inner 1, middle 100, outer 200). The single mask
-- reaches the middle, the double mask the outer. 100 + 200 = 300
fn deep() =
  handle (handle handle mask<Ask>(ask()) + mask<Ask>(mask<Ask>(ask())) with {
      ask() resume k => k(1),
      return r => r
    } with {
      ask() resume k => k(100),
      return r => r
    }) with
    ask() resume k => k(200)
    return r => r

-- the inner clause re-performs ask, answered by the outer (3). The masked ask
-- in the body skips to the outer too. 3 + 3 + 7 = 13
fn reask() =
  handle (handle ask() + mask<Ask>(ask()) + 7 with {
      ask() resume k => k(ask()),
      return r => r
    }) with
    ask() resume k => k(3)
    return r => r

fn main() =
  println(shadowed())
  println(deep())
  println(reask())

7.5 Named Handlers

The statement form with handler { ... } scopes a handler over the remainder of the enclosing block, so a stack of handlers reads as a flat sequence of layers rather than a rightward drift of nested handle expressions (composing rows puts this form to work). Adding a binder makes the handler first-class: with f <- handler { ... } installs the handler and binds it as an instance, and an operation addressed through it, f.read(), dispatches to that instance even when another handler of the same effect sits closer. A bare read() still reaches the innermost ordinary handler, so two instances of one effect can serve one scope, distinguished by name where the innermost-handler rule alone could not tell them apart. Masking skips handlers by position; a named handler addresses one directly.

-- Koka-style named handlers. `with f <- handler { .. }` binds a first-class
-- handler instance. `f.op(args)` dispatches to that instance even when another
-- handler of the same effect sits closer. Each instance desugars to a fresh
-- private effect (ops renamed op@f@n, unforgeable from source), so the rest of
-- the pipeline sees ordinary effects. Escape analysis rejects a closure that
-- would carry an instance out of its `with` block.
--
-- Expected output:
--   conf.toml
--   data.csv
--   conf.toml:data.csv
--   inner/named
--   70

effect Read
  read() : String

effect Ask
  ask() : Int

-- two instances of one effect. Dispatch is by instance, not by innermost.
fn sources() =
  with conf <- handler
    read() resume k => k("conf.toml")
    return r => r
  with data <- handler
    read() resume k => k("data.csv")
    return r => r
  println(conf.read())
  println(data.read())
  println(concat(conf.read(), concat(":", data.read())))

-- a bare read() still goes to the innermost ordinary handler. The named
-- instance only answers calls addressed through it.
fn mixed() =
  with named <- handler
    read() resume k => k("named")
    return r => r
  let inner =
    handle read() with
      read() resume k => k("inner")
      return r => r
  println(concat(inner, concat("/", named.read())))

-- multishot through a named instance. The continuation after h.ask() is
-- resumed twice. (3 * 10) + (4 * 10) = 70
fn multishot() : Int =
  with h <- handler
    ask() resume k => k(3) + k(4)
    return r => r
  h.ask() * 10

fn main() =
  sources()
  mixed()
  println(multishot())

Each instance desugars to a fresh private effect whose operations are unforgeable from source, so the rest of the pipeline sees ordinary effects and ordinary rows; resumption is unrestricted through an instance (the multishot clause above resumes the continuation of h.ask() twice). The escape analysis of local mutation applies here too: a closure or returned value that would carry an instance out of its with block is rejected, so an instance never outlives its handler.

The resource form with x <- f(args) generalizes the same shape to any function that takes its continuation last: the remainder of the block becomes a function \(x) -> rest appended to the call’s arguments, so f decides when, whether, and how often to run the rest. This is the bracket idiom (acquire, use, release) written without nesting.

The same scope-local skolem underwrites ordered containers. A Map(k, v) is ordered by the ambient canonical Ord(k), but a program that needs two orderings of the same keys at once cannot let a map built under one be walked under the other: the tree structure encodes the ordering, so a lookup under the wrong comparator silently returns the wrong answer. The map type carries a third, phantom parameter for exactly this, Map(k, v, ord), a brand naming the ordering a map was built under; it appears in no field, so an unbranded Map(k, v) is the same type with the brand left to inference, and pre-brand source keeps checking unchanged. The Data.Ordered module (import Data.Ordered) hands out brands the way a named handler hands out an instance. with_ordering(cmp, body) runs body with a witness carrying cmp, and the witness’s brand is a fresh rigid skolem unique to that call, so a map built through one witness carries a brand that a second witness’s brand cannot unify with. Two witnesses coexist in one scope, and handing a map built under one to the other’s operation is a compile-time type error naming both brands. The brand never escapes: the body’s result may not mention it, so only a summary of a branded map (a size, a looked-up value, an encoded form) leaves the block, never the branded map itself.

This is the explicit half of the coherence story, and it closes statically. The implicit half is calling the ambient map_insert under a non-canonical Ord chosen with using, then reading the result under the canonical one. Because those two maps have the same unbranded type, the implicit path is caught dynamically where it does the most harm: when an ordered container crosses a package boundary. A serialized map records its keys in the writer’s order, and Wire’s map reader checks that they arrive strictly ascending under its own Ord(k), faulting through failure rather than rebuilding a mis-ordered tree when a map ordered by one comparator is read where a different one is canonical. Both faults, the compile-time brand mismatch and the runtime order check, are pure functions of the source and the pinned inputs, so a program’s behavior never reveals which backend ran it. The division is deliberate and stated as such: the explicit witness path is static, while the implicit path is dynamically checked at the wire boundary.

7.6 Local Mutation

A var mutates, yet the function holding it stays pure. fib_iter below updates two locals in a loop but has type (Int) -> Int with an empty row, so it is accepted where only a pure function is allowed. Prism has no mutation primitive; var is sugar over the effect system.

A var x := e desugars to a private two-operation effect (a get and a set); each read of x becomes a perform of get, each x := v a perform of set. In the same pass, a handler that threads the value as a hidden parameter is wrapped around the block. That handler discharges the get and set labels (observability), so they never reach the function’s type: the state is implemented but not observable. Because an escape analysis (below) has proved the state never leaves its block, effect lowering then erases the whole handler to a mutable cell, turning each get into a cell read and each set into a cell write, and the loop into a constant-stack loop, so the lowered code allocates nothing per iteration.

-- twice demands a pure (Int) -> Int. fib_iter mutates two locals in a loop,
-- yet is accepted here: its inferred row is empty.
fn twice(f : (Int) -> Int) = f(f(6))

fn fib_iter(n : Int) : Int =
  var a := 0
  var b := 1
  repeat(n) fn
    let t = a + b
    a := b
    b := t
  a

fn main() = println(twice(fib_iter))

fn fib_iter(n) =
  handle
    handle
      return n to t@739
      thunk { \.
        return () to t@740
        do get@a@0(t@740) to t@742
        return () to t@741
        do get@b@1(t@741) to t@743
        t@742 + t@743 to t
        return () to t@744
        do get@b@1(t@744) to t@745
        do set@a@0(t@745)
        return t to t@746
        do set@b@1(t@746)
      } to t@747
      repeat(t@739, t@747)
      return () to t@748
      do get@a@0(t@748)
    with
      get@b@1(u@, k@) =>
        thunk { \s@.
          return s@ to t@749
          return s@ to t@750
          return k@ to t@751
          (force t@751)(t@750) to t@752
          (force t@752)(t@749)
        }
      set@b@1(v@, k@) =>
        thunk { \s@.
          return v@ to t@753
          return () to t@754
          return k@ to t@755
          (force t@755)(t@754) to t@756
          (force t@756)(t@753)
        }
      return r@ =>
        return thunk { \s@. return r@ }
    to run@1
    return 1 to t@757
    return run@1 to t@758
    (force t@758)(t@757)
  with
    get@a@0(u@, k@) =>
      thunk { \s@.
        return s@ to t@759
        return s@ to t@760
        return k@ to t@761
        (force t@761)(t@760) to t@762
        (force t@762)(t@759)
      }
    set@a@0(v@, k@) =>
      thunk { \s@.
        return v@ to t@763
        return () to t@764
        return k@ to t@765
        (force t@765)(t@764) to t@766
        (force t@766)(t@763)
      }
    return r@ =>
      return thunk { \s@. return r@ }
  to run@0
  return 0 to t@767
  return run@0 to t@768
  (force t@768)(t@767)

fn fib_iter(n) =
  ref_new 0 to 0@cell
  ref_new 1 to 1@cell
  thunk { \.
    ref_get 0@cell to t@742
    ref_get 1@cell to t@743
    t@742 + t@743 to t
    ref_get 1@cell to t@745
    ref_set 0@cell t@745
    ref_set 1@cell t
  } to t@747
  repeat(n, t@747)
  ref_get 0@cell

The two tabs are the compiler’s own dumps: Core (prism dump core) is the elaborated form, where each var has become a private two-operation State effect (do get@a@0 / do set@a@0) wrapped in a value-threading handler, one nested handler per var; Lowered (prism dump lowered) is after effect lowering, where the escape check has let those handlers collapse to a mutable cell (ref_new / ref_get / ref_set) and the loop to a constant-stack repeat. The get/set effect never reaches the function’s type, so fib_iter stays pure.

An escape analysis keeps the purity honest: the compiler rejects any closure or returned value that would carry the var out of its block, so the state cannot outlive its handler.

7.7 Errors and Failure

Prism has no built-in exception type. Errors and failure are two related mechanisms, both resting on the non-resumable never clause of the clause sugar. With the imperative break, continue, and return of imperative control flow, they are one mechanism wearing several faces: each is a single-operation effect whose handler never resumes the captured continuation, installed only where the corresponding keyword actually occurs, so non-local control costs nothing where it is not used and (being handled at its boundary) surfaces in no effect row where it is.

Extensible errors. An error N(t) declaration introduces a one-operation effect whose operation never resumes; throw N(x) performs it. A function’s error row is exactly the set of errors it may raise and has not caught, and distinct error declarations union structurally as functions compose, with no umbrella sum type and no conversion glue: find_port carrying {NotFound} and parse_port carrying {Malformed} compose to {NotFound, Malformed}. try e catch { ... } is subtractive handler sugar (one nested never per arm): a partial catch discharges the labels it names and lets the rest flow to an enclosing handler, and an uncaught error is an unhandled-effect error naming exactly the labels that remain. Each catch arm names an error and binds its fields to variables.

-- Errors as effect rows. Each `error` declaration is its own effect label and
-- `throw` performs it, so a function's row is its error set. find_port carries
-- {NotFound}, parse_port carries {Malformed}, and their composition unions to
-- {NotFound, Malformed} with no umbrella enum or conversion glue.
--
-- `try`/`catch` is subtractive handler sugar (one nested `never` per arm).
-- A partial catch discharges its label and passes the rest to an outer try. An
-- uncaught case is an unhandled-effect error naming exactly what remains.
--
-- Expected output:
--   8080
--   default 80
--   bad config: oops
--   443
--   no such key: tls
--
error NotFound(String)

error Malformed(String)

fn find_port(cfg, key) =
  match cfg of
    Nil => throw NotFound(key)
    Cons(pair, rest) =>
      let (k, v) = pair
      if k == key then
        v
      else
        find_port(rest, key)

fn parse_port(s) =
  if s == "8080" then
    8080
  elif s == "443" then
    443
  else
    throw Malformed(s)

-- Composed: the row unions to {NotFound, Malformed}.
fn port_of(cfg, key) : Int ! {NotFound, Malformed} =
  parse_port(find_port(cfg, key))

fn describe(cfg, key) =
  try
    show(port_of(cfg, key))
  catch
    NotFound(k) => "no such key: {k}"
    Malformed(s) => "bad config: {s}"

fn main() =
  let cfg = [("http", "8080"), ("https", "443"), ("smtp", "oops")]
  println(describe(cfg, "http"))
  let port =
    try
      try port_of(cfg, "gopher") catch { Malformed(_s) => 0 }
    catch
      NotFound(_k) => 80
  println("default {show(port)}")
  println(describe(cfg, "smtp"))
  println(describe(cfg, "https"))
  println(describe(cfg, "tls"))

Stacks of failure modes. Because each error is an ordinary row label, a row alias (composing rows) names a set of failure modes: alias ConfigErr = {NotFound, Malformed} states a subsystem’s failure vocabulary once, and a layer above extends it structurally, alias AppErr = {ConfigErr, NetErr}, with no umbrella type and no wrapping. A signature : Int ! {AppErr} reads as “may fail in exactly these ways”, and because expansion flattens before checking, catch subtracts labels from the expanded set like any other handler: a partial catch over an alias discharges the modes it names and leaves the rest in the row.

-- A row alias names a stack of failure modes. ConfigErr is the failure
-- vocabulary of the config subsystem, NetErr of the transport; AppErr splices
-- both. Expansion flattens, so !{AppErr} is exactly {NotFound, Malformed,
-- Timeout}, and a partial catch subtracts labels from that set: config_safe
-- discharges ConfigErr and its row keeps only NetErr.
--
-- Expected output:
--   8105
--   80

error NotFound(String)

error Malformed(String)

error Timeout(Int)

alias ConfigErr = {NotFound, Malformed}

alias NetErr = {Timeout}

alias AppErr = {ConfigErr, NetErr}

fn read_port(cfg, key) : Int ! {ConfigErr} =
  match cfg of
    Nil => throw NotFound(key)
    Cons(pair, rest) =>
      let (k, v) = pair
      if k == key then
        if v == "8080" then
          8080
        else
          throw Malformed(v)
      else
        read_port(rest, key)

fn ping(ms) : Int ! {NetErr} =
  if ms > 100 then
    throw Timeout(ms)
  else
    ms

fn boot(cfg) : Int ! {AppErr} = read_port(cfg, "http") + ping(25)

-- a partial catch: ConfigErr's labels are discharged, Timeout remains
fn config_safe(cfg) : Int ! {NetErr} =
  try boot(cfg) catch { NotFound(_k) => 80, Malformed(_s) => 80 }

fn main() =
  let good = [("http", "8080")]
  let bad = [("http", "oops")]
  let full =
    try
      boot(good)
    catch
      NotFound(_k) => 0
      Malformed(_s) => 0
      Timeout(_ms) => 0
  println(full)
  let fallback = try config_safe(bad) catch { Timeout(_ms) => 0 }
  println(fallback)

These idioms span the recovery spectrum: the built-in Exn effect, raised by error(code) and uncatchable (it aborts); Result with the postfix e? propagation of the expression forms; a plain match on Ok/Err; and a custom non-resumable effect.

-- Failure, four idioms from a defaulted lookup to a custom throw, over the
-- everyday shape: reaching into chains of things that can fail.
--
-- 1. Indexing performs `Fail`, not `Option`: `users[i]` and `scores[j]` each
--    may miss, the misses flow through the chain as one row, and `?? d`
--    supplies the default at the end. TypeScript's `a?.[i] ?? d`, with the
--    partiality in the type instead of a null.
-- 2. `?` propagates over `Result`: each step unwraps `Ok` and short-circuits
--    the function on the first `Err`, exactly Rust's `?`.
-- 3. The boundary is a plain match on `Ok`/`Err`.
-- 4. A custom non-resumable effect: `abort` never resumes, the continuation is
--    discarded, and the clause's value becomes the result. Cheap throws, with
--    no Result plumbing inside the throwing code.
--
-- Expected output:
--   71
--   0
--   ada scored 92
--   gus has no scores
--   no user zoe
--   pass
--   invalid: negative

type User = MkUser { name: String, scores: List(Int) }

fn lookup_user(users : List(User), want : String) : Result(User, String) =
  match find(\(u) -> u.name == want, users) of
    Some(u) => Ok(u)
    None => Err(concat("no user ", want))

fn top_score(u : User) : Result(Int, String) =
  match u.scores of
    Nil => Err(concat(u.name, " has no scores"))
    Cons(s, _) => Ok(s)

-- Two failable steps, one `?` each: the first Err returns from `headline`
-- immediately, so the happy path reads straight down.
fn headline(users : List(User), want : String) : Result(String, String) =
  let u = lookup_user(users, want)?
  let s = top_score(u)?
  Ok(concat(u.name, concat(" scored ", show_int(s))))

fn report(r : Result(String, String)) =
  match r of
    Ok(line) => println(line)
    Err(e) => println(e)

effect Abort
  abort(String) : Unit

fn grade(n : Int) : String ! {Abort} =
  if n < 0 then
    abort("negative")
  if n > 100 then
    abort("too big")
  if n >= 60 then
    "pass"
  else
    "fail"

fn safe_grade(n : Int) : String =
  handle grade(n) with
    never abort(msg) => concat("invalid: ", msg)
    return r => r

fn main() =
  let users = [
      MkUser { name = "ada", scores = [92, 71] },
      MkUser { name = "gus", scores = [] },
    ]
  -- 1: a chain of failable lookups, defaulted once at the end. The second
  -- line misses at the first hop and the whole chain yields the default.
  println((users[0].scores)[1] ?? 0)
  println((users[5].scores)[0] ?? 0)
  -- 2 and 3: `?`-propagated Results, matched once at the boundary.
  report(headline(users, "ada"))
  report(headline(users, "gus"))
  report(headline(users, "zoe"))
  -- 4: the custom throw.
  println(safe_grade(72))
  println(safe_grade(0 - 5))

The failure axis. Beyond named errors, Prism has an anonymous, recoverable fail(), the deterministic-functional-logic failure of the Verse calculus (Augustsson et al., 2023). guard(b) fails when b is false; a ?? b runs a under a failure handler and falls back to b; e?.field chains through options, failing on None; optional/succeeds/default reify a failing computation as an Option, a Bool, or a default; and a comprehension guard may itself fail, pruning the element (expressions). transact body else fallback snapshots every live var, runs the body under a failure handler, and restores the snapshots on failure, so an aborted attempt leaves observable state unchanged. The whole axis is never handlers over a Fail effect, so an unhandled fail() is the ordinary unhandled-effect error, and “failable only in a failure context” falls out of the row discipline for free.¹⁸

-- Transactional rollback. A purchase that fails on insufficient funds leaves
-- balance and stock untouched, as if it never happened. The first buy succeeds.
-- The second overspends, so `guard` fails inside the `transact` and both vars
-- roll back to their pre-attempt values.
fn main() =
  var balance := 100
  var stock := 5
  let r1 =
    transact
      balance -= 40
      stock -= 1
      guard(balance >= 0)
      1
    else
      0
  println(balance)
  println(stock)
  println(r1)
  let r2 =
    transact
      balance -= 90
      stock -= 1
      guard(balance >= 0)
      1
    else
      0
  println(balance)
  println(stock)
  println(r2)

Partiality is in the row, not the name. ML libraries such as OCaml’s Base and Core suffix a partial function with _exn (List.hd_exn) so a reader knows it may raise, a naming convention standing in for what the type itself cannot say. Prism needs no such convention: a function that may fail carries that in its effect row, whether as the anonymous Fail above or a named error, so the possibility of failure is written into the signature and the row discipline forces it to be handled before the result is used. The _exn suffix is the workaround for a type system that cannot express failure; the row is the version the compiler checks.

7.8 Composing Rows

A row alias composes rows the way + composes sums. With AB = {A, B} and CD = {C, D}, the row {AB, CD, E} assembles five effects from two named pairs and a fifth label: (A + B) + (C + D) + E. Because a row is an unordered set (subsumption and row equivalence) and an alias expands transparently before checking, the sum flattens: any grouping and any order of the same five labels is the same row, so omega and flat below are interchangeable, and a grouping is chosen for the reader, not for the checker. An alias may reference other aliases (a cycle is an error at the declarations involved), and takes no parameters.

-- Rows compose like sums. AB and CD each name a pair of effects; App splices
-- both and adds a fifth label. Aliases expand and flatten before checking, so
-- {AB, CD, E} IS {A, B, C, D, E}: omega and flat have the same type, and the
-- grouping is documentation that leaves no trace in the semantics.

effect A
  alpha() : Unit

effect B
  beta() : Unit

effect C
  gamma() : Unit

effect D
  delta() : Unit

effect E
  epsilon() : Unit

alias AB = {A, B}

alias CD = {C, D}

alias App = {AB, CD, E}

fn phi() : Unit ! {AB} =
  alpha()
  beta()

fn psi() : Unit ! {CD} =
  gamma()
  delta()

fn omega() : Unit ! {App} =
  phi()
  psi()
  epsilon()

-- the flattened spelling of the same row: either may call the other
fn flat() : Unit ! {A, B, C, D, E} = omega()

This is the row discipline’s answer to the monad-transformer stack. A transformer application fixes one composite type, ReaderT Config (WriterT Log (Except E)), and pays for it twice: every layer’s operations are lifted through the layers above (or a class such as MonadWriter is threaded through, at a quadratic cost in instances), and the order of wrapping is welded into every signature even where no code depends on it. An alias instead makes the application row a name for a set, Ctx = {Ask, Tell} and App = {Ctx, Invalid} below. An operation reaches its handler by label, never by position, so there is no lift; a function that uses only Tell states !{Tell} and slots unchanged into App or any other row containing it; and two subsystems’ aliases union structurally, with no adapter between their stack and ours.

What a transformer stack fixes in the type, the handler site decides per call (the layering point already made for {State, Fail} under higher-kinded classes). Discharged one label at a time with the scoped with handler layers of named handlers, the run function reads like the transformer stack it replaces, except that the order is chosen where the handlers install, free to differ between call sites without a signature changing. The application monad becomes the application row: a name for what may happen, not a recipe for how it is wrapped.

-- An application row in place of a transformer stack. Ask is the reader layer,
-- Tell the writer, Invalid the exception; Ctx names the ambient pair and App
-- adds failure. A function states the part of the stack it uses (greet needs
-- only Tell) and slots into any row that contains it, with no lifting. The
-- run function is a flat sequence of scoped handlers, one per label, in an
-- order chosen here rather than fixed by a type.
--
-- Expected output:
--   hello
--   step 3
--   7
--   hello
--   step 99
--   0

effect Ask
  ask() : Int

effect Tell
  tell(String) : Unit

error Invalid(Int)

alias Ctx = {Ask, Tell}

alias App = {Ctx, Invalid}

fn greet() : Unit ! {Tell} = tell("hello")

fn step(n) : Int ! {App} =
  greet()
  let limit = ask()
  tell("step {n}")
  if n > limit then
    throw Invalid(n)
  else
    limit - n

fn run_app(n : Int) : Int ! {IO} =
  with handler
    once ask() => 10
  with handler
    once tell(m) => println(m)
  try step(n) catch { Invalid(_bad) => 0 }

fn main() =
  println(run_app(3))
  println(run_app(99))

7.9 Effect Polymorphism

A function can be generic over the effects of a thunk it is given by quantifying over a row variable in the argument’s type. Below, twice accepts any (Unit) -> Int thunk and adds an open row {| e} for whatever that thunk performs; each call unifies e with the actual row (empty, {Tick}, or {Say}), and a handler discharges only the label it names, leaving the rest in e. This is the mechanism the prelude’s fmap and traverse use to thread a per-element effect (higher-kinded classes), so an effectful traversal needs no Applicative wrapper.

The same row variable also governs an effect operation whose argument is a computation. An operation such as concurrency’s fork(() -> a ! {Async(a) | e}) shares the ambient row for e: performing it ties the argument’s row to the caller’s own, so a forked or deferred computation may perform only effects the caller already admits, and those effects flow out to whoever handles the operation rather than escaping it (the discipline of Koka, Frank, and Links; Leijen, 2017). Combined with a Row-kinded parameter (kinds) that stores the reified continuations, this is what makes a handler like run_async both effect-polymorphic and sound: it is written once for any row e the fibers perform, and a fiber cannot smuggle past it an effect that no outer handler was required to discharge.

The quantifier’s scope is enforced in the other direction too. A row bound by an inner forall is rigid and dies with its binder, so a row introduced outside that forall may never be solved to it: a closure whose body’s effects could only be satisfied by pinning an enclosing row onto the bound variable is rejected with an error naming the capture, the row analogue of a skolem-escape error, rather than accepted with a solution that outlives its scope.

effect Tick
  tick() : Int

effect Say
  say(Int) : Unit

-- Effect polymorphism: one higher-order function, any effect row.
--
-- twice is written once, with a row variable e for whatever its argument
-- performs. Each call site unifies e with that thunk's row: {} for the pure
-- thunk, {Tick} and {Say} for the effectful ones. A handler discharges only
-- the label it names. e carries the rest along.

fn twice(f : (Unit) -> Int ! {| e}) = f(()) + f(())

-- e = {}: pure code needs no handler at all.
fn pure_use() = twice(\(_u) -> 21)

-- e = {Tick}: a counting handler hands out 1 then 2, so the same thunk
-- answers differently per force.
fn tick_use() =
  let g =
    handle twice(\(_u) -> tick()) with
      tick() resume k => \(n) -> k(n)(n + 1)
      return r => \(_n) -> r
  g(1)

-- e = {Say}: each force shouts before answering.
fn say_use() =
  handle twice(\(_u) -> let _ = say(9) in 9) with
    say(m) resume k =>
      println(m)
      k(())
    return r => r

fn main() =
  println(pure_use())
  println(tick_use())
  println(say_use())

7.10 Coeffects

Prism has two static axes that deliberately do not collapse into one row. The effect row records what a computation may do to the world: perform Console, FileSystem, Async, Clock, Fail, a user effect, and so on. Usage and resource annotations record how a value, call tree, or continuation may be used. They are coeffects, the dual of effects: an effect flows outward from the computation and is discharged by a handler around it, while a coeffect flows inward from the context and is discharged by the boundary that consumes the value, so one tracks what the program does to its world and the other what the world may do with the program’s values. The user model is one sentence: ! says what happens; @ says how a value may be used.

Think of a bottle of prescription medicine. The effect row is the side-effects leaflet: take this and it may cause drowsiness, print to the console, or talk to the filesystem; whoever administers it (the handler) decides what to do about that. The usage row is the dosage instructions on the label: take at most once (@ once), do not share (@ noescape), keep refrigerated (@ local), safe to travel with (@ portable). The leaflet describes what the pill does to you; the label restricts what you may do with the pill. A pharmacist who ignores the leaflet has a surprised patient; one who ignores the label has a lawsuit.

Usage rows. A usage row attaches usage facts to a type with a postfix @, mirroring how ! attaches an effect row to a function type:

buf : Buffer @ unique
fn spawn(f : (() -> a ! e) @ {once, portable}) : Fiber(a) ! {Async(a), e}

The row attaches to an atomic type: a constructor, an application, a tuple, or a parenthesized type. A function type must be parenthesized to take a row; writing one after an effect row is refused with the fix spelled out (parenthesize the function type before '@') rather than silently picking a precedence. A single fact may drop the braces (T @ unique); the formatter canonicalizes a one-fact row to that form. A row is a set: duplicate facts and two facts from one exclusive axis (@ {once, many}) are errors, the empty row is an error, and the canonical order is alphabetical, so a row’s spelling, its formatted output, and its contribution to a definition’s content hash never depend on the order the author wrote. The open-tailed form @ {fact | u} is reserved for usage-row polymorphism and rejected by name.

The reserved vocabulary is fixed, and an unknown word in usage position is a hard error, never a warning, so no program or package can establish a private meaning for a fact before its checker exists. The facts are not a flat list: each belongs to one semantic axis, and the axis determines how its facts combine in a row and which side of an API seam owes the proof:

An exclusive axis is a choice of one point, which is why @ {once, many} is rejected as a contradiction at parse. Only the fip axis composes, because its facts are cumulative strengthenings of one certificate rather than alternatives. Polarity is the axis’s variance discipline, the direction its proof obligation flows. A past fact is covariant: it records how a value was built, the producer proves it, and the fact travels with the value wherever it goes. A future fact is contravariant: it restricts what may still be done with the value, the consumer promises it, and the fact binds at the use site. The polarity is stated by proof obligation, deciding which side of an API seam owes the evidence when a fact is checked.¹⁹

The multiplicity axis already has a checked instance elsewhere in the language, applied to a continuation rather than a value: an operation’s grade (effects and handlers) is never, once, or many, the same words on the same lattice, restricting how a handler clause may resume the captured continuation k. The grade on an operation and the multiplicity fact on a closure are the same point on the same axis, read at two boundaries: the operation form is checked on a continuation and pins once to exactly one resumption in tail position, while the value form is affine, at most one use of the annotated closure. It adds one point the value facts omit, never (the continuation is dropped), because a value used zero times is not a tracked usage fact but a clause that never resumes is a real, useful grade. That shared vocabulary is not a coincidence of spelling: the continuation an operation hands its handler is the first value in the language to carry a coeffect, which is what makes “an effect is just a coeffect on its own continuation” (three posets) a literal statement rather than a slogan.

The facts themselves:

The checked facts are noalloc, once, portable, and noescape. Other reserved facts are rejected.

Boundary facts, not ambient modes. This design space ranges from ambient classifications carried by every value to explicit claims checked only where needed. Prism chooses the latter: @ once constrains one consumer, @ portable one crossing, and @ noalloc one call tree; unannotated values carry no mode vector.

Operation grades are the established instance of this design. never < once < many constrains one handler boundary, survives desugaring as typed data, and is consumed directly by lowering.

The wider family reads as one story. borrow lets a function read an argument without taking ownership. fip certifies allocation-freedom, linear consumption of owned heap values, and bounded stack for the recursive group. fbip keeps the allocation-free call-tree certificate without the full linear and bounded-stack promise. @ noalloc is the allocation certificate alone. Operation grades classify continuation use in handlers.

This split matters. A function may be @ noalloc and still perform IO; the row says the output effect is observable, while the allocation certificate says the call tree does not allocate fresh cells.

Two mechanisms, one vocabulary. Allocation can be forbidden: @ noalloc (allocation certificates) proves a call tree allocates no fresh cell. It can also be avoided: an unboxed representation stores a value inline, so no heap cell is created. The certificate establishes whether allocation happens, while the representation determines whether a cell is needed. The Arena library expresses allocator selection as a handled Alloc effect rather than a surface storage class; it changes the allocation path without changing the certificate vocabulary.

Checked closure contracts. Three usage facts are checked closure contracts. @ once on a function-typed parameter admits a value used at most once²⁰: a @ many value fits a @ once slot but never the reverse, and using the parameter twice, aliasing it through a let, or capturing it under a lambda counts as further use and is rejected (E6059). @ portable admits a closure that captures only what travels to a fresh runtime: a content-addressed top-level function or constructor, another portable parameter, or portable scalar data; a captured local closure, var cell, or handler operation is rejected by name (E6060). @ {once, portable} requires both at once. @ noescape, written on a function domain ((Builder @ noescape) -> a), promises the callback’s argument does not outlive the call: a token that is returned, embedded in returned data, aliased out, or captured by another closure is rejected (E6061), and the callback must be a checkable form, a closure literal, top-level function, or same-contract relay (E6062). Every fact is erased before the core, so an accepted program is byte-identical on both backends: the contract governs what the compiler accepts, never what a passing program does.

teleport(f : (() -> a) @ {once, portable}) : a (the Teleport module) is the checked mobility boundary built from those facts: its parameter type makes each call prove the closure captures only content-addressed code and portable data and runs at most once, so the computation is safe to move to a fresh runtime. Placement is unobservable in exactly the way tier and backend choice are, so running a teleported closure is observationally identical to calling it directly; the boundary changes what is accepted, not what happens.

import Teleport (..)

fn classify(seed : Int) : Int = seed * 2

fn run_once(f : (() -> Int) @ once) : Int = f()

fn main() =
  println(run_once(\() -> 1))
  -- The closure captures only a top-level function: portable, single use.
  println(teleport(\() -> classify(21)))

7.11 Structured Concurrency and Cancellation

The Concurrent library builds cooperative concurrency and cancellation on the Async operations above, and their contract is stated here as observable behavior rather than as a property of one lowering tier. A scope(tasks) is a structured join: it forks a list of fibers and awaits them all on a successful run. It is not a failure-isolation boundary or a distinct internal nursery protocol. The scheduler tracks fork parentage globally so cancellation reaches everything a target forked.

Cancellation is a cooperative unwind, not an abrupt drop. cancel(f) marks the fiber f and all of its descendants; each stops at its next suspension point (a yield, an await, a channel operation) rather than mid-step, and then unwinds through the cancellation handlers it has already entered. A cancellation cleanup is installed with on_cancel(cleanup, body): if cancellation crosses that handler, cleanup runs exactly once before cancellation continues outward; a normally returning body does not run it. Nested on_cancel cleanups run innermost first, the same order a stack of never handlers unwinds (clause sugar). The cleanup executes outside the handler clause it is finalizing, but the scheduler marks the fiber as unwinding: repeated cancellation is masked, so cleanup may suspend and resume normally rather than being stopped a second time. A child forked during cleanup is immediately marked for cancellation and cannot escape the unwind. Cancelling a fiber before it starts does not enter its body and therefore installs or runs none of that body’s cleanups. Cancelling a completed leaf changes nothing, but cancelling a completed parent still reaches any live descendants retained in the fork tree.

Waiting on a fiber that may be cancelled is a join. try_await(f) returns an Outcome(a) = Completed(a) | Was_Cancelled, Completed(v) when f produced v and Was_Cancelled only after the cancelled fiber’s unwind and installed cleanups have completed, where a bare await would have no value to yield. A cancellation request and a completed cancellation are therefore distinct scheduler states; observing the request alone is not enough to return from try_await. If a cleanup itself performs an unhandled fail(), the cancellation never enters the completed set and try_await returns no Outcome: the scheduler aborts instead. A cleanup parked with no runnable producer reaches the scheduler’s deterministic no-progress failure; a cleanup that continues to produce work forever may diverge like any other program.

Unhandled fiber failure is scheduler-global. If any fiber reaches an unhandled fail() (errors and failure), run_async or run_lifo cancels every other live fiber and all of their descendants, including fibers created outside the scope whose task happened to fail. Runnable cancellation cleanups drain, then the failure re-emerges at the scheduler boundary. scope neither catches nor localizes it; it is only the structured success-path join. The failure therefore remains in the residual row of the run: run_async : (() -> a ! {Async(a) | e}) -> a ! {e} discharges Async, but a fallible fiber forces Fail into e, and a caller handles that failure outside run_async/run_lifo.

Cooperative cancellation is source-driven scheduler behavior, not an observation of the outside world: cancel is an ordinary Async operation and the chosen deterministic scheduler policy orders its consequences. It therefore adds no capability or replay-trace event. A future timer, OS signal, or preemptive cancellation source would be an explicit external capability and would require its own recorded event; none exists in this cooperative contract.

7.12 Capability Effects and IO

Reading the outside world is itself effectful, and the row records which part of the world a function reads. The nondeterministic input operations are four capability effects:

A function that reads input names exactly that capability in its row: a function calling read_int carries ! {Console}, not a blanket ! {IO}, so the row says which part of the world is read rather than merely that some IO happens.²¹ (Console, FileSystem, Random, and Env are therefore reserved effect names, among the keywords. The Concurrent library adds a fifth capability, Clock, described below. Preempt is also reserved, but the cooperative scheduler does not handle it: user declarations are rejected, and the existing row check classifies it outside the replayable capability set.)

The surface is unchanged: read_int(), read_file(p), getenv(s), and friends stay ordinary calls, defined in the prelude as thin wrappers that perform the corresponding capability operation. A default run_io world handler is wrapped around main on demand, only when main reaches a capability, and discharges each operation by performing the real input and resuming with the result, so the capabilities collapse to ! {IO} at the program boundary. The handler is tail-resumptive, so it fuses to a direct call at no cost (effect lowering). Output stays an opaque IO effect: print, write_file, append_file, and remove_file carry ! {IO} and are not capability operations, because record and replay needs only inputs pinned. Binary file IO sits on the same split: read_bytes(p) is a FileSystem capability that reads a file as raw Bytes and is recorded like any other input, its own operation rather than a detour through read_file (routing bytes through a String would corrupt them at the first non-UTF-8 byte), while write_bytes(p, bs) is an IO output returning a Result.

Below, roll performs Random alone, user performs Env alone, and summary carries the structural union ! {Env, Random} of what it calls; the capabilities collapse to ! {IO} only at main, where run_io discharges them.

-- Capability effects, the parts a browser can serve. `Random` is a deterministic
-- SplitMix64 stream (pure arithmetic, identical to the native oracle) and `Env`
-- reads the environment, empty in the playground, so `getenv` falls back. Each
-- function's row names the slice of the world it reads: `! {Random}` alone,
-- `! {Env}` alone, and their structural union, never a blanket `! {IO}`. (The
-- inputs a browser cannot serve, file reads and stdin, would be reported instead.)

fn roll() : Int ! {Random} = rand_below(6) + 1

fn user() : String ! {Env} =
  let name = getenv("USER")
  if name == "" then
    "anonymous"
  else
    name

fn summary() : String ! {Env, Random} =
  "{user()} rolled {roll()}, {roll()}, {roll()}"

fn main() = println(summary())

Because input is now an interceptable operation rather than an untracked builtin, a handler other than run_io can supply the values, which is what record/replay rests on.

Virtual Simulation Clocks

Time is a capability too. The Concurrent library’s Clock effect (now, sleep) is discharged by run_clock, which threads a pure logical counter: now() reads the current tick and sleep(d) advances it. Time is therefore virtual, deterministic, and replayable, with no real clock and no time primitive.²²

A fiber may perform Clock; because the scheduler does not handle it, Clock flows out of run_async to an enclosing run_clock like any other capability. The important move is routing now, sleep, and timeouts through an ambient time capability rather than the wall clock. A test advances a virtual clock, scheduling becomes a pure function of it, and the cooperative-deterministic story is testable rather than merely asserted.

Treating time as one capability among Console, FileSystem, Random, and Env, discharged by a handler you can swap for a real-time one, is the same move applied to the clock. The Concurrent reference has the library details.

The example below is the whole discipline on one page. Two fibers sleep and read now under run_clock, which is installed outside run_async; because the scheduler is generic in its residual row, Clock tunnels through it to the clock handler, and logical time is the running sum of the sleeps, identical on every run with no real time elapsing.

-- A logical clock as an ordinary effect: deterministic virtual time, no OS clock.
--
-- `Clock` is an algebraic effect with two operations, `now` and `sleep`. Nothing
-- here reads the operating system. `run_clock` interprets the effect by threading a
-- single integer -- the current logical tick -- through the computation: it is a
-- parameter-passing handler that reifies the program into a function `Int -> a`,
-- where `sleep(d)` resumes with the tick advanced by `d`, `now()` resumes with the
-- tick unchanged, and the whole thing is seeded at 0.
--
-- The clock is installed *outside* `run_async`. The scheduler handles `Async`
-- (fork/await/...) but not `Clock`, so every `sleep`/`now` a fiber performs tunnels
-- out through the scheduler to `run_clock`. That pass-through is the row-kinded
-- effect polymorphism at work: `run_async` is generic in the residual row `e`, so
-- `Clock` flows through it untouched rather than being trapped or forcing the
-- scheduler to know anything about time.
--
-- One tick is threaded across the entire cooperative run, so logical time is the
-- running sum of the sleeps in schedule order: A sleeps 3 (0 -> 3), then B sleeps 4
-- (3 -> 7), so B reads t=7, not t=4. `sleep` advances the shared clock but does not
-- itself reschedule, so the result is a pure function of the sleeps -- identical on
-- every run, with no real time elapsing. Swap `run_clock` for a handler that reads
-- the OS clock and the same program runs in real time, unchanged: time is a
-- capability chosen at the edge, not a primitive baked into the language.
--
-- Expected output:
--   A woke at t=3
--   B woke at t=7
--   total 10

import Concurrent (..)

fn worker(name : String, d : Int) : Int ! {Clock, IO} =
  sleep(d)
  let t = now()
  println("{name} woke at t={t}")
  t

fn scene() : Int ! {Async(Int), Clock, IO} =
  let a = fork(\() -> worker("A", 3))
  let b = fork(\() -> worker("B", 4))
  await(a) + await(b)

fn main() = println("total {run_clock(\() -> run_async(scene))}")

7.13 Capability-Based Sandboxing

Because a function’s row records exactly which capabilities it exercises and a handler is what discharges a capability, a handle block that installs a restricted set of handlers is a sandbox: a sub-computation it runs can perform only the operations those handlers answer. A function given no Async handler in scope cannot spawn a fiber; a function whose row lacks FileSystem cannot read a file; a computation run under a world handler that stubs read_file to a fixed value cannot reach the real filesystem no matter what it calls, because the only interpreter for that operation in scope is the stub.

Anything the sandbox does not discharge is not ambient background authority it might reach anyway, it is a label left in the row that some enclosing handler must still answer, and if none does the program does not type. This is object-capability security recovered from the effect row at no additional cost: authority is precisely the set of handlers in scope, it is delegated by passing a thunk into a handler rather than by granting an ambient permission, and it is attenuated by nesting a sub-computation inside a narrower handler that intercepts or denies operations before any outer one sees them.

Concurrency is one capability among the rest rather than a privileged subsystem, so the same handle that sandboxes IO sandboxes spawning: a scheduler is just the handler that answers Async, and code with no such handler in scope is sequential by construction. The mechanism is exactly the effect handlers already described (capability effects, effect polymorphism); this section only names the security reading that the rows already justify.

Below, untrusted reads files, but sandbox discharges its FileSystem capability with stub handlers, so it cannot reach the real filesystem however it branches; sandbox stays polymorphic in the other effects e, constraining only the one capability it names.

-- Capability-based sandboxing: a restricted handler set IS a sandbox.
--
-- `untrusted` reads files: it performs the `FileSystem` capability but cannot
-- discharge it itself, so its row demands a handler. `sandbox` runs it under a
-- handler that answers `FileSystem` with stubs (`read_file` returns "<denied>",
-- `file_exists` returns false, `read_bytes` returns no bytes), so the
-- sub-computation never reaches the real filesystem no matter which files it
-- names or how it branches: the only interpreter for those operations in scope
-- is the stub. Authority is exactly the handlers installed, and `sandbox`
-- grants none for the real world. The compiler enforces that the stub set is
-- complete: a handler must implement every operation of the effect it handles,
-- so a capability op added later cannot silently tunnel past the sandbox to a
-- real handler outside it.
--
-- `sandbox` is polymorphic in the fiber's other effects `e` (row-kinded), so it
-- constrains `FileSystem` and lets everything else flow out unchanged. This is
-- object-capability security read straight off the effect row.
--
-- Expected output:
--   sandboxed read: <denied>

fn untrusted() : String ! {FileSystem} =
  if file_exists("/etc/passwd") then
    read_file("/etc/passwd")
  else
    read_file("/etc/secret")

fn sandbox(action : () -> a ! {FileSystem | e}) : a =
  handle action() with
    fs_read_file(path) resume k => k("<denied>")
    fs_read_bytes(path) resume k => k(buf_empty())
    fs_file_exists(path) resume k => k(false)
    return r => r

fn main() = println("sandboxed read: {sandbox(untrusted)}")

7.14 Record and Replay

A program that reads stdin, files, randomness, or the environment takes a different path each time the world answers differently, which is what makes such a run hard to reproduce. Record and replay captures one run as a trace and re-runs it deterministically: an interactive session becomes a fixed regression test, a failing run becomes a reproducible bug report that needs none of the original environment, and a program can be re-executed offline against the captured trace rather than the live world. Persisting that trace to a log as it is produced turns replay into durable execution: the module’s durable handler reloads the logged prefix on restart and continues live once it is exhausted, so a crashed run resumes where it stopped rather than starting over. A suspended computation is likewise a value that can be persisted and resumed after a crash; the next section specifies that runtime boundary.

The Replay stdlib module (import Replay) turns a program’s interaction with the world into a recordable, replayable trace over the capability effects. record(action) runs action against the real world, logging every Console/FileSystem/Random/Env observation into an opaque Trace and returning (result, trace). replay(trace, action) re-runs the same action performing no real input, discharging each operation from the recorded trace instead; a wrong-variant or exhausted trace is a fail() (errors and failure). Replaying a recorded trace reproduces the original result, because the effect-erased core is deterministic and the trace pins every input.

A replayable function annotation, in the family of fip/fbip but orthogonal to them (replayable fn and replayable fip fn are both valid), certifies that a function is reproducible from a recorded trace. It is accepted only when the inferred effect row stays within {Console, FileSystem, Random, Env, Exn, Fail}, the recordable capabilities plus the deterministic builtin effects. A row containing IO (un-logged nondeterminism: output, the system clock, srand) or any user-defined effect is rejected with a caret diagnostic naming the offending effects. The check is a row-subset test on the already-inferred row, so it costs nothing beyond inference.

The two pieces fit together in a few lines: roll is replayable because it reads only Random, and recording one run then replaying its trace reproduces the result without drawing real randomness the second time.

import Replay (..)

-- `roll` reads only the Random capability, so it is `replayable`: its result is
-- reproducible from a recorded trace.
replayable fn roll() = rand() % 6 + rand() % 6 + 2

fn main() =
  -- Record one real run, logging every draw into the trace.
  let pair = record(\(_u) -> roll())
  match pair of
    (recorded, trace) =>
      -- Replay the trace: no real randomness is drawn, yet the result matches.
      let again = replay(trace, \(_u) -> roll())
      if recorded == again then
        println("reproduced")
      else
        println("diverged")

durable(path, action) persists the trace as each observation is made, so a run that stops partway resumes on re-run: the logged prefix replays performing no real input, then the run continues live once the log is exhausted. Re-running this workflow reaches the same result rather than redrawing its inputs.

import Replay (..)

-- A workflow whose every input is logged to the path as it runs. If the program
-- crashes partway, re-running it replays the logged prefix without redoing that
-- work and continues live from where it stopped.
replayable fn workflow() = rand() + rand()

fn main() =
  let total = durable("target/workflow.log", \(_u) -> workflow())
  println("total: {total}")

7.15 Lineage

Record and replay pins a run; lineage explains one. A run recorded with a --lineage sidecar carries, beside the replay trace, a typed account of everything that produced its output, so an artifact can be asked why it exists after the source, inputs, and environment are gone. prism run p.pr --record run.replay --lineage run.plineage -- args writes both: the .replay trace (record and replay) and a .plineage sidecar. --lineage requires --record, because the sidecar names the trace it explains.

The sidecar names the source, Std, and package roots (content-addressed, content-addressed core); the full compiler identity (version, hash scheme, target, backend, optimizer surface, and every behavior-affecting flag); the invocation’s argv; each environment read; each input file by content digest and byte length; any file the run wrote; the stdout digest; and the replay trace digest, recorded as a relation so verification reads the graph rather than a filesystem convention. It records observations of the world, not the world: an input file is named by the hash of the bytes read, never by trusting the file still on disk.²³

Four verbs read a sidecar. Because every fact lives inside it, show and why still answer after the source, inputs, and environment are gone.

The change-one-input workflow reads directly. The program under observation reads one input file and prints one line:

-- Greet whoever name.txt names. The fallback keeps the program runnable
-- before the input file exists, so the same source serves both runs of the
-- change-one-input lineage workflow.
fn main() =
  let name =
    if file_exists("name.txt") then
      read_file("name.txt")
    else
      "ada"
  println("hello {name}")

Record it twice, changing only the input file in between, and ask what moved:

$ printf ada > name.txt
$ prism run greet.pr --record run.replay --lineage run.plineage
hello ada
recorded 4 observations to run.replay and run lineage to run.plineage
$ printf grace > name.txt
$ prism run greet.pr --record run2.replay --lineage run2.plineage
hello grace
recorded 4 observations to run2.replay and run lineage to run2.plineage
$ prism diff run.plineage run2.plineage
lineage diff: 3 moved, 0 added, 0 removed, 5 preserved
  moved    trace: sha256:f8e63490265d... -> sha256:46f3e178a163...
  moved    stdout: stdout:sha256:e27f6e52492b... -> stdout:sha256:9b915ac89684...
  moved    input-file name.txt: input-file:sha256:fdee430d40bd... -> input-file:sha256:e010fd1ce1ac...
  same     request: sha256:4ad56c808cb9...
  same     source-root: prism-core-hash-v1:f8b5f50c4578...
  same     stdlib-root: prism-core-hash-v1:ac8a7aa43202...
  same     compiler: sha256:ab4bbf1853f2...
  same     argv: sha256:5feceb66ffc8...

The source root and compiler identity held; the changed input, the trace it drove, and the stdout it produced all moved. prism lineage verify run.plineage --replay confirms the first run still reproduces exactly, provided its input files are unchanged on disk.

A passed verification can be persisted. prism lineage verify SIDECAR --certify out.cert mints a digest-named certificate over the sidecar it verified, its claim being replay-verified under --replay or lineage-verified otherwise, riding the store’s existing certificate discipline (parity certificates). prism lineage check-cert out.cert SIDECAR checks a certificate against the sidecar it names; a certificate whose subject digest does not match the sidecar is rejected, and a certificate carrying a claim the reader does not recognize is rejected rather than trusted, so no unknown assertion is ever silently honored.

Two further surfaces share the same lineage graph, detailed in the compiler chapter. prism docs writes a manifest of what it documented, and prism docs --verify-manifest rejects a stale page or a drifted root. prism pkg check-world reports per-package gates over a package universe, each gate either passing or honestly marked not-run, and against a baseline names exactly which public definitions changed behavior, by digest.

7.16 Streams

Streams are the prelude’s data-processing combinators, built on a single Emit(a) effect rather than on intermediate collections. A producer performs Emit once per element (srange, sof); a transformer handles a producer’s emissions and re-emits the survivors (smap, skeep, stake); and a consumer handles Emit by folding every emission into a result (sfold, ssum, scollect). A pipeline is the consumer wrapped around the transformers wrapped around the producer, one handler stack over one producer loop.

Because emission is an effect the consumer discharges, a pipeline fuses: srange(1, 1000).smap(square).skeep(even).stake(5).ssum() runs as one loop that allocates neither an intermediate list nor a cell per element, the state-threading path of effect lowering. A transformer that stops early, like stake, drops the producer’s continuation, so the source halts at once. Comprehensions and the statement for desugar to these combinators (comprehensions) and fuse the same way.

The push model above fuses but is single-source: a consumer drives one producer. For the combinators that need to advance two sources in step, zip, interleave, window, the Sequence module (import Sequence as Seq) offers the dual, a pull sequence built on an explicit step co-structure Step(a) = SDone | SMore(a, () -> Step(a)) where a sequence is a thunk the consumer pulls one element at a time. It carries the full combinator vocabulary (map, filter, take, flat_map, zip_with, scan, chunk, and the rest) over a value the caller holds and passes around, which the effect-emission producer, being a running loop rather than a value, cannot be. The two are complementary: reach for the fusing prelude streams when one pipeline consumes one source, and for Sequence when a sequence must be named, stored, or advanced alongside another.

-- Streams as effects: a stream is a producer performing Emit(a), the
-- transformers smap/skeep/stake are handlers that re-emit, and the consumers
-- ssum/scollect/for are handlers that fold. A dot chain nests the handlers over
-- one producer, with no intermediate lists. stake stops the source early by
-- dropping its continuation. Expected output:
--
--   220
--   lo
--   hi
--   0
--   3
--   6

fn square(n) = n * n

fn main() =
  println(srange(1, 1000).smap(square).skeep(even).stake(5).ssum())
  for w in sof(["lo", "hi"]) do
    println((w : String))
  let xs = srange(0, 1000000).smap(\(n) -> n * 3).stake(3).scollect()
  for x in sof(xs) do
    println((x : Int))

7.17 Incremental Computation

The Incr stdlib module (import Incr) is self-adjusting computation as a handler: a program builds a demand graph of source nodes and derivations, and re-reading the graph after a change recomputes only the part a change can reach. input(v) creates a mutable source, get(n) reads a node (recording the read as a dependency of whatever derivation is running), set(n, v) updates a source, and memo(thunk) wraps a derivation whose value is cached and re-demanded rather than recomputed blindly. run_incr(action) discharges the effect, running action as the root observer of a fresh graph; the ambient row of effects the derivations perform flows out unchanged, exactly as run_async passes a fiber’s row through.

The contract that makes it incremental is early cutoff: after a set, re-reading a node re-demands exactly the affected cone, and a derivation whose recomputed value is unchanged does not disturb its dependents. “Unchanged” is an exact content-hash comparison over the serialized value, the same blake3 digest that content-addresses code (content-addressed core), not a user-written equality, so a derivation that recomputes to the same answer halts propagation with no dirty-bit bookkeeping, and a set to a value a source already holds is a no-op.

run_incr_durable(path, tag, action) persists the memo table to a snapshot so a later run warms from it rather than recomputing from scratch. A warm run’s output is byte-identical to a cold one, and a missing, corrupt, or foreign-tagged snapshot silently cold-starts rather than yielding a wrong answer, so the snapshot changes only cost, never result. Because warming a derivation skips its thunk, a durable derivation must be pure up to Fail (a thunk that printed or drew randomness would change the output if skipped), and only the derivations built before the first input-dependent read are warmed.

run_incr_durable_replay(path, tag, action) lifts the purity restriction for the one effect a skipped thunk can still honor: output. It records each memo’s emitted output beside its cached result and replays that output on a warm hit, so a derivation that prints when it fires is warmed from the snapshot without running its thunk yet reproduces the recorded lines byte-for-byte. A second run therefore fires no memo, does no work, and still prints exactly what the first run printed, effects and all, extending the “snapshot changes cost, never result” guarantee to effectful memos rather than only pure ones (the action’s row is ! {Incr, Output, Fail | e}).

7.18 Suspend and Resume

Record and replay reproduces a run from its start; suspend and resume is the stronger checkpoint the previous section points at, a paused computation that is itself a value. prism exec suspend FILE --at N -o snapshot.kont runs a program, pauses it after N machine steps, and writes the whole live continuation, its pending work, its call stack, and every value bound along the way, to a file as a kont envelope. prism exec resume FILE snapshot.kont reads that file and runs the continuation to completion. The suspending run’s output followed by the resuming run’s output is byte-identical to one uninterrupted run: suspend is a cut, not a change, another corollary of the determinism contract. Because a machine step is a pure state transition, a given step count pauses at a deterministic point, so a snapshot is reproducible.

fn count(i, last) =
  if i > last then ()
  else
    println("step {i}: {i} squared is {i * i}")
    count(i + 1, last)

fn main() = count(1, 6)

The recursion is an ordinary tail call carrying i forward; nothing in the program knows it can be interrupted. Where should the cut go? A step count is opaque until the program is laid out on the step clock, which is what prism exec steps does: it runs the program once and prints every observation with the machine step at which it fired. Because a step is a pure state transition, these indices are stable program points, the same on every machine and every run:

$ prism exec steps count.pr
step 1: 1 squared is 1
...
step 6: 6 squared is 36
step  68  Console.print    "step 1: 1 squared is 1"
step  70  Console.newline
step 145  Console.print    "step 2: 2 squared is 4"
step 147  Console.newline
step 222  Console.print    "step 3: 3 squared is 9"
step 224  Console.newline
step 299  Console.print    "step 4: 4 squared is 16"
...
total 482 steps, 12 observations

Pausing after the third line and before the fourth is any budget between steps 224 and 299. Suspend there and the live call (the pending count, the bound i, the frame that will print next) is written to a file; resume it elsewhere and the count continues from where it stopped, the suspend reporting exactly where on the observation timeline the cut fell:

$ prism exec suspend count.pr --at 240 -o half.kont
step 1: 1 squared is 1
step 2: 2 squared is 4
step 3: 3 squared is 9
suspended after 240 steps to half.kont (632 bytes); 6 observation(s) before the cut, last at step 224 (Console.newline)
$ prism exec resume count.pr half.kont
step 4: 4 squared is 16
step 5: 5 squared is 25
step 6: 6 squared is 36

Concatenate the two outputs and you have exactly prism run count.pr. The resuming process never re-ran the first three steps; it decoded the frozen call stack, checked that count.pr still hashes to the bundle the snapshot was captured in, and stepped the machine forward from the cut.

The snapshot is a kont envelope whose header carries the program’s namespace root, the same code identity used by the content-addressed store (the kont envelope). resume re-derives that digest from its own copy of the program and refuses a snapshot whose digest does not match, so a continuation only resumes against the code it was captured in. Hostile or truncated envelopes are rejected with diagnostics rather than trusted; the wire details live in the compiler document.

The suspendable subset is explicit. A value that cannot cross the boundary, a graph nested past the suspendable depth, or a native resource is refused at suspend time naming what could not be written, never encoded into a snapshot that would fail on the far side. The envelope is a runtime-value encoding over the interpreter’s representation, serialized and resumed by the tree-walking interpreter, including that interpreter compiled to WebAssembly, so the browser demo can move a running program between same-origin contexts that already share the same bundle. Native-code suspension is unsupported.

Mobility is therefore a consequence of the same two invariants the rest of the runtime already uses: continuations are reified values, and code identity is content-addressed. Teleporting a computation means sending the kont envelope, not inventing a separate remote-call mechanism: the receiver decodes the suspended continuation, recomputes the namespace root for its local program, and resumes only if that digest matches the envelope. What crosses the wire is the pending computation and captured state; what authorizes it is the hash of the code it was captured in.²⁴

That keeps the mobility story aligned with replay rather than distribution magic. A suspended program resumed by another same-origin context must produce the same suffix as the original uninterrupted run, because the step it resumes from and the code it resumes into are both checked facts. Content addressing names the definitions, the kont envelope names the live continuation over those definitions, and deterministic replay is the observable contract tying them together.

7.19 Arena Allocation

Where @ noalloc (allocation certificates) is the static axis that forbids allocation, the dynamic axis redirects it: allocation is treated as an ordinary handled capability. The standard-library Arena module defines a single-shot Alloc effect and with_arena : (() -> a ! {Alloc}) -> a, which services allocations inside its body from a bump region and reclaims the whole region at scope exit. Choosing an allocator is installing a handler; a program that installs no Alloc handler allocates exactly as before, byte for byte.

fn build(n : Int) : List(Int) =
  with_arena(fn () = range(0, n))

The redirection is scope-directed and invisible except through cost. Only constructors and tuples reachable solely through an arena scope are served from the region; a helper reachable from both arena and ordinary paths stays on the ordinary allocator, preserving byte identity for its non-arena callers. A value may outlive its region: at scope exit any cell reachable from the result is copied into an ordinary reference-counted cell, so escape costs a copy, never a use-after-free. An arena scope is single-shot (a multishot resume across the boundary is refused) and is not replayable, because addresses are not reproducible. @ noalloc still composes: an arena allocation is a fresh cell served differently, not an absent one. The lowering and region runtime are described under arena allocation.

7.20 Adapter Ladders

An effect declaration is a versioned protocol and a handler is one provider for it. When a protocol gains a version, an old client written against the earlier one keeps running against the newer provider through an adapter: a handler that discharges the old operations and re-performs the adjacent new ones. For N versions an author writes the N-1 adjacent adapters and composes them, never a converter for every pair. An adapter is polymorphic in the rest of the row: it removes its source protocol, introduces its target protocol, and forwards the ambient tail e untouched.

(() -> a ! {KvV1 | e}) -> a ! {KvV2 | e}

The relationship is directional. KvV1 -> KvV2 runs a KvV1 computation against a KvV2 provider: it handles KvV1 operations and performs KvV2 ones. The reverse is a separate adapter and may be failable, and the compiler never infers symmetry. Ordinary handler typing already enforces three of the adapter’s obligations. Coverage is handler exhaustiveness: every source operation must be handled unless the adapter is written with partial (residual handlers), so an omitted source operation is the ordinary missing-operation error. Resumption grade is the clause-grade comparison (effects and handlers): a clause may not resume a once source operation more than once, so a grade-changing translation is refused at the clause. Direction is caught wherever the target row is stated: a bridge annotated with the target protocol reports a re-performed source operation as an effect not declared in its annotation.

Two obligations are not derived from the handler’s structure. Ambient preservation holds only by leaving the adapter’s result row to inference; the row-polymorphic result above cannot be written as a declaration annotation, because a declaration effect row must be closed, so an open tail in result position is a parse error. An adapter that adds a clause for an operation outside its source protocol discharges that operation, and that is accepted with no diagnostic. Without a target-row annotation a backwards adapter also type-checks and faults only at run time, on the unhandled source operation. Coverage is likewise not termination: an exhaustive adapter may still loop or perform effects, so an adapter is not total by construction, and a termination claim is the ordinary total or assume total evidence (totality) rather than a protocol-specific spelling.

Recording and replay observe an adapter ladder at one fixed boundary. Record and replay log only the capability vocabulary, never a user protocol operation, so an adapter that translates protocol operations is invisible to a recorder except where a protocol operation bottoms out in a real capability read. That read is performed by the provider, after adaptation, so a recorded trace pins the provider’s post-adaptation vocabulary and not the client’s pre-adaptation one. Translating a historical trace from one protocol version to another is separate work.

The adapter below evolves get from an integer sentinel to an Option: it discharges each KvV1 operation by performing the adjacent KvV2 one and translating the result, forwarding the ambient row untouched. A second KvV2 -> KvV3 rung composes onto it the same way, so a client written once against KvV1 runs against a KvV3 provider by stacking the two adjacent adapters.

effect KvV1
  get_v1(Int) : Int
  put_v1(Int, Int) : Unit

effect KvV2
  get_v2(Int) : Option(Int)
  put_v2(Int, Int) : Unit

fn adapt_v1_to_v2(action : () -> a ! {KvV1 | e}) =
  handle action() with
    get_v1(key) resume k =>
      match get_v2(key) of
        Some(v) => k(v)
        None => k(0 - 1)
    put_v1(key, value) resume k =>
      put_v2(key, value)
      k(())
    return r => r

8. Expressions

The expression grammar is in the surface grammar and the effect and failure forms are in effects and handlers; the forms below are those the grammar alone does not settle.

8.1 Method Calls

A method call e.m(args) is uniform-function-call syntax (UFCS): pure sugar for m(e, args), with the receiver e supplied as the first argument. Prism has no methods, only top-level functions; the dot is notation, not dispatch, so any function reads as a method and calls chain left to right (e.f().g() is g(f(e))). Extra arguments follow the receiver: a.add(b) is add(a, b). A trailing block argument, e.m(args) fn (x) { body }, appends the lambda as the last argument; this is how the stream consumers in streams.pr chain. Field access is e.field, and the two compose, e.field.m(args) being m(e.field, args).

-- Uniform Function Call Syntax (UFCS).
--
-- A method call `e.m(args)` is sugar for `m(e, args)`: the receiver becomes the
-- first argument. Prism has no methods, only functions; the dot is notation, so
-- any function reads as a method and calls chain left to right.
-- Expected output:
--
--   10
--   10
--   8
--   11
--   7
--   3

fn double(n) = n * 2

fn add(a, b) = a + b

type Vec = Vec { x: Int, y: Int }

fn main() =
  -- `e.m(args)` is exactly `m(e, args)`: these two lines are the same call.
  println(double(5))
  println(5.double())
  -- Extra arguments follow the receiver: `a.add(b)` is `add(a, b)`.
  println(5.add(3))
  -- Chaining reads left to right, each result feeding the next call:
  --   5.double().add(1)  ==  add(double(5), 1)
  println(5.double().add(1))
  -- Field access is `e.field`.
  let v = Vec { x = 7, y = 3 }
  println(v.x)
  println(v.y)

Function composition is core to functional programming, and Prism keeps the full algebra: f >> g is the forward composition \x -> g(f(x)), f << g the backward \x -> f(g(x)), and x |> f pipes an already-computed value into a function. Composition binds tighter than the pipe, so x |> f >> g pipes x through the composed pipeline.

The contrast with Haskell is direction, not power. Haskell’s primitive is backward composition (.), and idiomatic Haskell builds the function first and applies it last, reading right to left; pipelining a value forward takes the library operator (&). Prism makes the forward reading the default: dot-chains, |>, and >> all read in dataflow order, left to right, the order in which the value actually moves.

The denotations agree exactly (e.f().g(), e |> f >> g, and (f >> g)(e) are the same program), so the choice among them is prose style: the dot for a value stepping through transformations, |> for a computed result flowing into a pipeline, >>/<< for naming a composed function that is passed around or applied later.

-- Function composition three ways: composed functions are values built with
-- `>>` (forward) and `<<` (backward), a computed value flows on with `|>`,
-- and the UFCS dot chains the same calls in the same left-to-right order.
--
-- Prints:
--   22
--   21
--   22
--   22
--   100

fn inc(x : Int) : Int = x + 1

fn double(x : Int) : Int = x * 2

fn clamp_hundred(x : Int) : Int =
  if x > 100 then
    100
  else
    x

fn main() =
  let up = inc >> double  -- \x -> double(inc(x))
  let down = inc << double  -- \x -> inc(double(x))
  println(show(up(10)))
  println(show(down(10)))
  println(show(10 |> inc |> double))
  let ten = 10
  println(show(ten.inc().double()))
  println(show(200 |> inc >> double >> clamp_hundred))

8.2 Comprehensions

A comprehension [ e for x in s, q, ... ] collects e for each element; a qualifier q is a guard if g or a binder let y = e. A guard is evaluated in a failure context, so an element is pruned both when g is false and when computing g fails: a failable accessor such as at_list (a prelude lookup from the standard prelude) past the end of a list prunes that element rather than aborting. The statement form for x in s, q, ... do body runs body per survivor. Both desugar to the prelude’s stream combinators (the Emit effect of the standard prelude), so they fuse without building an intermediate list.

A guard-free comprehension [ e for x in s ] is exactly a mapped and collected stream, and it desugars to that composition directly, so it rides the fused state-threading tier of effect lowering: no effect-operation cells, about two cells per element (the result list itself), the source evaluated exactly once before iteration, and e evaluated left to right once per element. Qualifiers (guards and binders) keep the general consumer path, whose pruning semantics need the failure context above. The choice of path is a cost decision only; both produce the identical list in the identical order.

-- List comprehensions and qualified for-loops. A comprehension
-- `[ e for x in s, <quals> ]` collects e per element. Qualifiers filter with
-- `if g` and bind with `let y = e`. A guard may be failable: it prunes the
-- element when computing g raises Fail, not only when g returns false. The
-- statement form `for x in s, <quals> do body` runs body per survivor.
-- Expected output:
--
--   1
--   4
--   9
--   16
--   25
--   30
--   40
--   50
--   2
--   4
--   10
--   30

fn main() =
  for sq in sof([x * x for x in srange(1, 6)]) do
    println(sq)
  for y in sof([y for x in srange(1, 6), let y = x * 10, if y > 20]) do
    println(y)
  for x in srange(1, 6),
      if even(x) do
    println(x)
  -- Failable guard: `at_list` fails past the end, so the guard prunes
  -- out-of-range indices just as it prunes the zero price. Keeps 10 and 30.
  let prices = [10, 0, 30]
  for i in srange(0, 6),
      if at_list(prices, i) > 0 do
    println(at_list(prices, i))

8.3 Records

Record construction C { f = e, ... }, functional update C { ..base, f = e }, and nested path update { base | a.b = e, ... } build and modify the record types; each is an in-place write on a uniquely owned value. The deriving (Lens) getters and setters compose with them for deeper access. A path generalizes past nested fields to traversals, indices, prisms, filters, and a read form (optic paths).

-- `deriving (Lens)` synthesizes a getter `<f>_of` and a functional setter
-- `with_<f>` per field. They are ordinary functions, no optic types needed.
-- On a uniquely owned value the setter is FBIP-reused.
--
-- Expected output:
-- 3
-- 7
-- 9
-- 4
type Vec2 = Vec2 { x: Int, y: Int } deriving (Lens)

fn main() : Unit ! {IO} =
  let v = Vec2 { x = 3, y = 4 }
  println(x_of(v))
  let v2 = with_x(v, 7)
  println(x_of(v2))
  let v3 = with_y(with_x(v, 9), 4)
  println(v3.x)
  println(v3.y)

8.4 Imperative control flow

Loops and early exit are surface sugar over tail recursion and effects, so they cost nothing beyond what an explicit recursion would. while cond do body and loop body (an unconditional loop) lower to a tail-recursive driver applied to the condition and body as thunks; because a var is a State effect (the standard prelude) the body mutates freely and the loop runs in constant stack with no per-iteration allocation. break and continue (valid inside while, loop, and for) and statement-form return e (which exits the enclosing function) compile to non-resumable performs of internal, fully-handled control effects, installed only for the keyword a body actually uses; a nested loop captures its own break/continue. Because each control effect is discharged at its loop or function boundary, none appears in the surfaced effect row: a loop is as pure as its body, and a function using return infers the same row as the equivalent recursion. Compound assignment x += e (and -=, *=, %=) on a var is shorthand for x := x <op> e.

Each form desugars to an existing construct:

-- Imperative control flow recovered from effects and tail recursion: `while`,
-- `loop`, `break`, `continue`, early `return`, and compound assignment, all
-- desugaring to the existing core. `var` is a State effect, so loop bodies mutate
-- freely yet each function below stays observably pure `(Int) -> Int`.
fn sum_evens(limit : Int) : Int =
  var total := 0
  var i := 0
  while i < limit do
    i += 1
    if i % 2 == 1 then
      continue
    total += i
  total

fn first_factor(n : Int) : Int =
  var d := 2
  loop
    if d * d > n then
      return n
    if n % d == 0 then
      return d
    d += 1

fn countdown(start : Int) : Int =
  var n := start
  var ticks := 0
  loop
    if n <= 0 then
      break
    n -= 1
    ticks += 1
  ticks

fn main() : Unit ! {IO} =
  println(show_int(sum_evens(10)))
  println(show_int(first_factor(91)))
  println(show_int(first_factor(97)))
  println(show_int(countdown(5)))

8.5 Exponentiation

a ^ b raises a to the power b. It binds tighter than * and than unary minus (-2 ^ 2 is -(2 ^ 2), the mathematical reading; a negative base needs parentheses, (-2) ^ 2), and is right-associative, so 2 ^ 3 ^ 2 is 2 ^ (3 ^ 2). It is the method of the Pow class (the standard prelude) with Int and Float instances, so it desugars to pow(a, b): over Int it is bignum-correct (the instance multiplies), over Float it is a pow_float call. A mixed Int ^ Float is a type error, resolved by an explicit to_float, exactly as 2 + 3.0 is (Prism never coerces between Int and Float implicitly).

An Int exponent may be negative: a ^ b with b < 0 is defined as 1 / a ^ (-b) under the language’s one truncating division rule (integer arithmetic).²⁵ Float exponents follow IEEE pow, so 2.0 ^ -1.0 is 0.5.

8.6 Indexing

a[i] reads, a[i] := v writes, and a[i] += e updates an indexed container. The form is dispatched on the receiver’s type (not a class, so no inference change): Array is indexed by Int, HashMap by String, String by Int (yielding the byte), and List by Int. Array, HashMap, and List are writable; String is read-only. Array and HashMap rewrite the cell in place (FBIP); a List write is the functional list_set, rebuilding the spine.

A read is failable: a missing index or key performs the Fail effect (errors and failure), so a[i] has type Elem ! {Fail} and the partiality surfaces in the row rather than in an Option wrapper. It therefore composes with ??, ?., default, and the rest of the failure axis: a[i] ?? d supplies a default, and the counter idiom is m[k] := (m[k] ?? 0) + 1, honest that an absent key starts at zero. A plain write a[i] := v is total; a[i] += e reads first, so it is ! {Fail}. Writes rebind the underlying var and rewrite the cell in place when it is uniquely owned (FBIP, declarations and programs); nested grid[i][j] := v composes the same way. a[i] := v requires a to be an assignable var.

8.7 Typed Buffers and Tensors

FloatBuf and IntBuf are flat buffers of unboxed 8-byte elements, read and written through the tbuf_* and ibuf_* operations (new, len, get, set, blit). A buffer carries the same ownership discipline as Array: a write mutates it in place when it is uniquely owned and copies it when shared, so mutation is never observable through an alias, and elements thread bit-for-bit identically on both backends (NaN payloads and subnormals included). Data.FlatArray puts one typed surface over both: FlatArray(a) is dispatched by the FlatElem class (instances for Float and I64), so an unsupported element type is a missing-instance error rather than a representation fault. Data.Tensor is a record over FloatBuf carrying per-axis shape, strides, and names: transpose by axis name is a stride permutation that moves no data, reshape is contiguity-checked, and a bracket with two or more indices is multi-index sugar extending indexing: t[i, j] reads and t[i, j] := v writes through the strides. The storage under all of these is flat; only a read boxes the scalar it returns, so element layout stays a cost fact rather than a change in what a program computes.

import Data.Tensor (..)

fn main() =
  var t := from_list([2, 3], [1.0, 2.0, 3.0, 4.0, 5.0, 6.0])
  t[0, 1] := 4.0
  -- Transpose by axis name: a stride permutation, no data movement.
  let u = transpose(t, "0", "1")
  println(u[1, 0])

8.8 SIMD Vectors

F64x2 and I64x2 are opaque baseline 128-bit vectors. Each operation acts on both lanes as one vector operation.