Yon, Syntax Reference

This is the normative reference for Yon 1.0. Every form below was re-verified against the real grammar (frontend/parser.mly and frontend/lexer.mll) and the compiling examples under regression/book/jp/*/Entry.yon, not from memory, not from older documents. Where a construct could not be confirmed in the live grammar it has been removed or flagged, rather than asserted.

This table answers is this form valid? For what does this keyword mean?, with a compiling example next to each explanation, see Keywords, one by one. Every keyword, alphabetically:

absent · adjunction · aggregates · algebra · along · and · as · at · back · backward · be · bi · by · carry · cell · comp · compose · converts · do · drop · each · effects · El · el_match · else · emit · error · every · exact · false · fold · for · forces · forever · forward · from · fst · fun · functor · functorial · geomorph · hcomp · here · heyting · hit · hit_elim · holds · I0 · I1 · Id · if · import · in · ind_path · induct · internal · invertible · is · iter · law · lawful · list · map · maps · match · morph · morphism · morphisms · most · move · multishot · nat · new · not · of · operation · or · otherwise · over · pair · parallel · partial · PathP · Pi · place · plainly · plam · present · produce · promote · prop · pull · pullback · push · pushout · quote · reduction · refl · repeat · requires · resolves · return · Same · scope · sequence · share · show · Sigma · snd · space · span · spawn · stay · stream · subcontains · terminal · then · this · through · times · to · topology · topos · true · Type · unifies · unknown · uses · verify · via · view · visits · when · where · while · wire · with

Each construct carries a status:

• ✓, verified end-to-end: a regression example or a compiled probe exercises it through yonc down to a running binary.
• ✗ rejected, the grammar accepts it but the type checker refuses it cleanly, by design, with a specific error. A deviation, pinned by a negative fixture in regression/canonical_forms/.
• ⚠ not implemented, the grammar accepts it, but the 1.0 compiler does not implement it (it fails at emission, or the construct cannot actually be used). Listed for completeness; not part of the 1.0 contract.

Lexical structure

Form	Status	Meaning
// ..., /* ... */	✓	Line / block comments
42, 3.14	✓	number literal (IEEE f64)
"ciao"	✓	String literal, a real value of type text/String (see Strings)
true, false	✓	Boolean literals
present, absent, unknown	✓	Heyting truth values (intuitionistic Ω)
mod::name	✓	Qualified name (module namespace)

Duration literals (100ms, 5s, 2min) were removed in v1.1.0: 2s now lexes as NUM_LIT 2 followed by the identifier s. Currency literals (10.50 EUR) are likewise not in the grammar; the money type exists (see Types).

Strings

Since the string fusion, text and String are the same semantic object: sections of the builtin String place. At runtime a string is a handle into the content-addressed heap; literals are interned, so the same literal is the same value and String.equal compares content:

fun greet(who: String): String {
  return String.concat("ciao ", who)
}

fun main(): number {
  be msg holds greet("mondo")
  be _w holds File.write_text("/tmp/out.txt", msg)
  return String.length(msg)        // 10
}

Strings are process-local: they cannot cross a Space (package) boundary, only numbers travel on the wire.

Bindings and mutation

