The Prism Language Specification

Prism is a strict, impure functional language in the ML family whose type system tracks side effects. This document defines the surface language: its lexical structure, grammar, type system, and evaluation. It describes the language as the prism compiler accepts it. Where the implementation is incomplete or carries known debt, the limitation is stated as such, not hidden.

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.

Two things distinguish Prism from its ML and Haskell ancestors. Side effects are inferred, extensible effect rows (Section 7) that combine structurally across calls instead of through monads, and they track observability: an operation handled inside a function does not appear in its type, so internally effectful code is reused as pure. The same reference-count discipline both frees memory and performs fully-in-place (FBIP) update (Section 10), 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 Compiler).

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 3 (varid, conid, qualid, integer, float, char, string) and the character classes defined just above. Layout (Section 3.6) 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 of Section 3.6. 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  ->  digit { digit } [ "i64" | "u64" ]
float    ->  digit { digit } "." digit { digit } [ exponent ]
          |  digit { digit } exponent
exponent ->  ( "e" | "E" ) [ "+" | "-" ] 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.


`fn`	`fip`	`fbip`	`pub`	`import`
`as`	`type`	`newtype`	`opaque`	`alias`
`effect`	`error`	`throw`	`try`	`catch`
`transact`	`class`	`instance`	`pattern`	`deriving`
`where`	`given`	`handle`	`with`	`handler`
`mask`	`ctl`	`final`	`fun`	`val`
`return`	`let`	`var`	`borrow`	`in`
`for`	`do`	`if`	`then`	`else`
`elif`	`match`	`of`	`forall`	`true`
`false`	`while`	`loop`	`break`	`continue`
`using`	`canonical`

The built-in type names Int, I64, U64, Bool, Unit, Float, Char, and String are also reserved.

3.3 Operators and Punctuation

The operator set is fixed; the language has no user-defined operators. Every comparison operator, and every arithmetic operator except % and ^, also has a floating-point form suffixed with a dot. Exponentiation ^ is a single operator over both Int and Float (Section 8.4).

