Appendix D: Bridger Language Reference

This appendix covers Bridger’s formal definitions: the rules that dictate what a program means. The concrete syntax (how one writes a Bridger program as a string of characters) can be found in Appendix B, and Bridger’s prelude (the set of built-in functions and capabilities) is in Appendix C. Throughout the book, each chapter develops the semantics of Bridger one feature at a time. This appendix develops the full formal semantics all at once in its complete form. To learn how to read an inference rule, and the symbols the rules use, see the Notation reference in Appendix G.

Abstract syntax

The rules range over the abstract syntax (the output of Bridger’s parser, after the surface details of the concrete syntax are resolved). In the AST chapter we detail that tree, including the exact Rust enum this book asks you to interpret through its milestones. Below is the grammar, over programs, expressions e, blocks, definitions d, patterns p, and query atoms q:

$$\begin{array}{rlrl}e::=& n\mid b\mid s\mid ()& & \text{literals}\\ \mid & x\mid \text{self}& & \text{variable, receiver}\\ \mid & -e\mid e\oplus e\mid e\otimes e& & \text{negation, arithmetic, comparison}\\ \mid & \text{not}e\mid e\text{and}e\mid e\text{or}e\mid e++e\mid e::e& & \text{boolean, concatenation, cons}\\ \mid & \text{if}e\text{then}e\text{else}e\mid \text{match}e\{{arm}^{+}\}& & \text{conditionals}\\ \mid & (e,\dots ,e)\mid [e,\dots ,e]\mid e.i\mid e.f& & \text{tuple, list, projection, field}\\ \mid & C(e,\dots ,e)\mid S\{f:e,\dots \}& & \text{constructor, struct literal}\\ \mid & e(e,\dots ,e)\mid e.m(e,\dots ,e)\mid \lambda x,\dots ,x.e& & \text{application, method, lambda}\\ \mid & e?& & \text{error propagation}\\ \mid & \text{ref}e\mid \text{deref}e\mid e:=e& & \text{references}\\ \mid & \text{while}ee\mid \text{for}x\text{in}ee\mid \text{for}qe\mid \text{return}e& & \text{loops, return}\\ \mid & \{blk\}\mid \text{add}q\mid \text{clear}R\mid \text{solutions}q\mid q& & \text{block, relations}\\ blk::=& (\text{let}x=e)blk\mid eblk\mid e\mid \epsilon & & \text{block interior}\\ arm::=& p[\text{if}e]\Rightarrow e& & \text{match arm}\\ prog::=& d^{\ast }& & \text{program (definitions, order-free)}\\ d::=& \text{fn}f(x,\dots ,x)=e& & \text{function}\\ \mid & \text{let}x=e& & \text{global}\\ \mid & \text{type}T=C(\tau ,\dots )\text{’|’}\cdots \text{’|’}C(\tau ,\dots )& & \text{data type}\\ \mid & \text{struct}S\{f:\tau ,\dots \}& & \text{struct}\\ \mid & \text{trait}Tr\{(\text{fn}m(\text{self},x:\tau ,\dots )\to \tau {)}^{\ast }\}& & \text{trait}\\ \mid & \text{impl}[Tr\text{for}]\tau \{(\text{fn}m(\text{self},x,\dots )=e{)}^{\ast }\}& & \text{impl}\\ \mid & \text{relation}R:(\tau ,\dots )& & \text{relation}\\ \mid & \text{rule}q[\text{:-}body]& & \text{rule}\\ p::=& \_\mid lit\mid x\mid C(p,\dots )\mid (p,\dots ,p)& & \text{wildcard, literal, variable, constructor, tuple}\\ \mid & [p,\dots ]\mid [p,\dots ,\dots x]\mid p::p\mid S\{f:p,\dots \}\mid p\text{’|’}p& & \text{list, cons, struct, or}\\ q::=& R(a,\dots ,a)& & \text{query atom}\\ a::=& e\mid ?x\mid ?& & \text{query argument}\end{array}$$

Here $\oplus \in \{+,-,\ast ,/,\%\}$ ranges over the arithmetic operators and $\otimes \in \{==,!=,<,\le ,>,\ge \}$ over the comparisons. A projection index i is a literal integer; f is a field name, m a method name, C a constructor, S a struct name, $Tr$ a trait, R a relation. The quoted '|' inside a data type or an or-pattern is Bridger’s own token, set apart from the metagrammar’s $\mid$ as in Appendix B. The ref x = e binding desugars to let x = ref e, and fn foo(x: Int) = e; to fn foo(x: Int) { e }. The keyword form if e then e else e is this grammar’s spelling of the braced concrete syntax if e { e } else { e }. Error propagation e? is sugar over match and return (error handling); it has no evaluation rule of its own below, and its typing is stated after $\text{T-Return}$.

Definitions appear only at the top level; a block holds let bindings and expressions, so a local function is a let-bound lambda — which, like any let, is not in scope in its own right-hand side, so a local function cannot call itself; recursion is for top-level fns — and execution begins at a required main. A type, struct, trait, impl, or fn may take type parameters $⟨\bar{T}⟩$ with trait bounds; the grammar leaves these implicit and the typing rules make them explicit. A bound on a type or struct parameter is required where a value of the type is built — a constructor application or a struct literal — so a Box<T: Ord> never holds a function.

Values

Evaluation produces a value. The values are the literals, the compound forms built from them, a location (the identity of an allocated cell), and a closure (a function paired with the environment it captured):

$$\begin{array}{rlrl}v::=& n\mid b\mid s\mid ()& & \text{integer, boolean, string, unit}\\ \mid & (v,\dots ,v)\mid []\mid v::v& & \text{tuple, empty list, cons}\\ \mid & C(v,\dots ,v)\mid S\{f=v,\dots \}& & \text{constructor value, struct value}\\ \mid & \ell \mid ⟨\lambda x,\dots ,x.e,\rho ⟩& & \text{location, closure}\\ \mid & R\mid T& & \text{relation, type name}\end{array}$$