Form	Status	Meaning
be x holds e	✓	Immutable binding, the only declaration form, at top level and inside functions alike (there is no let keyword). Declares once per scope: re-holds of a name already bound in the same scope is a compile error (use x = e to reassign); nested-scope shadowing is allowed, _-prefixed names are exempt
x = e	✓	Space-cell assign (the content-addressed mutation mechanism). The target binding is promoted to a Space cell: its be allocates the cell, reads go through it, x = e updates it. Works on locals and parameters. Snapshot semantics, no aliasing (be y holds x does not alias x's cell)
Space.make / set / get	✓	The underlying mutable cells, also usable directly
x.f = e	✗ rejected	Field mutation: place sections are immutable in 1.0; the type checker rejects it ("place sections are immutable"). Mutate through cells

= is the assignment operator. The same = token also appears in top-level categorical definitions (place P = pullback(f, g)), in prop name(...) = e inside a topos, and in show f = e inside views. There is no becomes keyword.

Types

Form	Status	Meaning
number, text, boolean, proposition, money	✓	Primitives. boolean ≡ proposition (Ω); text ≡ String
T in A, B, C	✓	Constrained primitive (e.g. money in EUR, USD)
A | B | C(T)	✓	Sum type; variants may carry arguments
list of T, map of K to V	✓	Collections
stream of T	✓	Stream type. (The buffer N / drop oldest / drop newest modifiers were parsed but never consumed and were removed in v1.1.0)
T -> U	✓	Function type, right-associative
heyting<N>	✓	Heyting integer: N trits with an Unknown mask
Type, Type_0, Type_1, …	✓	Universes (HoTT)
Pi(x: A). B, Sigma(x: A). B	✓	Dependent function / pair types
Id(A, x, y)	✓	Identity (path) type between terms x, y
{ x : A where P }	✓	Comprehension: the subobject of A carved out by the fibre P (a Σ whose first projection is monic when P is a mere proposition)
move from W1 to W2	✓	Handle types: arrows are first-class values that
reduction of P	✓	can be passed as parameters. Each keeps its
morph from S1 to S2	✓	categorical stratification (no nesting, only
view of P	✓	composition via compose)

A function parameter may omit its annotation; the signature pre-pass infers it from the call sites.

Expressions

Form	Status	Meaning
f(a, b), mod::f(a)	✓	Calls. Nullary builtins are called with empty parens (): HashSet.empty(), XSet.empty(), Vec.empty(), Arena.empty(). A few builtins instead take an explicit unit argument (0) (signature [unit]): List.empty(0), Time.now_ms(0), Args.count(0)
obj.field, x.f1.f2	✓	Field access (chains left-associatively)
e.method(args).map(f).fold(0, g)	✓	Method chaining: recv.m(args) ≡ m(recv, args)
a |> f(args)	✓	Pipe: passes a as the first argument of the call
if c then a else b	✓	Conditional expression (lowers to scf.if)
fun(x: T, y) => e	✓	Inline lambda (unannotated params are inferred)
move(s: P) => new Q {...} from P to Q	✓	Inline handle lambdas, one per arrow kind. They bind, compose
reduction(acc, x) => e of P	✓	(kind-checked: same kind, or post-compose of view/reduction with
view(s: P) => e of P	✓	a fun), and apply, a bound or composed handle is called like a
functor(x) => e from W to V [law id]*	✓	function, and apply_move accepts a locally bound move-lambda.
morph(s) => e from S1 to S2	✓	Functor laws are checkable
compose h1 with h2	✓	Handle composition, (compose f with g)(x) = g(f(x)). Kind discipline enforced: e.g. reduction ∘ reduction is rejected (the eliminator lands in number)
morphism body is closed	✓	A move/functor/view/reduction/morph body may use only its parameters and top-level definitions; capturing an enclosing local is a compile-time error (it could not survive crossing a Space). A plain fun lambda, by contrast, captures enclosing locals at any nesting depth
f(args) in S	✓	Call in a Space context (apply_move ... in S, morph dispatch)
all P where cond	✓	Quantification over the sections of a place
verify P	✓	Instantiate a law-verified place as a Magma handle
new P { field value }	✓	Section construction, no = between field and value
refl(t), pair(a,b), fst(p), snd(p)	✓	HoTT introduction forms
ind_path(C, d, p)	✓	The J eliminator: computes d(basepoint) when p is refl in evidence at the call site; a J stuck on a non-refl path is rejected at compile time (the runtime never decides path equality)
plam i => e	✓	Path abstraction over a dimension i; the face system for the compositions is written i = I0 => plam j => e / i = I1 => plam j => e
hit(ctor) / hit(ctor, a), hit_elim(C, [b => e, ...], x)	✓	Higher inductive type constructor and eliminator; one branch per constructor, the path branches respecting the points (examples/circle_hit)
comp(line)[faces] / hcomp T[faces]	✓	Kan composition along a line / homogeneous composition; reduced by the kernel (regression/yon_tests/prove)
quote(c, a) / el_match(target, ret, body)	✓	Universe-code introduction / elimination for El(c); lowers to the inhabitant / the body application. The deeper Tarski reflection is 1.2
pullback(f, g, a, b)	✓	Runtime compatible pair with f(a) == g(b) checked. The no-arg expression forms pullback(f, g) / pushout(f, g) were removed in v1.1.0; the two-argument form survives only as the declaration place P = pullback(f, g) (see Places)
heyting(v), heyting(v, mask)	✓	Heyting-integer constructor (mask marks Unknown trits)

Operators (by family)

Operators	Status	Meaning
+ - * / %, unary -	✓	Arithmetic
== != < > <= >=	✓	Comparison
and/&&, or/||, not/!	✓	Classical logic
a => b	✓	Classical implication, sugar for (not a) or b
& | ^ ~	✓	Bitwise on numbers
&&? ||? =>? !?	✓	Heyting (scalar Ω): and, or, implication, negation
&? |? ^? ~?	✓	Heyting trit-wise on heyting (Unknown-mask propagation)
: . -> |>	✓	Annotation, access, function type, pipe

Statements

Form	Status	Meaning
return e	✓	Return from the function
when c { } when c2 { } otherwise { }	✓	Conditional chain. A return inside a branch does not exit the function, branches are for effects; select values with if/then/else
e is pattern, e is not pattern	✓	Pattern conditions (in when/forces): patterns are a variable, a literal, present, absent, unknown; chainable with and/or
iter n do { }	✓	Bounded loop (always terminates; scf.for)
while c do { }	✓	General loop (scf.while)
scope [Name] { }	✓	Hermetic block (see below)
with R of P { }	✓	Activate reduction R over P for the block
produce { } / emit e	✓	Producer block / emit into the active stream or handler
spawn { } / spawn in N parallel { } / promote e	✓	Fork one or N isolated process replicas; each promote e contributes to the block's collection stream, drained by the parent with .fold / .for_every. spawn_index (0..N-1) is in scope in the body. Scaling measured in Appendix D
forces stage cond { }	✓	Kripke–Joyal forcing block at a stage
for every x in e { } (+ when here)	✓	Iteration over a List. 1.0 executes sequentially; parallelism (and the when here space filter) are declared intent, not yet a runtime distinction
in sequence over x in e { }	✓	Sequential iteration over a List
repeat at most N times { } [otherwise { }]	✓	The body runs exactly N times, then otherwise (if present) runs. A success-based early exit is a post-1.0 protocol
forever { }	✓	Infinite loop (while present); typically paired with effects inside

Hermetic scope

A scope block is a formally hermetic region: at the IR level it becomes a topos.scope_with_yield region with the MLIR trait IsolatedFromAbove. Every outer binding the body uses enters as an explicit capture; an implicit reference is a compiler error, verified on the real IR.

fun main(): number {
  be base holds 40
  scope Hermetic {
    be sealed holds base + 2    // `base` enters as an explicit capture
  }
  return base + 2               // 42
}

Functions

fun f(x: number, y: number): number { return x + y }
fun g<A, B>(x: A): B { ... }                      // type parameters
fun h(x: number): number visits Output { ... }    // declared effect
internal fun secret(x: number): number { ... }    // not exported cross-Space
partial fun p(x: number): number { ... }          // partial (may not return)

All four modifiers are ✓ verified. Effect discipline (visits): calling a function that visits E requires the caller to cover E, by declaring visits E itself or having a handler active; the effect propagates up to main. I/O is an effect (visits Output).

Worlds

A world has no surface syntax. world is not a lexer keyword, so any world W { ... }, world W = A * B, world W = A + B, world W = Base / Rel, or world W subset of V is a parse error.

A world is declared only in yon.toml, never in a .yon file:

[world.Park]
objects = ["Dinosaur", "Herd"]
spaces  = ["Enclosure"]

A place then takes its world by inference from the project's toml, not from an in W clause in the source.

Places, operations, laws

Form	Status	Meaning
place P [over X] [subcontains B] [on error E] { members }	✓	An object (its world is inferred from the toml; there is no in W clause). over X = slice (fibered over X); subcontains B = sub-object mono P ↪ B; on error E = error morphism P → E
place P ... with effects { ... }	✓	Enables operations (1-cells) among the members
error E [subcontains B] { fields }	✓	An error place (target of on error); world inferred from the toml, no in W clause
field_name type	✓	Field, no colon: balance number
operation op(a: T): U	✓	Operation (1-cell)
functorial operation op(...)	✓	Operation lifted along world morphisms (Yoneda lifting)
operation op(...) uses algebra Additive	✓	Bind to a catalog algebra; laws certified by the compiler
law commutative etc.	✓	Declared law, verified (AlgebraVerifier)
cell c from e1 to e2	✓	Higher cell between lower cells (CaTT witness)
place P = pullback(f, g) / pushout(f, g)	✓	Place as a limit / colimit

Catalog algebras: Additive, Multiplicative, TropicalMax, TropicalMin, BooleanOr, BooleanAnd, Gcd.

Arrows

Form	Status	Meaning
move m from P to Q [requires CAP1, CAP2] { A maps to B by f ... }	✓	Move between places; the body is a list of mapping clauses; requires lists capabilities
move m unifies A, B { share f1, f2 conflict on f resolves to fn }	✓	Merge move: shared fields plus per-field conflict resolution; applied with Move.merge(m, s1, s2), result in the first source place
A maps to B by f / converts to / aggregates to	✓	Mapping kinds; by fun(x) => e inline lambda allowed
morph F from W to V { on object(...) { } on morphism op via op2 }	✓	Functor by components; on object: fun(...) => e inline form allowed; on, object, morphism stay free as user identifiers
functor F(x: T) from W to V [law identity] [law composition] { return e }	✓	Functor given by a return expression with declared laws
nat transform t from F to G { for each X by fnX }	✓	Natural transformation: one component per object
geomorph g from P to Q { pull(...) { } push(...) { } }	✓	Geometric morphism, the adjoint pair f* ⊣ f∗: pull is the inverse image, push the direct image; clauses adjunction, exact pull, exact push declare its properties
view V of P { show f show f = e show f as "label" }	✓	Derived projection of a place, lowered to a record place plus a constructor: V(x) builds the projection, fields read normally
topology j of P { ... }	✓	Lawvere–Tierney topology: a body defining j : Ω → Ω
reduction [forward|backward|bi] [lawful] [invertible] R[<T>] of P [with multishot] [fold "sum_f64"] { on op(params) { } be x holds e }	✓	Reduction with direction and laws; clauses are contextual on handlers and be bindings

Topos declarations

topos Account where {
  terminal Unit                                  // optional
  morphisms { ...morphism declarations... }      // optional
  prop is_overdrawn(s: State): proposition = s.balance < 0
}

Status: ✓ (regression examples). Under v1.1.0 topos-per-space there is no in W or at SPACE annotation and no inline objects { } block: the world, the residence space, and the objects are all inferred from the filesystem. The morphisms { } block declares its members with the singular morphism keyword. A prop is a subobject classifier, a map into Ω; the abstract form (no = body) declares the signature only.

Spaces and packages

A Space has no surface declaration. There is no space S ... declaration form (the space keyword's SPACE token appears only inside the expression wire to space S), and init is not a keyword (init X as Space is a parse error). A Space is a filesystem directory plus its yon.toml, discovered by the toolchain, not declared in source.

The import forms below are the surface syntax that references Spaces:

Form	Status	Meaning
import "file.yon"	✓	File import
import m::n [as alias]	✓	Symbol import from a module
import m::n from Space	✓	Cross-package import: n becomes a remote arrow into Space

Cross-package calls are RPC over a named channel (/yon_stream_<Space>): only numbers cross the boundary, at most 4 arguments; internal functions are not exported; the server binary is ./<Space>_srv by convention (override with YON_SRV_DIR), spawned on first contact, shut down in cascade, and transparently recovered after a crash (virgin channel, epoch advanced, one retry).

Hermeticity model: cross-package = process isolation (kernel MMU, values only on the wire); intra-package = typed/logical (visibility, internal, effects, move/morphism gating) with opt-in physical heap separation (YON_BACKEND=separate).

Standard library (module index)

Module	Operations
IO	print_num
String	length, concat, equal, char_at, substring, find_char, from_char, from_int, parse_number, print
File	read_text, exists, write_text, append_text
Env	get, has
Args	count, get
Time	now_ms, now_ns
Random	seed, int, range
Math	sqrt, abs, floor, ceil, round, min, max, pow, log, log2, log10, exp, sin, cos, sinh, cosh, tanh, atan2, modulo, gcd, lcm, pi, e
Bits	and, or, xor, not, shl, shr, popcount, fold, *_64
Crypto	fnv1a, hash_int
List / HashMap / HashSet / XSet	Immutable collections over the content-addressed heap
Vec	empty, push, get, set, size, a dynamic array on an arena strip (in-place mutable, no malloc)
MerkleTree	Content-addressed Merkle trees
VoyagerList	Golay-sealed list (error-correcting)
Magma	gen, closure_size, is_commutative, is_associative, identity, word_push, normal_form, from_catalog, with verify P
Stream	from_list, map, filter, fold, iterate, take
Space	make, set, get, mutable cells (the 1.0 mutation mechanism)

Failure convention: string-producing operations return the 0.0 handle on failure (missing file, unset variable, out-of-range index).

Conventions

• Nullary builtins are called with empty parens (): XSet.empty(), Vec.empty(). The few with a unit-argument signature take (0): List.empty(0), Time.now_ms(0), Args.count(0).
• new P { field value } and place fields name type, no =, no :.
• A program's exit code is main's return value, truncated mod 256.
• return inside a when branch does not exit the function; use if/then/else to select values.