Class	Operators
Arithmetic	`+` `-` `` `/` `%` `^` and float `+.` `-.` `.` `/.`
Comparison	`==` `/=` `<` `<=` `>` `>=` and float `==.` `/=.` `<.` `<=.` `>.` `>=.`
Logical	`&&` `\|\|`
Pipeline	`\|>` `>>` `<<`
Failure	`??` `?.` `?`
Arrows	`->` `<-` `=>`
Binding	`=` `:=` `:` and compound `+=` `-=` `*=` `%=`
Effect	`!`
Brackets	`(` `)` `{` `}` `[` `]`
Other	`,` `.` `..` `\|` `\`

3.4 Literals

An integer is a sequence of decimal digits. 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. A char is a single Unicode scalar in single quotes. A string is double-quoted UTF-8.

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 Show value is spliced into the string. 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 in Section 7.5 use interpolation, as in "no such key: {k}".

3.6 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). 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 and may always be used in place of an implicit block, as in the brace-delimited handler arms of the masking example (Section 7.3).

4. Surface Grammar

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

program   ->  { topdecl }                       -- separated by layout

topdecl   ->  [ "pub" | "opaque" ] item
item      ->  import | datatype | newtype | synonym | rowalias
           |  classdecl | instancedecl | canonicaldecl | effectdecl
           |  errordecl | patterndecl | constdecl | fundecl

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

datatype  ->  "type" conid [ tyvars ] "=" ctor { "|" ctor } [ deriving ]
newtype   ->  "newtype" conid [ tyvars ] "=" ctor [ deriving ]
synonym   ->  "alias" conid [ tyvars ] "=" type
rowalias  ->  "alias" conid "=" "{" [ label , ... ] "}"
tyvars    ->  "(" varid , ... ")"
ctor      ->  conid [ "(" type , ... ")" ]
           |  conid "{" field , ... "}"
field     ->  varid ":" type
deriving  ->  "deriving" "(" conid , ... ")"

constdecl ->  "let" varid [ ":" type ] "=" expr
fundecl   ->  [ "fip" | "fbip" ] "fn" varid "(" [ param , ... ] ")"
                [ retann ] [ given ] "=" expr [ wheres ]
param     ->  [ "borrow" ] varid [ ":" type ] [ ":=" expr ]
retann    ->  ":" "!" "{" [ label , ... ] "}" type
           |  ":" "!" type
           |  ":" type
given     ->  "given" constraint , ...
constraint -> conid "(" type ")"
wheres    ->  "where" "{" { varid "=" expr } "}"

classdecl    ->  "class" conid "(" varid ")" [ given ] "{" sig , ... "}"
instancedecl ->  "instance" varid ":" conid "(" type ")" [ given ]
                   "{" fundecl , ... "}"
canonicaldecl -> "canonical" conid "(" type ")" "=" varid
sig          ->  varid ":" type

effectdecl   ->  "effect" conid [ tyvars ] "{" effop , ... "}"
effop        ->  "ctl" varid "(" [ type , ... ] ")" ":" type
errordecl    ->  "error" conid [ "(" type , ... ")" ]

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

Type syntax. A function type carries an optional effect row on its codomain (Section 7); 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
         |  atype "->" arrow                     -- single domain
         |  atype
atype   ->  scalar
         |  "[" type "]"                          -- List(type)
         |  conid [ "(" type , ... ")" ]          -- type constructor
         |  varid [ "(" type , ... ")" ]          -- variable, possibly applied
         |  "(" type ")"
         |  "(" type "," type , ... ")"           -- tuple
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 Section 7).

expr    ->  "if" expr "then" expr { "elif" expr "then" expr } "else" expr
         |  "let" pattern "=" expr  expr            -- bind, then continue
         |  "var" varid ":=" expr  expr             -- local mutable, then continue
         |  "\\" "(" [ varid , ... ] ")" "->" expr  -- lambda
         |  "match" expr "of" { arm }
         |  "handle" expr "with" handler
         |  "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
         |  "return" expr                             -- early return
         |  varid ":=" expr                          -- assignment
         |  varid ( "+=" | "-=" | "*=" | "%=" ) expr  -- compound assignment
         |  opexpr

opexpr  ->  opexpr binop opexpr                      -- binop and binding per 4.1
         |  appexpr
appexpr ->  appexpr "(" [ expr , ... ] [ "using" iname , ... ] ")"
                                                     -- application; `using` selects instances
         |  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 | 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     ->  varid { "." varid }                     -- a nested field path
binop    ->  "??" | "|>" | ">>" | "<<" | "||" | "&&" -- binding given in 4.1
         |  "==" | "/=" | "<" | "<=" | ">" | ">="
         |  "+" | "-" | "*" | "/" | "%" | "^"
         |  "==." | "/=." | "<." | "<=." | ">." | ">=."
         |  "+." | "-." | "*." | "/."

pattern  ->  conid [ "(" pattern , ... ")" ]        -- constructor
          |  conid "{" fieldpat , ... "}"            -- record, ".." allowed
          |  varid                                    -- variable binding
          |  "_"                                      -- wildcard
          |  integer | float | char | "true" | "false"
          |  "[" [ pattern , ... ] "]"                -- list
          |  "(" pattern "," pattern , ... ")"        -- tuple
fieldpat ->  varid "=" pattern  |  ".."

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

hclause   ->  "return" varid "=>" expr                 -- result transform
           |  varid "(" [ varid , ... ] "," varid ")" "=>" expr  -- op, last arg is 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 application, field access, and the postfix failure operators, which bind tighter than every binop.

Level	Operators	Associativity
1	`??`	right
2	`\|>`	left
3	`>>` `<<`	left
4	`\|\|`	left
5	`&&`	left
6	`==` `/=` `<` `<=` `>` `>=` (and float forms)	none
7	`+` `-` (and float forms)	left
8	`` `/` `%`, and float `.` `/.`	left
9	`^`	right
10	`f(...)` `a[i]` `.field` `?.field` `?`	left

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 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.2 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 Section 6. There is no explicit kind-checking phase: well-kindedness is enforced during unification, which requires a constructor and its arguments to agree in arity.

5.3 Inference, Generalization, and Defaulting

A row is built from labels, the effect names of Section 7 (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. 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 (Section 12).

5.4 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 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.

5.5 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 operations are named builtins, not operators, since the surface +, -, and so on target Int and Float. Each takes two operands of the lane type.

Family	Operations (and the `u64_*` counterparts)
Arithmetic	`i64_add` `i64_sub` `i64_mul` `i64_div` `i64_rem` `i64_cmp`
Bitwise	`i64_and` `i64_or` `i64_xor`
Shift	`i64_shl` `i64_shr`

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.6 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 (Section 9) destructures a value by constructor. A type may take type parameters and may be recursive, including mutually so.

-- 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. A deriving (C, ...) clause generates the named instances structurally (Section 6); Eq, Ord, Show, and Lens are derivable.

5.7 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 expressions of Section 8.2. 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)

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 constrained function receives its dictionaries as hidden arguments resolved at each call site. The following program declares a second Ord(Int) instance named ordDesc that reverses the ordering, designates the prelude’s ascending ordInt as canonical, and selects each explicitly.

-- Typeclasses with Lean-style named instances. A class declares a dictionary
-- shape, instances are named values, and constrained functions take hidden
-- dictionaries resolved at the call site. When a head has two instances one is
-- canonical (here the prelude's ascending ordInt, designated below); implicit
-- resolution picks it, and the other is selected explicitly with
-- f(args, using instName). Coherence: resolution is never silently ambiguous.

fn maximum_by_ord(xs : List(a)) : Option(a) given Ord(a) =
  match xs of
    Nil => None
    Cons(x, rest) =>
      match maximum_by_ord(rest) of
        None => Some(x)
        Some(y) =>
          if cmp(x, y) >= 0 then
            Some(x)
          else
            Some(y)

instance ordDesc : Ord(Int) {
  fn cmp(x, y) = int_cmp(y, x)
}

-- The prelude's ascending ordInt is the canonical Ord(Int); ordDesc stays the
-- explicit yardstick. Without this, two Ord(Int) instances would be a coherence
-- error at definition rather than a silent ambiguity at the use site.
canonical Ord(Int) = ordInt

fn join_shown(xs : List(a)) : String given Show(a) =
  match xs of
    Nil => ""
    Cons(x, rest) =>
      match rest of
        Nil => show_c(x)
        Cons(_, _) => concat(show_c(x), concat(", ", join_shown(rest)))

fn main() : !{IO} Unit =
  let xs = [3, 1, 4, 1, 5, 9, 2, 6]
  println(join_shown(sort_by_ord(xs, using ordInt)))
  println(join_shown(sort_by_ord(xs, using ordDesc)))
  println(unwrap_or(0, maximum_by_ord(xs, using ordInt)))
  println(unwrap_or(0, maximum_by_ord(xs, using ordDesc)))
  println(join_shown(sort_by_ord(["pear", "apple", "quince"])))

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

Two instances for one head with no 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.

6.2 Superclasses

A class may require another as a superclass with given. Each instance then stores a resolved superclass dictionary as the leading field of its dictionary cell, and a given Ord(a) constraint discharges an Eq(a) obligation by projecting that field. The superclass witness is found automatically from the instances in scope.

-- Superclasses: a class may declare another class as a superclass with
-- `given`. Every instance then carries a resolved superclass dictionary, stored
-- as a leading field of its dict cell, and a `given Ord2(a)` constraint can
-- discharge an `Eq2(a)` obligation by projecting that field. The superclass
-- witness is found automatically from the instances in scope, so the instance
-- declaration does not repeat it.
--
-- Prints:
--   equal
--   less
--   greater

class Eq2(a) {
  eq2 : (a, a) -> Bool
}

class Ord2(a) given Eq2(a) {
  cmp2 : (a, a) -> Int
}

instance eqInt2 : Eq2(Int) {
  fn eq2(x, y) = x == y
}

instance ordInt2 : Ord2(Int) {
  fn cmp2(x, y) = if x < y then 0 - 1 elif x > y then 1 else 0
}

-- Polymorphic over any Ord2(a). It calls cmp2 (its own method, taken from the
-- Ord2 dictionary parameter) AND eq2 (a superclass method, projected out of the
-- same dictionary). No Eq2 constraint is written: Ord2 entails it.
fn describe(x : a, y : a) : String given Ord2(a) =
  if eq2(x, y) then
    "equal"
  elif cmp2(x, y) < 0 then
    "less"
  else
    "greater"

fn main() : !{IO} Unit =
  println(describe(3, 3))
  println(describe(3, 5))
  println(describe(7, 2))

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. Its methods are effect-polymorphic (defined in Section 7.6): a per-element effect row threads through in place of an Applicative wrapper, so effectful traversal needs no monad and no do-notation.

-- Higher-kinded type classes over the language's own data types: 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]

fn main() : !{IO} Unit =
  -- Functor: map over either container with one `fmap`.
  println(show(fmap(\(x) -> x + 1, [1, 2, 3])))
  println(show(fmap(\(x) -> x * 2, Some(21))))
  -- Foldable: an effect-polymorphic right fold.
  println(show(fold_r(\(x, acc) -> x + acc, 0, [1, 2, 3, 4])))
  -- Applicative: `ap` is cartesian on List, positional on Option.
  println(show(ap([\(x) -> x + 1, \(x) -> x * 10], [1, 2])))
  println(show(ap(Some(\(x) -> x + 5), Some(10))))
  -- Monad: structural `bind` (List is nondeterminism, Option is failure).
  println(show(bind([1, 2, 3], \(x) -> [x, x])))
  println(show(bind(Some(3), \(x) -> Some(x * x))))
  -- Traversable: effectful map (here the effect is none).
  println(show(traverse(\(x) -> x * 10, [1, 2, 3])))

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

7. Effects and Handlers

An effect declares a set of operations; each ctl 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.

effect State {
  ctl get(Unit) : Int,
  ctl put(Int) : Unit
}

-- Algebraic State, the Koka way.
--
-- 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() : !{State} Int =
  let n = get(())
  put(n + 1)
  n

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

fn run_counter(init) =
  let f =
    handle counter() with
      get(u, k) => \(s) -> k(s)(s)
      put(s2, 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 Section 4. 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 (Section 7.1) and a final ctl clause abort.

7.1 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 {
  ctl 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) : !{Exn} Int =
  if d == 0 then
    raise(0 - 1)
  else
    n / d

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

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

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

7.2 Clause Sugar

Two clause forms abbreviate common shapes. fun op(x) => e is tail-resumptive sugar for op(x, 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.

-- Koka-style fun and val handler clauses, pure desugaring sugar.
--
-- `fun 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 {
  ctl name() : String,
  ctl tag() : Int,
  ctl width(Int) : Int,
  ctl log(String) : Unit
}

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

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