where n ranges over integers ($\mathbb{Z}$), b over the booleans $\text{true}$ and $\text{false}$ ($\mathbb{B}$), and s over strings. An integer is a signed 64-bit two’s-complement value — every literal denotes one, the least of them written -9223372036854775808 — and the arithmetic operators wrap on overflow: the $v_1+v_2$ the rules write is addition modulo $2^{64}$, so no overflow is stuck. Division truncates toward zero and the remainder takes the dividend’s sign, so -7 / 2 is -3 and -7 % 2 is -1. A list is the empty list $[]$ or a cons $v_h::v_t$; the literal $[v_1,\dots ,v_n]$ is shorthand for $v_1::\cdots ::v_n::[]$. A nullary constructor value is written C for C(). The last two are not data: a relation value $R$ is what a declared relation’s name evaluates to, consumed only by the query forms, and a type name $T$ is what a bare struct, type, or built-in type name evaluates to, consumed only as the receiver of an associated call. Neither compares, prints, or enters a relation.

Evaluation is carried out against three pieces of state. The environment $\rho$ maps each variable in scope to its value; the store $\sigma$ maps each allocated location to the value it holds; and (from the relations section) the relation database $\Delta$ holds the facts that queries read.

$$\rho :Var\rightharpoonup v\sigma :Loc\rightharpoonup v\Delta \subseteq \{R(v,\dots ,v)\}$$

The grammar above is complete — every value a Bridger program produces is one of these. Its forms enter the language across the book (locations with mutable references, closures with functions, the compound forms with tuples and lists); the reference gathers them here so the rules below have their operands defined.

The evaluation judgment

The central judgment is

$$\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨r,{\sigma }^{\prime },{\Delta }^{\prime }⟩r::=\mathsf{Val}v\mid \mathsf{Ret}v$$

read in environment $\rho$, evaluating expression $e$ against store $\sigma$ and relation database $\Delta$ produces outcome $r$, updated store ${\sigma }^{\prime }$, and updated database ${\Delta }^{\prime }$. The outcome is $\mathsf{Val}v$ for an expression that finishes normally with value $v$, and $\mathsf{Ret}w$ for one that returns early (return w) without executing the remaining body of the enclosing function. Once $\mathsf{Ret}w$ hits the enclosing function boundary, it turns from a returned value into a regular $\mathsf{Val}w$.

Two conventions keep the rules readable:

• A bare value ($v$) in result position means $\mathsf{Val}v$. A conclusion or premise written $⟨v,{\sigma }^{\prime }⟩$ abbreviates $⟨\mathsf{Val}v,{\sigma }^{\prime }⟩$. The $\mathsf{Ret}$ outcome is always written out. So every value-case rule reads as an ordinary big-step rule, and only return, application, and the loops mention $\mathsf{Ret}$ at all.
• $\mathsf{Ret}$ short-circuits. When a premise written $⟨v_i,{\sigma }_i⟩$ is discharged by a subexpression that instead yields $⟨\mathsf{Ret}w,{\sigma }_i⟩$, the rule does not fire; the enclosing expression evaluates to $⟨\mathsf{Ret}w,{\sigma }_i⟩$, and the subexpressions to its right are not evaluated. This one convention threads $\mathsf{Ret}$ outward through every rule without doubling any of them.

Worked expansion. To see what the conventions abbreviate, consider the rule for addition:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨v_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v_2,{\sigma }_2,{\Delta }_2⟩v_1,v_2\in \mathbb{Z}}{\rho ⊢⟨e_1+e_2,\sigma ,\Delta ⟩\Downarrow ⟨v_1+v_2,{\sigma }_2,{\Delta }_2⟩}(\text{E-Add})$$

The above rule is actually three separate rules. The case where bot operands evaluate to values:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\mathsf{Val}{v}_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨\mathsf{Val}{v}_2,{\sigma }_2,{\Delta }_2⟩v_1,v_2\in \mathbb{Z}}{\rho ⊢⟨e_1+e_2,\sigma ,\Delta ⟩\Downarrow ⟨\mathsf{Val}(v_1+v_2),{\sigma }_2,{\Delta }_2⟩}(\text{value})$$

and two more cases where the left or right operand return a value $\mathsf{Ret}w$:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\mathsf{Ret}w,{\sigma }_1,{\Delta }_1⟩}{\rho ⊢⟨e_1+e_2,\sigma ,\Delta ⟩\Downarrow ⟨\mathsf{Ret}w,{\sigma }_1,{\Delta }_1⟩}(\mathsf{Ret}\text{in}{e}_1)$$

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\mathsf{Val}{v}_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨\mathsf{Ret}w,{\sigma }_2,{\Delta }_2⟩}{\rho ⊢⟨e_1+e_2,\sigma ,\Delta ⟩\Downarrow ⟨\mathsf{Ret}w,{\sigma }_2,{\Delta }_2⟩}(\mathsf{Ret}\text{in}{e}_2)$$

Every rule uses these conventions to implicitly thread returned values while only needing to explicitly describe the semantics for the case where all operands evaluate to values. The application is explicitly stated as it unlike other rules explicitly turns a returned value within the function to a value (the value computed/returned by the function).

The environment $\rho$ is read-only; the store $\sigma$ and the database $\Delta$ are threaded — each rule passes them out of one subexpression and into the next, so a change one subexpression makes is visible to those evaluated after it. Threading is needed because a subexpression can be effectful: a call may allocate or write a reference, add and clear change the database, and either can sit as an operand of +, so x + f() may alter $\sigma$ or $\Delta$ between evaluating x and combining the results.

Every rule below threads both the store and $\Delta$ in evaluation order, so each records how its subexpressions are sequenced; the rules that leave a piece of state untouched thread it unchanged rather than drop it. Slices appear in the chapters, not here — each an honest projection of the judgment above. Nothing writes the store until mutable references in Part IV, so those chapters use the store-free $\rho ⊢e\Downarrow v$; nothing writes $\Delta$ until the relations material, so earlier chapters drop it.

The typing judgment

The static semantics is the judgment

$$\Gamma ⊢e:\tau$$

read in typing context $\Gamma$, expression $e$ has type $\tau$, where $\Gamma$ records the type of each variable in scope together with the enclosing function’s return type. The typing rules below give the static semantics declaratively; the bidirectional checking and local inference that decide it are built with the type checker in Part VI. The judgment is stated here first so the evaluation rules can name the types they assume.

The metavariables used throughout extend the notation reference ’s table:

Runtime errors: stuck evaluation

Some expressions have no value. Adding a boolean to an integer, applying a non-function, or reading a field a value does not have fits no rule, so no derivation of $\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨r,{\sigma }^{\prime },{\Delta }^{\prime }⟩$ exists. Evaluation is then stuck: the interpreter halts and reports the offending expression rather than producing an outcome. These are Bridger’s runtime type errors, and in the untyped evaluator they are how a nonsensical program fails.

Stuckness is the absence of an outcome rather than a special one. It stands apart from the recoverable failures modeled by Option and Result, which are ordinary values handled with match and live entirely inside the evaluation relation — evaluating Err("…") is a successful derivation that yields a value. Error handling develops that distinction; the type checker later rules out the type-shaped stuck cases for the programs it accepts — a non-exhaustive match among them — leaving division by zero and a failed read from input as the errors that survive typing.

The stuck cases, gathered from the rules below, are: an unbound variable; arithmetic, negation, or ordering on a non-integer, and min, max, minimum, or maximum on operands with no shared order; a non-boolean condition to if, while, and, or, or not; division or modulo by zero; ++ on operands that are not both strings or both lists, or :: onto a value that is not a list; a projection or field access on a value that lacks it; applying a non-function, or calling a function, a method, a constructor, or a relation — in add or a query — with the wrong arity; applying a name that is not a constructor, or a struct literal naming no struct, missing one of its fields, or giving one twice; a match no arm covers; iterating a non-list; dereferencing or assigning through a non-location; equality on a function or relation, and printing one; a method the receiver’s head lacks, a self method called on a type name, or one without self called on a value; a return no function catches; a query, an add, or a clear inside a rule’s filter, and a filter or a guard whose value is not a boolean; a hole in an add atom; a program with no main, or whose global initializers form a cycle; a read_* whose input is not what it reads (its _opt form returns None instead and consumes no input; read_line drops a trailing carriage return); and two bounds of the machine, a call nested more than 100 000 frames deep — a frame per application of a function, lambda, or method body, the from a ? converts through included; natives and constructors open none, while the prelude’s functions written in Bridger open one like any other — and a range of more than 2^26 elements. The static checks report the first error in source order, and reject an expression nested more than 150 000 levels deep — every expression node a level, a block or a branch included. The interpreter holds that same bound before a program runs, so a milestone with no type checker rejects such a tree in place of exhausting the evaluator’s recursion; where the checker runs, it reports the depth first. Premises are discharged left to right, and a premise whose result has the wrong form ends evaluation there: a non-location target of := is stuck before its right-hand side runs, a non-function operator before its arguments, and a wrong arity — of a function, a method, a constructor, or a relation atom alike — or a method the receiver lacks, after them.

The reference interpreter names the stuck cases as follows in its RuntimeError, and a submission reports the same names. Each carries the span of the node whose rule failed — the operator, the call, the match, the guard, the add or query form; a return or ? that escapes an initializer or a filter carries that initializer’s or filter’s span, and a missing main a synthetic one. Where a rule has several operands, found is the first, left to right, whose form is wrong, and expected is the form the rule required of it.

Evaluation rules

Throughout, the store and database are threaded left to right. Where a rule’s premises evaluate several subexpressions, they are written in evaluation order, and both pass $\sigma \to {\sigma }_1\to {\sigma }_2\to \cdots$ and $\Delta \to {\Delta }_1\to {\Delta }_2\to \cdots$ from each to the next.

Literals and variables

A literal evaluates to itself and leaves the store untouched ($n$, $b$, $s$, and () all take this form):

$$\frac{}{\rho ⊢⟨n,\sigma ,\Delta ⟩\Downarrow ⟨n,\sigma ,\Delta ⟩}(\text{E-Lit})$$

A variable evaluates to the value the environment binds to it; self, inside a method, is the variable bound to the receiver:

$$\frac{\rho (x)=v}{\rho ⊢⟨x,\sigma ,\Delta ⟩\Downarrow ⟨v,\sigma ,\Delta ⟩}(\text{E-Var})$$

When $\rho$ has no binding for $x$ the premise cannot be met, no rule applies, and evaluation is stuck on the unbound variable.

Arithmetic

Addition evaluates its left operand, then its right against the store the left produced, then combines the results — threading store and database, $\sigma \to {\sigma }_1\to {\sigma }_2$ and $\Delta \to {\Delta }_1\to {\Delta }_2$, in evaluation order:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨v_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v_2,{\sigma }_2,{\Delta }_2⟩v_1,v_2\in \mathbb{Z}}{\rho ⊢⟨e_1+e_2,\sigma ,\Delta ⟩\Downarrow ⟨v_1+v_2,{\sigma }_2,{\Delta }_2⟩}(\text{E-Add})$$

Subtraction and multiplication take the same shape, with $\oplus \in \{+,-,\ast \}$ computed on integers:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨v_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v_2,{\sigma }_2,{\Delta }_2⟩v_1,v_2\in \mathbb{Z}}{\rho ⊢⟨e_1\oplus e_2,\sigma ,\Delta ⟩\Downarrow ⟨v_1\oplus v_2,{\sigma }_2,{\Delta }_2⟩}(\text{E-Arith})$$

Division and modulo add a premise that the divisor is nonzero; when $v_2=0$ no rule applies and evaluation is stuck:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨v_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v_2,{\sigma }_2,{\Delta }_2⟩v_1,v_2\in \mathbb{Z}{v}_2\ne 0}{\rho ⊢⟨e_1/e_2,\sigma ,\Delta ⟩\Downarrow ⟨v_1÷v_2,{\sigma }_2,{\Delta }_2⟩}(\text{E-Div})$$

Modulo ($\%$) is identical with the remainder in place of the quotient. Negation evaluates its operand and negates an integer:

$$\frac{\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }^{\prime },{\Delta }^{\prime }⟩v\in \mathbb{Z}}{\rho ⊢⟨-e,\sigma ,\Delta ⟩\Downarrow ⟨-v,{\sigma }^{\prime },{\Delta }^{\prime }⟩}(\text{E-Neg})$$

Comparison and equality

A comparison evaluates both operands and returns a boolean. Writing $\otimes$ for one of the six operators and $\hat{\otimes }$ for the corresponding relation on values:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨v_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v_2,{\sigma }_2,{\Delta }_2⟩v_1,v_2\in \mathbb{Z}}{\rho ⊢⟨e_1\otimes e_2,\sigma ,\Delta ⟩\Downarrow ⟨(v_1\hat{\otimes }{v}_2),{\sigma }_2,{\Delta }_2⟩}(\text{E-Ord})$$

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨v_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v_2,{\sigma }_2,{\Delta }_2⟩}{\rho ⊢⟨e_1\otimes e_2,\sigma ,\Delta ⟩\Downarrow ⟨(v_1\hat{\otimes }{v}_2),{\sigma }_2,{\Delta }_2⟩}(\text{E-Eq})$$