fn main() = println(run_app())

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

7.3 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.

-- Koka-style 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 {
  ctl ask() : Int
}

-- inner answers 2, outer 10. ask() + mask<Ask>(ask()) = 2 + 10 = 12
fn shadowed() =
  handle (handle ask() + mask<Ask>(ask()) with {
      ask(k) => k(2),
      return r => r
    }) with
    ask(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(k) => k(1),
      return r => r
    } with {
      ask(k) => k(100),
      return r => r
    }) with
    ask(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(k) => k(ask()),
      return r => r
    }) with
    ask(k) => k(3)
    return r => r

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

7.4 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 (Section 7.1), 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))

-- Conceptual desugaring. Each `var` becomes a private two-operation effect
-- (a get and a set), and a handler that threads the value is wrapped around the
-- body in the same pass. Reads become `do get_*`, assignments `do set_*`.
fn fib_iter(n) =
  handle
    do set_a(0)
    do set_b(1)
    repeat(n) fn
      let t = do get_a() + do get_b()
      do set_a(do get_b())
      do set_b(t)
    do get_a()
  with
    get_a(u, k) => \(s) -> k(s)(s)     -- resume with s; state unchanged
    set_a(v, k) => \(s) -> k(())(v)    -- resume with (); new state is v
    return r    => \(s) -> r           -- discard final state; return the answer
  -- a second, identical handler for `b` wraps this one (elided)