The ordering operators <, <=, >, >= require integer operands. Equality == and inequality != are structural: they compare integers, booleans, strings, unit, tuples, lists, constructor values, and struct values componentwise, so $(1,[2])==(1,[2])$ is true. A location compares by identity: two references are equal exactly when they are the same cell, whatever the cells hold. Equality on a function (closure) or a relation has no value and is stuck. Comparisons do not chain: the grammar makes them non-associative, so a < b < c is not a program.

Boolean connectives

and and or short-circuit: the right operand is evaluated only when the left does not already settle the result. For and, a false left operand settles it, and the right is not evaluated:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\text{false},{\sigma }_1,{\Delta }_1⟩}{\rho ⊢⟨e_1\text{and}{e}_2,\sigma ,\Delta ⟩\Downarrow ⟨\text{false},{\sigma }_1,{\Delta }_1⟩}(\text{E-And-False})$$

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\text{true},{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩v\in \mathbb{B}}{\rho ⊢⟨e_1\text{and}{e}_2,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩}(\text{E-And-True})$$

or is symmetric: a true left operand settles it as $\text{true}$ without evaluating the right, and a false left operand yields the value of the right.

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\text{true},{\sigma }_1,{\Delta }_1⟩}{\rho ⊢⟨e_1\text{or}{e}_2,\sigma ,\Delta ⟩\Downarrow ⟨\text{true},{\sigma }_1,{\Delta }_1⟩}(\text{E-Or-True})$$

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\text{false},{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩v\in \mathbb{B}}{\rho ⊢⟨e_1\text{or}{e}_2,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩}(\text{E-Or-False})$$

Negation evaluates its operand, which must be a boolean, and flips it:

$$\frac{\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨b,{\sigma }^{\prime },{\Delta }^{\prime }⟩b\in \mathbb{B}}{\rho ⊢⟨\text{not}e,\sigma ,\Delta ⟩\Downarrow ⟨\neg b,{\sigma }^{\prime },{\Delta }^{\prime }⟩}(\text{E-Not})$$

A non-boolean operand to any of the three fits no rule and is stuck.

Concatenation, tuples, and lists

++ concatenates two strings or two lists, threading the store left to right. On lists it appends; on strings it joins:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨v_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v_2,{\sigma }_2,{\Delta }_2⟩v_1,v_2\text{ strings or }{v}_1,v_2\text{ lists}}{\rho ⊢⟨e_1++e_2,\sigma ,\Delta ⟩\Downarrow ⟨v_1++v_2,{\sigma }_2,{\Delta }_2⟩}(\text{E-Concat})$$

where $v_1++v_2$ on lists is $v_2$ when $v_1=[]$ and $v_h::(v_t++v_2)$ when $v_1=v_h::v_t$. :: prepends one value to a list; its right operand must be a list, and its left may be any value:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨v_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v_2,{\sigma }_2,{\Delta }_2⟩v_2\text{ a list}}{\rho ⊢⟨e_1::e_2,\sigma ,\Delta ⟩\Downarrow ⟨v_1::v_2,{\sigma }_2,{\Delta }_2⟩}(\text{E-Cons})$$

A tuple and a list evaluate their elements left to right and collect the results:

$$\frac{\rho ⊢⟨e_i,{\sigma }_{i-1},{\Delta }_{i-1}⟩\Downarrow ⟨v_i,{\sigma }_i,{\Delta }_i⟩(1\le i\le n)}{\rho ⊢⟨(e_1,\dots ,e_n),{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨(v_1,\dots ,v_n),{\sigma }_n,{\Delta }_n⟩}(\text{E-Tuple})$$

$$\frac{\rho ⊢⟨e_i,{\sigma }_{i-1},{\Delta }_{i-1}⟩\Downarrow ⟨v_i,{\sigma }_i,{\Delta }_i⟩(1\le i\le n)}{\rho ⊢⟨[e_1,\dots ,e_n],{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨v_1::\cdots ::v_n::[],{\sigma }_n,{\Delta }_n⟩}(\text{E-List})$$

Tuple projection e.i and struct field access e.f evaluate the compound and select a component; a projection out of range, or a field the value lacks, is stuck:

$$\frac{\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨(v_0,\dots ,v_{n-1}),{\sigma }^{\prime },{\Delta }^{\prime }⟩0\le i<n}{\rho ⊢⟨e.i,\sigma ,\Delta ⟩\Downarrow ⟨v_i,{\sigma }^{\prime },{\Delta }^{\prime }⟩}(\text{E-Proj})$$

$$\frac{\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨S\{\dots ,f=v,\dots \},{\sigma }^{\prime },{\Delta }^{\prime }⟩}{\rho ⊢⟨e.f,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }^{\prime },{\Delta }^{\prime }⟩}(\text{E-Field})$$

Conditionals

if evaluates its condition, which must be a boolean, and then evaluates the chosen branch against the store the condition produced. The other branch is not evaluated.

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\text{true},{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩}{\rho ⊢⟨\text{if}{e}_1\text{then}{e}_2\text{else}{e}_3,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩}(\text{E-If-True})$$

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\text{false},{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_3,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩}{\rho ⊢⟨\text{if}{e}_1\text{then}{e}_2\text{else}{e}_3,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩}(\text{E-If-False})$$

Both branches must have the same type, which is a typing rule rather than an evaluation one. The else -less form is admitted only when the then-branch has type (); it behaves as if e1 then e2 else (), taking the value () when the condition is false.

Bindings and blocks

A block evaluates its elements top to bottom in an environment that grows as its bindings are met, and its value is the final expression (or () when the last element is followed by ;). A let evaluates its right-hand side and extends the environment over the rest of the block:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨v_1,{\sigma }_1,{\Delta }_1⟩\rho [x\mapsto v_1]⊢⟨\{rest\},{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩}{\rho ⊢⟨\{\text{let}x=e_1;rest\},\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩}(\text{E-Let})$$

An element evaluated for its effect discards its value and threads its store into the rest of the block; the final expression is the block’s value:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨v_1,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨\{rest\},{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩}{\rho ⊢⟨\{e_1;rest\},\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩}(\text{E-Seq})$$

$$\frac{\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }^{\prime },{\Delta }^{\prime }⟩}{\rho ⊢⟨\{e\},\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }^{\prime },{\Delta }^{\prime }⟩}(\text{E-Block})\frac{}{\rho ⊢⟨\{\},\sigma ,\Delta ⟩\Downarrow ⟨(),\sigma ,\Delta ⟩}(\text{E-Empty})$$