-- After effect lowering. The escape analysis proved the var never leaves its
-- block, so lowering erases the State handler to a mutable cell: each `get` is a
-- cell read and each `set` a cell write. The loop is a self tail call, so it
-- lowers to a constant-stack loop with no per-iteration allocation. The get/set
-- effect is gone, leaving code equivalent to the threaded-argument loop below.
fn fib_iter(n) = loop(n, 0, 1)            -- (count, a, b) as plain arguments

fn loop(n, a, b) =
  if n == 0 then a
  else loop(n - 1, b, a + b)

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.5 Errors and Failure

Prism has no built-in exception type. Errors and failure are two related mechanisms, both resting on the non-resumable final ctl clause of Section 7.2.

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 final ctl 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 `final ctl` 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) : !{NotFound, Malformed} Int =
  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"))

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 Section 8; a plain match on Ok/Err; and a custom non-resumable effect.

-- Exceptions tour, four idioms from fatal to fully recoverable.
--
-- 1. Built-in Exn row: `error(code)` aborts the process, uncatchable. Any
--    caller carries `!{Exn}`. checked_div sees only safe input here.
-- 2. `?` propagation over Result: `half(n)?` unwraps Ok and short-circuits
--    the chain on the first Err. report matches the outcome at the boundary.
-- 3. Recovery is a plain match on Ok/Err (or result_or for a default).
-- 4. Custom exception effect via a `final ctl` clause: abort never resumes,
--    the continuation is discarded, and the clause's value becomes the
--    result. Cheap throws, no Result plumbing in the throwing code.
--
-- Expected output:
--   42
--   3
--   odd
--   3
--   0
--   pass
--   fail
--   invalid: negative
--   invalid: too big