A block whose last item is a let has the value (), like a block with no trailing expression; naming that value binds x to (), and the checker catches a later use of x as anything else.

A program is a set of definitions whose order does not matter: every top-level name is visible in every definition, so any function, global, or method may refer to any other wherever it is written. Top-level names are distinct — declaring one twice is rejected, and so is declaring a name the prelude defines. Within one declaration, names are distinct too: a function’s or lambda’s parameters, a declaration’s type parameters, a struct’s fields, and a trait’s methods each name a thing once. A constructor is a top-level name like any other, since a constructor expression or pattern refers to it by that name alone: it may not coincide with a type, struct, trait, or another constructor, its own type included. A constructor name is not a value: it appears only applied. Evaluation binds them all in one program environment ${\rho }_0$ — each relation to a relation value that stands for it, each fn to a closure over ${\rho }_0$, each global let x = e to the value of its right-hand side — and runs main under it — main takes no parameters, and its result is the program’s value, which the bridger command discards: a program reports through print. A missing main, or one that takes parameters or is not a function, is reported before the globals initialize. The fn bindings make ${\rho }_0$ recursive, each closure capturing the very environment that holds it:

$${\rho }_0\supseteq [f\mapsto ⟨\lambda \vec{x}.e_f,{\rho }_0⟩|(\text{fn}f(\vec{x})=e_f)\in prog]$$

Global initializers run in dependency order: a global depends on every global its initializer can reach — directly, through the body of any function it calls, through any method of a name it calls, or through the rule bodies if it evaluates a query — and each is initialized after the globals it depends on, so let a = b + 1; let b = 10; binds a to 11 whichever is written first. Globals are visited in alphabetical order of their names, each initialized after the globals it depends on, so a program’s initialization order is fixed; beyond the dependencies it carries no meaning. A cycle among initializers has no such order and is rejected before anything runs.

The type, struct, trait, impl, relation, and rule definitions register in the contexts they introduce (structs, relations) and bind no runtime value.

References and the store

ref e allocates a fresh location holding the value of e; the location is the value. deref e reads the location’s contents; e1 := e2 writes and yields (). Allocation picks a location outside the current store’s domain:

$$\frac{\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }_1,{\Delta }_1⟩\ell \notin \mathrm{dom}({\sigma }_1)}{\rho ⊢⟨\text{ref}e,\sigma ,\Delta ⟩\Downarrow ⟨\ell ,{\sigma }_1[\ell \mapsto v],{\Delta }_1⟩}(\text{E-Ref})$$

$$\frac{\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨\ell ,{\sigma }^{\prime },{\Delta }^{\prime }⟩\ell \in \mathrm{dom}({\sigma }^{\prime })}{\rho ⊢⟨\text{deref}e,\sigma ,\Delta ⟩\Downarrow ⟨{\sigma }^{\prime }(\ell ),{\sigma }^{\prime },{\Delta }^{\prime }⟩}(\text{E-Deref})$$

Assignment evaluates the cell first, then the value, then updates the store — the cell, then the right-hand side, then the write:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\ell ,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩\ell \in \mathrm{dom}({\sigma }_2)}{\rho ⊢⟨e_1:=e_2,\sigma ,\Delta ⟩\Downarrow ⟨(),{\sigma }_2[\ell \mapsto v],{\Delta }_2⟩}(\text{E-Assign})$$

Two names may hold the same location, so a write through one is visible through the other — the aliasing the store model makes possible. Dereferencing or assigning through a value that is not a location is stuck.

Loops

while evaluates its condition; on false it stops with (), and on true it runs the body (whose value is discarded and is ()), then repeats against the resulting store:

$$\frac{\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\text{false},{\sigma }_1,{\Delta }_1⟩}{\rho ⊢⟨\text{while}{e}_1{e}_2,\sigma ,\Delta ⟩\Downarrow ⟨(),{\sigma }_1,{\Delta }_1⟩}(\text{E-While-False})$$

$$\frac{\begin{array}{c}\rho ⊢⟨e_1,\sigma ,\Delta ⟩\Downarrow ⟨\text{true},{\sigma }_1,{\Delta }_1⟩\\ \rho ⊢⟨e_2,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v,{\sigma }_2,{\Delta }_2⟩\\ \rho ⊢⟨\text{while}{e}_1{e}_2,{\sigma }_2,{\Delta }_2⟩\Downarrow ⟨(),{\sigma }_3,{\Delta }_3⟩\end{array}}{\rho ⊢⟨\text{while}{e}_1{e}_2,\sigma ,\Delta ⟩\Downarrow ⟨(),{\sigma }_3,{\Delta }_3⟩}(\text{E-While-True})$$

By the $\mathsf{Ret}$ convention, a return inside the body abandons the loop: the body premise yields $⟨\mathsf{Ret}w,{\sigma }_2,{\Delta }_2⟩$, so the whole while does, and the remaining iterations do not run.

for x in e evaluates the iterable to a list, then walks it, binding x to each element. Once the iterable is a value, two rules drive the walk (a list value stands in the in position as an intermediate configuration):

$$\frac{\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨v_{list},{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨\text{for}x\text{in}{v}_{list}{e}_b,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨(),{\sigma }^{\prime },{\Delta }^{\prime }⟩}{\rho ⊢⟨\text{for}x\text{in}e{e}_b,\sigma ,\Delta ⟩\Downarrow ⟨(),{\sigma }^{\prime },{\Delta }^{\prime }⟩}(\text{E-For})$$

$$\frac{}{\rho ⊢⟨\text{for}x\text{in}[]e_b,\sigma ,\Delta ⟩\Downarrow ⟨(),\sigma ,\Delta ⟩}(\text{E-For-Nil})$$

$$\frac{\rho [x\mapsto v_h]⊢⟨e_b,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }_1,{\Delta }_1⟩\rho ⊢⟨\text{for}x\text{in}{v}_t{e}_b,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨(),{\sigma }_2,{\Delta }_2⟩}{\rho ⊢⟨\text{for}x\text{in}(v_h::v_t)e_b,\sigma ,\Delta ⟩\Downarrow ⟨(),{\sigma }_2,{\Delta }_2⟩}(\text{E-For-Cons})$$