fn checked_div(n, d) : !{Exn} Int =
  if d == 0 then
    error(1)
  else
    n / d

fn half(n) =
  if even(n) then
    Ok(n / 2)
  else
    Err("odd")

fn quarter(n) =
  let h = half(n)?
  let q = half(h)?
  Ok(q)

fn report(r) =
  match r of
    Ok(v) => println(v)
    Err(e) => println(e)

fn quarter_or_zero(n) =
  match quarter(n) of
    Ok(v) => v
    Err(_) => 0

effect Abort {
  ctl abort(String) : Unit
}

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

fn safe_grade(n) =
  handle grade(n) with
    final ctl abort(msg) => concat("invalid: ", msg)
    return r => r

fn main() =
  println(checked_div(84, 2))
  report(quarter(12))
  report(quarter(6))
  println(quarter_or_zero(12))
  println(quarter_or_zero(6))
  println(safe_grade(72))
  println(safe_grade(40))
  println(safe_grade(0 - 5))
  println(safe_grade(200))

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 (Section 8). 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 final ctl 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)

7.6 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 (Section 6.3), so an effectful traversal needs no Applicative wrapper.

effect Tick {
  ctl tick(Unit) : Int
}

effect Say {
  ctl 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(u, 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, k) =>
      println(m)
      k(())
    return r => r

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

8. Expressions

The expression grammar is in Section 4 and the effect and failure forms are in Section 7; the forms below are those the grammar alone does not settle.

A method call e.m(args) is uniform-function-call sugar for m(e, args). A trailing block argument, e.m(args) fn (x) { body }, appends a lambda as the last argument; this is how the stream consumers in streams.pr chain. Field access is e.field.

8.1 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, Section 12) 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 Section 12), so they fuse without building an intermediate list.

-- 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.2 Records

Record construction C { f = e, ... }, functional update C { ..base, f = e }, and nested path update { base | a.b = e, ... } build and modify the records of Section 5.7; 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 (Section 8.6).

-- `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() : !{IO} Unit =
  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.3 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 (Section 12) 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:

Surface	Desugaring
`x += e` (and `-=`, `*=`, `%=`)	`x := x <op> e`
`while cond do body`	`repeat_while(\() -> cond, \() -> body)`
`loop body` (reachable `break`)	`repeat_while(\() -> true, \() -> body)`
`loop body` (no `break`)	`forever(\() -> body)`, whose result is a bottom type
`break` / `continue`	a `final ctl` perform of an internal `Break`/`Continue` effect handled at the loop
`return e`	a `final ctl` perform of an internal `Return(a)` effect handled at the function body

-- 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() : !{IO} Unit =
  println(show_int(sum_evens(10)))
  println(show_int(first_factor(91)))
  println(show_int(first_factor(97)))
  println(show_int(countdown(5)))

8.4 Exponentiation

a ^ b raises a to the power b. It binds tighter than * and is right-associative, so 2 ^ 3 ^ 2 is 2 ^ (3 ^ 2). It is the method of the Pow class (Section 12) 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).

8.5 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 (Section 7.5), 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, Section 10); nested grid[i][j] := v composes the same way. a[i] := v requires a to be an assignable var.

8.6 Optic Paths

Prism has no optic library: no Lens type, no over/set/toListOf to compose, no profunctor encodings. It has one rule instead. Between the | and the operator of a record update (Section 8.2), or inside s.[ ... ], a path is a sequence of steps read left to right. The path is the optic, spelled at the use site rather than reified as a value. Every form is sugar over map/with/match, so in-place reuse and fusion come for free and nothing new reaches the core: this is the language’s “effects instead of monads” stance applied to optics, paths instead of optic combinators.

A step is one of:

Step	Meaning
`.field`	descend into a record field
`each`	traverse every element of a functor (lowers to `fmap`)
`[i]`	focus one element of a list or array, by index
`?Ctor`	focus through a sum constructor; others pass through
`(steps where p)`	keep only the foci satisfying the predicate `p`

End a path with = v to set the focus or ~ f to modify it (apply f); wrap a path in s.[ path ] to read every focus it selects into a list. each is a reserved keyword; the other steps reuse existing tokens.

Each form lowers to ordinary code, shown here over type Player = Player { name: String, pos: Vec2, hp: Int, bag: List(Int) } and type Shape = Circle { radius: Int } | Square { side: Int }. A field sets through the derived setter, { p | hp = 100 } to with_hp(p, 100), and nests, { pl | pos.x = 30 } to with_pos(pl, with_x(pl.pos, 30)). Modify reads the focus, { p | hp ~ heal } to with_hp(p, heal(p.hp)). each fans out over any functor, { players | each.hp ~ heal } to fmap(\p -> with_hp(p, heal(p.hp)), players), and composes with descent, { world | party.each.pos.x = 0 }. An index focuses one element, { world | party[0].hp = 100 }, lowering through list_set (or in-place array_set); an out-of-range index leaves the container unchanged. A prism rebuilds a matched constructor and passes the others through, the prism law for update:

{ shape | ?Circle.radius ~ double }
  =>  match shape of
        Circle { radius = r } => Circle { radius = double(r) }
        other                 => other

A filter guards a traversal, { world | party.(each where alive).hp ~ heal } applying the rest only to the foci alive keeps and passing the rest through. The whole vocabulary composes in one path:

{ world | party.(each where alive).bag.each.count ~ \(n) -> n + 5 }
  =>  with_party(world,
        fmap(\p -> if alive(p)
                   then with_bag(p, fmap(\it -> with_count(it, it.count + 5), p.bag))
                   else p,
             world.party))

The read form s.[ path ] collects every focus a path selects into a list, the read twin of the update: players.[each.hp] is the list of each hp, each flat-maps so world.[party.each.bag.each.count] flattens, ?Ctor previews zero or one focus, and a single-focus path yields a one-element list.

Paths are deliberately use-site syntax, not first-class values: there is no Optic type, no passing an optic to a function, no library of named composable optics, and optic kinds are not tracked in the type system (that a read-only path is read-only is a structural fact of the desugaring, not a typed law). This is the explicit trade: paths cover the great majority of real optic use and give up abstracting over which optic. The mental model is one breath: steps read left to right, = v/~ f to write, s.[ ... ] to read, nothing escaping into a new core construct.

-- A tour of optics by path. A path is a sequence of steps between `|` and the
-- operator (or inside `s.[ ... ]`): `.field` descends, `each` traverses a
-- functor, `[i]` indexes, `?Ctor` focuses a constructor, `(each where p)`
-- filters. End with `= v` to set or `~ f` to modify; wrap in `s.[ path ]` to
-- read every focus into a list. Every form is sugar over `map`/`with`/`match`,
-- so in-place reuse and fusion come for free; nothing reaches a new core form.
--
-- Expected output:
--   Vec2(1, 4)
--   Player(hero, Vec2(7, 4), 30, [])
--   [Player(a, Vec2(0, 0), 15, []), Player(b, Vec2(0, 0), 10, [])]
--   World([Player(a, Vec2(1, 2), 100, []), Player(b, Vec2(1, 2), 0, [])], 1)
--   Circle(20)
--   Square(3)
--   [Player(a, Vec2(1, 2), 15, []), Player(b, Vec2(1, 2), 0, [])]
--   [5, 0]
--   [5]

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

type Player = Player { name: String, pos: Vec2, hp: Int, bag: List(Int) }

type World = World { party: List(Player), turn: Int }

type Shape = Circle { radius: Int } | Square { side: Int }

fn alive(p : Player) : Bool = p.hp > 0

fn heal(h : Int) : Int = h + 10

fn mk(n : String, h : Int) : Player =
  Player { name = n, pos = Vec2 { x = 1, y = 2 }, hp = h, bag = Nil }

fn main() =
  -- Set and modify a (possibly nested) field.
  let v = Vec2 { x = 3, y = 4 }
  println({ v | x ~ \(n) -> n - 2 })
  let hero = Player { name = "hero", pos = v, hp = 20, bag = Nil }
  println({ hero | pos.x = 7, hp ~ heal })
  -- Traverse with `each`, then descend; modify and set per element.
  let party = Cons(mk("a", 5), Cons(mk("b", 0), Nil))
  println({ party | each.hp ~ heal, each.pos = Vec2 { x = 0, y = 0 } })
  -- A field, an index, then a field, mixed with a plain field.
  let world = World { party = party, turn = 1 }
  println({ world | party[0].hp = 100 })
  -- A prism focuses one constructor and passes the others through.
  println({ Circle { radius = 10 } | ?Circle.radius ~ \(r) -> r * 2 })
  println({ Square { side = 3 } | ?Circle.radius = 0 })
  -- Filter a traversal: only the living are healed.
  println({ party | (each where alive).hp ~ heal })
  -- Read every focus a path selects into a list.
  println(party.[each.hp])
  println(party.[(each where alive).hp])

9. Patterns

Patterns appear in match arms, let bindings, lambda and function parameters, and catch arms; their grammar is the pattern nonterminal of Section 4. A constructor pattern destructures a value of the algebraic data type that built it (Section 5.6), binding its fields; literal, tuple, wildcard, and record patterns match the remaining forms.

A match arm may carry a guard, pat if cond => body; when the guard is false, control falls through to the next arm. Matches are checked for exhaustiveness and redundancy by the usefulness algorithm of Maranget (2007): an unreachable arm is an error, and a non-exhaustive match is an error naming a missing pattern. A guarded arm does not count toward exhaustiveness, since its guard may fail at run time.

-- Pattern guards: `pat if cond => body`. The guard sees the pattern's
-- variables; when it is false the value falls through to the next arm.
-- Coverage counts only unguarded arms toward exhaustiveness, so a match
-- covered solely by guarded arms is rejected at compile time.

-- The classic: literal-free fizzbuzz, first true guard wins.
fn fizzbuzz(n : Int) : String =
  match n of
    k if k % 15 == 0 => "FizzBuzz"
    k if k % 3 == 0 => "Fizz"
    k if k % 5 == 0 => "Buzz"
    k => show(k)

-- Guarded insertion keeps the list sorted. The catchall handles both Nil and
-- the spot where x belongs.
fn insert(x : Int, xs : List(Int)) : List(Int) =
  match xs of
    Cons(h, t) if h < x => Cons(h, insert(x, t))
    _ => Cons(x, xs)

fn isort(xs : List(Int)) : List(Int) = foldr(insert, [], xs)

-- Expected output:
--   1 2 Fizz 4 Buzz Fizz 7 8 Fizz Buzz 11 Fizz 13 14 FizzBuzz
--   [1, 2, 5, 7, 9]
fn main() =
  println(str_join(" ", map(fizzbuzz, range(1, 16))))
  println(show(isort([5, 2, 9, 1, 7])))

A pattern N(x) for T = view ... make ... declaration defines a bidirectional pattern synonym: in match position it runs view and succeeds when that returns Some (the present case of Option, Section 12); in expression position it runs make. Here view and make are contextual keywords, significant only inside a pattern declaration. A synonym with both halves is a prism (a composable view-and-build pair); one with only view is a view pattern.

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

-- a bidirectional pattern synonym: matches when y == 0, binding x
pattern OnXAxis(x) for Vec2 =
  view \(v) -> if v.y == 0 then Some(v.x) else None
  make \(x) -> Vec2 { x = x, y = 0 }

fn describe(v) =
  match v of
    OnXAxis(x) => x
    _ => 0 - 1

fn main() =
  println(describe(Vec2 { x = 5, y = 0 }))
  println(describe(Vec2 { x = 5, y = 3 }))

10. Declarations and Programs

A function is declared with fn; a parameter may carry a type annotation, a default value := e, or the borrow modifier, which lets a pure function read a parameter without taking ownership of it. A return annotation is written : !{R} T for result type T and effect row R, : ! T for an explicit empty row, or : T to leave the row inferred. A parameter with a default may be omitted, and any argument may be passed by name as f(p = e); the call is rewritten to positional form, filling omitted defaults. Defaults and named arguments are honored on top-level functions. A top-level let is a constant: its references are inlined. A where block attaches non-recursive, lexically scoped definitions to a function body.

A function may be annotated fip or fbip to assert the fully-in-place discipline of Lorenzen et al. (2023). fbip proves the body allocates no fresh cell and calls only annotated, allocation-free functions. fip additionally proves linearity (each owned, non-immediate binding is consumed at most once) and bounded stack (each recursive call in the group is a tail call or a single tail-modulo-cons or tail-modulo-add). These are static checks that reject a non-conforming body; the mechanism is described in Compiler.

-- FP^2 in-place list operations (Lorenzen/Leijen/Swierstra, ICFP 2023),
-- statically checked. The annotation makes the compiler PROVE the function
-- allocates no fresh cell: every `Cons` it builds reuses one it just matched and
-- dropped. Run with PRISM_REUSE_STATS=1 to watch the reuse hits, or
-- PRISM_CHECK_LEAKS=1 to confirm zero live cells at exit.
--
-- `rev_onto` and `bump` are `fip`: linear (each binding used once) AND bounded
-- stack. `rev_onto` is a plain tail call and `bump` is a tail-modulo-constructor
-- (`Cons(.., bump(t))`), so both lower to a constant-stack loop, not recursion.
-- `cap_at` is only `fbip`: its `h` is read by the guard AND rebuilt into the
-- `Cons`, two uses of one value, so it is not linear (its element type is generic
-- `a`, so `h` cannot be assumed an immediate). Zero-allocation still holds.
--
-- Prints:
--   10
--   6
--   22

-- Reverse onto an accumulator, the canonical fip. Each input `Cons` is matched,
-- freed, and immediately reused as the next accumulator cell, so the reversal
-- runs in place with zero allocation, and the tail call makes it a loop.
fip fn rev_onto(xs, acc) =
  match xs of
    Nil => acc
    Cons(h, t) => rev_onto(t, Cons(h, acc))

-- The seeding wrapper is not fbip: that initial `Nil` is a genuine fresh
-- allocation with no cell to reuse, so it stays un-annotated.
fn reverse_ip(xs) = rev_onto(xs, Nil)

-- Spine-rebuilding map: drop each `Cons`, rebuild it around the bumped head.
fip fn bump(xs) =
  match xs of
    Nil => Nil
    Cons(h, t) => Cons(h + 1, bump(t))

-- Saturating transform: rebuild every cell, head chosen by a test. Both `if`
-- branches end in a `Cons` reusing the same freed cell, so the reuse credit is
-- spent exactly once on every path. (A `filter` that DROPS cells could not be
-- fbip: the discard path frees a cell with no local allocation to reuse, and
-- this runtime has no cross-call reuse credit, so it would allocate.)
fbip fn cap_at(xs) =
  match xs of
    Nil => Nil
    Cons(h, t) =>
      if h > 9 then
        Cons(9, cap_at(t))
      else
        Cons(h, cap_at(t))

fn main() =
  println(sum(reverse_ip([1, 2, 3, 4])))
  println(sum(bump([1, 1, 1])))
  println(sum(cap_at([1, 20, 3, 40])))

11. Modules

A file is a module and a directory is a namespace prefix: import Data.Map loads Data/Map.pr. A project is a prism.toml manifest plus a source tree, resolved from the project root. A single-file program is one module.

import M brings M’s exports into scope under qualified names; import M (a, b) also brings a and b into bare scope; import M as N adds the alias N. The pub modifier on a declaration makes it visible to importers; pub import M (x) re-exports x through the importing module. An opaque type exports its name but not its constructors.

Name resolution rewrites every top-level definition to a canonical, module-qualified symbol (an export as Data.Map.insert, a private as the unforgeable, source-unwritable Data.Map@helper) and merges all modules into one program keyed by those symbols. Because identity is the canonical symbol, two modules may export the same short name and coexist. This is namespacing, not separate compilation: there are no per-module artifacts, and changing one module recompiles the whole program.

Instances are global, but each records its defining module. An orphan instance (defined apart from both its class and its head type) and instances that overlap across modules are reported as warnings; an ambiguity names each candidate’s module.

12. The Standard Prelude

The prelude in lib/prelude.pr is in scope in every module. It is ordinary Prism, not built-in. Its contents, by category:

Data types. Option(a), Result(a, e), List(a), the balanced-tree Map(k, v), and the hash table HashMap(v). A set is a Map(k, Unit), with a set_* API rather than a distinct type.
List combinators. map, filter, foldl, foldr, length, append, reverse, zip/unzip, take/drop, sort, range, and the rest of the usual vocabulary.
Option and Result combinators. map_option, and_then, unwrap_or, map_result, and_then_result, result_or, and conversions between the two.
The class tower. Eq, Ord (with Eq as superclass), Show, Pow (exponentiation ^, with Int and Float instances), and the higher-kinded Functor, Applicative, Monad, Foldable, Traversable, with instances for List and Option.
Strings and characters. Classifiers (is_digit, is_alpha, …), case mapping, starts_with/ends_with/contains/index_of, split, trim, chars, and single-allocation joining.
Arrays and maps. The growable Array(a) API (array_new, array_get, array_set, array_push, with in-place update on unique ownership), the AVL Map and set_* API, and the HashMap API over string keys.
Streams. The Emit(a) effect and the producer/transformer/consumer combinators srange, sof, smap, skeep, stake, sfold, ssum, scollect, which fuse without intermediate collections.
Numerics and failure. Fixed-width i64_*/u64_* operations, common math, and the failure helpers guard, optional, succeeds, default.

Keyboard shortcuts

Prism