A return in the body propagates out by the same convention, abandoning the rest of the iteration. Iterating a non-list is stuck. The relational form for q e_b walks the solutions of a query instead of a list; its rule is with the relations.

return

return e evaluates e and wraps the value as a $\mathsf{Ret}$ outcome, which the conventions above carry outward until a function boundary catches it:

$$\frac{\rho ⊢⟨e,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }^{\prime },{\Delta }^{\prime }⟩}{\rho ⊢⟨\text{return}e,\sigma ,\Delta ⟩\Downarrow ⟨\mathsf{Ret}v,{\sigma }^{\prime },{\Delta }^{\prime }⟩}(\text{E-Return})$$

That return is legal only inside a function body is checked rather than evaluated: a $\mathsf{Ret}$ that reaches the top level with no function boundary to catch it is a static error, ruled out before evaluation.

Functions and application

A lambda evaluates, with no effect, to a closure that captures the current environment — the source of Bridger’s lexical scope, since the body will later run under the environment of the lambda’s definition rather than its call:

$$\frac{}{\rho ⊢⟨\lambda \vec{x}.e,\sigma ,\Delta ⟩\Downarrow ⟨⟨\lambda \vec{x}.e,\rho ⟩,\sigma ,\Delta ⟩}(\text{E-Lam})$$

A named fn is reached through E-Var: hoisting bound it to its closure in the program environment, so f evaluates to that closure and is applied by the same rule as a lambda. Application evaluates the operator to a closure, then the arguments left to right, then the body under the captured environment extended with the parameters; a return in the body is caught here and becomes the call’s value. When the operator evaluates to a relation value instead, the application is the hole-free query $R(e_1,\dots ,e_n)$ of E-Query-True/False, so path(0, 3) is a query exactly when path resolves to the relation — a local of that name shadows it, as it would a function:

$$\frac{\begin{array}{c}\rho ⊢⟨e_0,{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨⟨\lambda \vec{x}.e_b,{\rho }^{\prime }⟩,{\sigma }_0^{\prime },{\Delta }_0^{\prime }⟩\\ \rho ⊢⟨e_i,{\sigma }_{i-1}^{\prime },{\Delta }_{i-1}^{\prime }⟩\Downarrow ⟨v_i,{\sigma }_i^{\prime },{\Delta }_i^{\prime }⟩(1\le i\le n)\\ {\rho }^{\prime }[\vec{x}\mapsto \vec{v}]⊢⟨e_b,{\sigma }_n^{\prime },{\Delta }_n^{\prime }⟩\Downarrow ⟨r,{\sigma }^{\prime },{\Delta }^{\prime }⟩\end{array}}{\rho ⊢⟨e_0(e_1,\dots ,e_n),{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨\mathsf{Val}(\mathrm{unwrap}r),{\sigma }^{\prime },{\Delta }^{\prime }⟩}(\text{E-App})$$

where $\mathrm{unwrap}(\mathsf{Val}v)=\mathrm{unwrap}(\mathsf{Ret}v)=v$: whether the body finished normally or hit return, the application yields that value as a $\mathsf{Val}$, so the $\mathsf{Ret}$ never escapes the function it belongs to. Applying a value that is not a closure, or supplying the wrong number of arguments, is stuck.

A constructor application C(e_1, …, e_n) builds a tagged value rather than calling code — the constructor C comes from a type definition, and evaluation collects its arguments:

$$\frac{\rho ⊢⟨e_i,{\sigma }_{i-1},{\Delta }_{i-1}⟩\Downarrow ⟨v_i,{\sigma }_i,{\Delta }_i⟩(1\le i\le n)}{\rho ⊢⟨C(e_1,\dots ,e_n),{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨C(v_1,\dots ,v_n),{\sigma }_n,{\Delta }_n⟩}(\text{E-Con})$$

Constructors and pattern matching

match evaluates its scrutinee, then tries the arms top to bottom, taking the first whose pattern matches and whose guard holds. Pattern matching is the auxiliary relation

$$\mathrm{match}(p,v)=\theta \text{ or }\perp$$

giving a binding $\theta$ (a finite map from the pattern’s variables to values) when v fits p, and $\perp$ when it does not. Its clauses:

$$\begin{array}{rl}\mathrm{match}(\_,v)& =\varnothing \\ \mathrm{match}(x,v)& =\{x\mapsto v\}\\ \mathrm{match}(lit,v)& =\varnothing \text{if}v=lit,\text{else}\perp \\ \mathrm{match}(p_1\mid p_2,v)& =\mathrm{match}(p_1,v)\text{if}\mathrm{match}(p_1,v)\ne \perp ,\text{else}\mathrm{match}(p_2,v)\\ \mathrm{match}(C(p_1,\dots ,p_n),C(v_1,\dots ,v_n))& ={⨄}_i\mathrm{match}(p_i,v_i)\\ \mathrm{match}((p_1,\dots ,p_n),(v_1,\dots ,v_n))& ={⨄}_i\mathrm{match}(p_i,v_i)\\ \mathrm{match}(p_1::p_2,v_h::v_t)& =\mathrm{match}(p_1,v_h)\uplus \mathrm{match}(p_2,v_t)\\ \mathrm{match}(S\{f_i:p_i\},S\{\dots ,f_i=v_i,\dots \})& ={⨄}_i\mathrm{match}(p_i,v_i)\end{array}$$

A constructor pattern matches only its own constructor (a different one gives $\perp$); a list pattern $[p_1,\dots ,p_k]$ matches a list of exactly $k$ elements, and $[p_1,\dots ,p_k,\dots x]$ a list of at least $k$, binding x to the remaining tail as a list. A struct pattern names a subset of the fields, each at most once, and constrains only those (unchecked, a pattern naming a field the struct lacks simply fails to match); fields it omits may be anything. An or-pattern $p_1\mid p_2$ requires both sides to bind the same variables at the same types. Patterns are linear — a variable appears at most once in one pattern, a list pattern’s ...rest binder included — so the unions $⨄$ never collide. Both are static checks (T-Match). Any structural mismatch yields $\perp$.

The match rule takes the first arm $j$ whose pattern matches and whose guard (if present) evaluates to true. A guard is pure — the purity judgment is required of every guard, as of every rule filter — so a failed guard leaves the store and the database as the scrutinee left them:

$$\frac{\begin{array}{c}\rho ⊢⟨e_0,\sigma ,\Delta ⟩\Downarrow ⟨v,{\sigma }_1,{\Delta }_1⟩\\ \mathrm{match}(p_j,v)={\theta }_j\rho \cup {\theta }_j⊢⟨g_j,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨\text{true},{\sigma }_1,{\Delta }_1⟩\\ \mathrm{match}(p_k,v)=\perp \text{or its guard is }\text{false}(k<j)\\ \rho \cup {\theta }_j⊢⟨e_j,{\sigma }_1,{\Delta }_1⟩\Downarrow ⟨v^{\prime },{\sigma }_2,{\Delta }_2⟩\end{array}}{\rho ⊢⟨\text{match}{e}_0\{p_1[\text{if}{g}_1]\Rightarrow e_1,\dots \},\sigma ,\Delta ⟩\Downarrow ⟨v^{\prime },{\sigma }_2,{\Delta }_2⟩}(\text{E-Match})$$

An arm with no guard is the case $g_j=\text{true}$. When no arm matches, no rule applies and evaluation is stuck on the non-exhaustive match; the untyped evaluator reports it at run time, and the checker’s exhaustiveness check (T-Match) rules it out for the programs it accepts.

Structs, fields, and methods

A struct literal evaluates its fields in source order and builds a struct value whose fields are held in declaration order, so two literals that name the same fields in different orders build the same value — under ==, in a pattern, and when printed. A literal names every declared field exactly once; a missing or unknown field is stuck. Field access reads one back:

$$\frac{\rho ⊢⟨e_i,{\sigma }_{i-1},{\Delta }_{i-1}⟩\Downarrow ⟨v_i,{\sigma }_i,{\Delta }_i⟩(1\le i\le n)}{\rho ⊢⟨S\{f_1:e_1,\dots ,f_n:e_n\},{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨S\{f_1=v_1,\dots ,f_n=v_n\},{\sigma }_n,{\Delta }_n⟩}(\text{E-Struct})$$

A method call e0.m(e1, …, en) evaluates the receiver and the arguments, then runs the method whose impl matches the receiver’s runtime head type. Let $\mathrm{head}(v_0)$ be that type — a struct name, a constructor’s type, or a built-in — and $\mathrm{lookup}(\mathrm{head}(v_0),m)$ the method the matching impl provides. The body runs with self bound to the receiver, catching return as an application does; as with an application, the wrong number of arguments is stuck. When e0 is a bare struct or type name, or one of the built-in names Int, Bool, and String, the call is an associated call: the name is the head, the method is one declared without self, and its body runs with only the arguments bound. A method with self called on a type name, and one without called on a value, are both stuck:

$$\frac{\begin{array}{c}\rho ⊢⟨e_0,{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨v_0,{\sigma }_0^{\prime },{\Delta }_0^{\prime }⟩\\ \rho ⊢⟨e_i,{\sigma }_{i-1}^{\prime },{\Delta }_{i-1}^{\prime }⟩\Downarrow ⟨v_i,{\sigma }_i^{\prime },{\Delta }_i^{\prime }⟩(1\le i\le n)\\ \mathrm{lookup}(\mathrm{head}(v_0),m)=⟨\lambda \text{self},\vec{x}.e_b,{\rho }^{\prime }⟩\\ {\rho }^{\prime }[\text{self}\mapsto v_0,\vec{x}\mapsto \vec{v}]⊢⟨e_b,{\sigma }_n^{\prime },{\Delta }_n^{\prime }⟩\Downarrow ⟨r,{\sigma }^{\prime },{\Delta }^{\prime }⟩\end{array}}{\rho ⊢⟨e_0.m(e_1,\dots ,e_n),{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨\mathsf{Val}(\mathrm{unwrap}r),{\sigma }^{\prime },{\Delta }^{\prime }⟩}(\text{E-Method})$$

Resolution is by the receiver’s runtime type, and coherence — at most one impl of a given trait instance per head type; one definition of an inherent method name per head type, and of a trait’s method per head type and instance, across all of its impl blocks; both checked statically — makes that method the same one a static, declared-type dispatch would choose. A method name belongs to one trait per head: a trait may provide it at several instances, but a second trait’s method of that name, an inherent one, or a built-in conformance’s cannot join it on the head, since a call through a bound is dispatched by head and name alone. An impl therefore extends a head type: a declared type or struct, Int, Bool, String, (), or the list head. A tuple, a function type, a reference, and a bare type parameter have no head, so an impl may not name one. An impl may extend a head at a particular instance, impl Len for Seq<Int>, or generically, impl<T> Len for [T]: a call on a receiver of known type is resolved to the impl covering it when the program is checked, and the evaluator runs the method the checker chose, so the two dispatch strategies agree on the code that runs. A trait may have several impls for one head only at instances its type arguments tell apart by their outermost form — a head, or a tuple, function, or reference type — From<[T]> and From<Map<K, V>> for Seq<…> — so a generic instance such as From<T> is the only one, and two impls of a trait without arguments are one too many. A call through a bound T: Tr runs the head’s method of that name, so a bound met by a type whose head implements Tr at several instances is rejected, whether the bound is a call’s or an impl’s own; a ? chooses its from by the error type, and a direct call chooses by its arguments or is ambiguous. (Unchecked, a run dispatches on the head alone and may take the first impl declared, and e? returns an Err payload as it is, converting nothing; passing the chosen impl along with a bounded call — dictionary passing — would lift the restriction and is left as further reading.) The built-in conformances count as impls for coherence: a program may declare neither impl Ord for Int nor an inherent cmp on Int, and likewise for the other built-in types and Len. An impl Tr for τ conforms to its trait: it provides every method Tr declares, each with the trait’s signature under Self = τ and the trait’s type arguments, and no method the trait lacks; a bounded call through Tr is therefore always answered. The built-in types carry the prelude’s trait methods without an impl: with no impl for the receiver, cmp on Int, String, or Bool and length on String or a list resolve to primitives. A call to a method neither an impl nor a built-in conformance provides is stuck.

Relations

The Datalog fragment reads and extends a global relation database $\Delta$, a set of ground facts $R(v_1,\dots ,v_n)$. Every rule threads $\Delta$; the rules here are the ones that change it, where the rest pass it along untouched. The chapters before the relations material present the $\Delta$ -free slice.

A program’s rule definitions form a fixed rule set $P$. Together with the current facts $\Delta$, they denote a set of derivable facts: the least set $M(P,\Delta )$ that contains $\Delta$ and is closed under every rule, where a rule $H\text{ :- }{B}_1\text{ and }\dots \text{ and }{B}_m$ derives $H\theta$ whenever a substitution $\theta$ makes each generator atom $B_i\theta$ a member and each pure filter $B_i\theta$ evaluate to true under ${\rho }_0[\theta ]$ — the program environment extended by the substitution. A rule is a top-level definition and closes over ${\rho }_0$ like a fn body; the locals in scope where a query is asked are not visible to it. $M(P,\Delta )$ is the least fixpoint of that immediate-consequence operator; it exists and is unique because the operator is monotone (all recursion is positive — negation is confined to pure filters), and it is finite because the fragment is range-restricted and terminating, the subject of the chapter on rule bodies and safety. Every query reads $M(P,\Delta )$; an implementation may compute it once and reuse it until $\Delta$ or $P$ changes, which a pure filter cannot tell.

add evaluates a relation atom’s arguments to values and inserts the ground fact; clear drops a relation’s facts. Both change $\Delta$ and yield (). An atom — in add or in a query — with other than the relation’s number of columns is stuck:

$$\frac{\rho ⊢⟨e_i,{\sigma }_{i-1},{\Delta }_{i-1}⟩\Downarrow ⟨v_i,{\sigma }_i,{\Delta }_i⟩(1\le i\le n)}{\rho ⊢⟨\text{add}R(e_1,\dots ,e_n),{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨(),{\sigma }_n,{\Delta }_n\cup \{R(v_1,\dots ,v_n)\}⟩}(\text{E-AddFact})$$

$$\frac{}{\rho ⊢⟨\text{clear}R,\sigma ,\Delta ⟩\Downarrow ⟨(),\sigma ,\Delta \setminus \{R(\vec{v})\mid \vec{v}\}⟩}(\text{E-Clear})$$

A rule with no body is a base fact of $P$, not of $\Delta$: clear leaves it. In add, a query, solutions, and for, the bound arguments evaluate left to right, threading the store and $\Delta$, once per form — a for evaluates them once, not per solution — and the query reads $M(P,\Delta )$ as the arguments left it, so an add inside an argument is seen by that query. A filter whose evaluation is stuck makes the query, and the program, stuck. Global initializers may add, clear, and query, in initialization order; a global holding solutions q keeps the list as it was then.

add is monotone by design — facts accumulate and are never retracted individually — which is what lets a query denote a least fixpoint; clear resets a relation wholesale between uses. The name R in each of these forms resolves in $\rho$ like any other: ${\rho }_0$ binds it to the relation, a local of the same name shadows that binding, and a form whose name is bound to anything but a relation is stuck. A query atom q carries holes ?x; a solution is a substitution $\theta$ for its holes with $q\theta \in M(P,\Delta )$. A hole named twice is one variable, bound to one value at every position it names, and the query’s holes are its distinct names in order of first appearance. An anonymous hole ? binds no name: a solution is an assignment to the named holes, each distinct assignment counted once, so solutions r(?) is [()] when some fact matches and for r(?) { … } runs its body once. solutions q returns the list of solutions — the tuples of hole values, in that order; a single hole gives the value itself, and a hole-free query gives (), so its list is [()] when the fact is derivable and [] when it is not. A query in boolean position is true exactly when it has a solution: for a hole-free query, when its fact is derivable; with holes, when some filling of them is.

$$\frac{\{{\theta }_1,\dots ,{\theta }_k\}=\mathrm{sols}(q,M(P,\Delta ))\text{in canonical order}}{\rho ⊢⟨\text{solutions}q,\sigma ,\Delta ⟩\Downarrow ⟨[{\bar{\theta }}_1,\dots ,{\bar{\theta }}_k],\sigma ,\Delta ⟩}(\text{E-Solutions})$$

$$\frac{\mathrm{sols}(q,M(P,\Delta ))\ne \varnothing }{\rho ⊢⟨q,\sigma ,\Delta ⟩\Downarrow ⟨\text{true},\sigma ,\Delta ⟩}(\text{E-Query-True})\frac{\mathrm{sols}(q,M(P,\Delta ))=\varnothing }{\rho ⊢⟨q,\sigma ,\Delta ⟩\Downarrow ⟨\text{false},\sigma ,\Delta ⟩}(\text{E-Query-False})$$

The canonical order is the total order on data values: integers numerically, false before true, strings lexicographically, tuples and lists lexicographically with a shorter prefix first, constructor values by constructor name and then by arguments, struct values by name and then by fields in declaration order, and references by location. Solutions are ordered by their hole values, first hole first, so the list depends on $M(P,\Delta )$ alone and never on the order the facts were added or derived.

The relational for q e_b walks the solutions of q in that same canonical order, binding the hole variables of each solution and running the body once per solution, threading the store and $\Delta$ through:

$$\frac{\begin{array}{c}\mathrm{sols}(q,M(P,{\Delta }_0))=[{\theta }_1,\dots ,{\theta }_k]\text{in canonical order}\\ \rho \cup {\theta }_i⊢⟨e_b,{\sigma }_{i-1},{\Delta }_{i-1}⟩\Downarrow ⟨v_i,{\sigma }_i,{\Delta }_i⟩(1\le i\le k)\end{array}}{\rho ⊢⟨\text{for}q{e}_b,{\sigma }_0,{\Delta }_0⟩\Downarrow ⟨(),{\sigma }_k,{\Delta }_k⟩}(\text{E-For-Query})$$

A return in the body abandons the remaining solutions by the $\mathsf{Ret}$ convention. The body neither reads a partially built relation nor writes one it is iterating — for iterates a fixed $M(P,{\Delta }_0)$ — so the iteration order is the only thing the canonical ordering pins down, and it pins it down precisely for reproducibility.