Expression language: denotational semantics

In plain terms

The expression language panproto-expr is what you use to describe field-level transforms inside a migration (“the new full_name field is the old first plus a space plus the old last”) and predicates inside a query (“only records where created_at > '2024-01-01'”). Everything in the language is pure: no IO, no mutation, no clock reads, no random numbers. Two expressions that look the same always do the same thing. Every expression terminates within a fixed number of evaluation steps.

This page describes what those properties mean and what the evaluator actually computes.

Surface syntax

The Haskell-style surface, parsed by panproto-expr-parser:

expr  ::= literal
        | ident
        | expr expr                    -- application
        | "\\" ident "->" expr         -- lambda
        | "let" ident "=" expr "in" expr
        | "if" expr "then" expr "else" expr
        | "case" expr "of" alts        -- pattern match
        | builtin "(" expr,... ")"     -- builtin application
        | expr "." ident               -- field access
        | expr "[" expr "]"            -- index
literal ::= int | float | str | bool | "null"
        | "[" expr,... "]"             -- list
        | "{" ident ":" expr,... "}"   -- record

The parser desugars if c then a else b to a Match over a boolean scrutinee with two arms, and case e of ... to a Match directly. There is no separate If or Case node in the abstract syntax.

Abstract syntax

pub enum Expr {
    Var(Arc<str>),
    Lam(Arc<str>, Box<Self>),
    App(Box<Self>, Box<Self>),
    Lit(Literal),
    Record(Vec<(Arc<str>, Self)>),
    List(Vec<Self>),
    Field(Box<Self>, Arc<str>),
    Index(Box<Self>, Box<Self>),
    Match { scrutinee: Box<Self>, arms: Vec<(Pattern, Self)> },
    Let { name: Arc<str>, value: Box<Self>, body: Box<Self> },
    Builtin(BuiltinOp, Vec<Self>),
}

Match covers both if/then/else and case/of; pattern matching is the only branching primitive. Each arm pairs a Pattern (whose variants include Wildcard, Var, Lit, Record, List, and Constructor) with a body expression. The full enum lives at crates/panproto-expr/src/expr.rs.

Type system

The type-formation grammar:

$$\tau ::=\mathsf{Int}\mid \mathsf{Float}\mid \mathsf{Str}\mid \mathsf{Bool}\mid \mathsf{Null}\mid \mathsf{Any}\mid \mathsf{List}\tau \mid \mathsf{Record}\mid \tau \to \tau$$

A typing context $\Gamma$ is a finite map from variable names to types. The typing relation $\Gamma ⊢e:\tau$ is defined inductively by the usual rules; selected:

$$\frac{}{\Gamma ⊢n:\mathsf{Int}}(\text{T-Int})\frac{x:\tau \in \Gamma }{\Gamma ⊢x:\tau }(\text{T-Var})\frac{\Gamma ,x:{\tau }_1⊢e:{\tau }_2}{\Gamma ⊢\lambda x.e:{\tau }_1\to {\tau }_2}(\text{T-Lam})$$

$$\frac{\Gamma ⊢e_1:{\tau }_1\to {\tau }_2\Gamma ⊢e_2:{\tau }_1}{\Gamma ⊢e_1{e}_2:{\tau }_2}(\text{T-App})\frac{\Gamma ⊢e:{\tau }_1\Gamma ,x:{\tau }_1⊢e^{\prime }:{\tau }_2}{\Gamma ⊢\mathsf{let}x=e\mathsf{in}{e}^{\prime }:{\tau }_2}(\text{T-Let})$$

Builtin signatures have type schemes given in reference/expression-language; each Builtin(op, \overline{e}) rule plugs in $op$’s scheme and checks that the arguments match.

Semantic domain

Let $\mathsf{Val}$ be the recursive sum

$$\mathsf{Val}\cong \mathbb{Z}+\mathbb{R}+\mathsf{String}+\mathbb{B}+\{\star \}+\mathsf{List}(\mathsf{Val})+\mathsf{Record}(\mathsf{Val})+[\mathsf{Val}\rightharpoonup \mathsf{Val}]$$

interpreting Null as the singleton $\{\star \}$ and the function space as partial continuous maps. Lift to ${\mathsf{Val}}_{\perp }=\mathsf{Val}+\{\perp \}$ to adjoin a bottom for divergence under the step budget. Environments live in $\mathsf{Env}=\mathsf{Var}\rightharpoonup \mathsf{Val}$, and ranked environments in ${\mathsf{Env}}_n=\mathsf{Env}\times \mathbb{N}$ to track the remaining step budget.

Semantic function

The denotational semantics is the family

$$[[\cdot ]]:\mathsf{Expr}\to {\mathsf{Env}}_n\to {\mathsf{Val}}_{\perp }$$

defined by structural recursion on $\mathsf{Expr}$. Write ${\rho }_n=(\rho ,n)$ and ${\rho }_n\downarrow 1=(\rho ,n-1)$ for the budget decrement. The equations:

$$\begin{array}{rl}[[\mathsf{Lit}(c)]]{\rho }_n& =c\\ [[\mathsf{Var}(x)]]{\rho }_n& =\rho (x)\\ [[\mathsf{Lam}(x,e)]]{\rho }_n& =\lambda v.[[e]](\rho [x\mapsto v]{)}_n\\ [[\mathsf{Let}(x,e_1,e_2)]]{\rho }_n& =[[e_2]](\rho [x\mapsto [[e_1]]{\rho }_n]{)}_{n-1}\\ [[\mathsf{App}(e_1,e_2)]]{\rho }_n& =([[e_1]]{\rho }_n)([[e_2]]{\rho }_n)\\ [[\mathsf{Match}(e,\overline{(p_i,b_i)})]]{\rho }_n& =\mathsf{matchArms}([[e]]{\rho }_n,\overline{(p_i,b_i)},{\rho }_{n-1})\\ [[\mathsf{List}(\overline{e})]]{\rho }_n& =[[[e_i]]{\rho }_n{]}_i\\ [[\mathsf{Field}(e,x)]]{\rho }_n& =([[e]]{\rho }_n).x\\ [[\mathsf{Index}(e,i)]]{\rho }_n& =([[e]]{\rho }_n)[[[i]]{\rho }_n]\\ [[\mathsf{Builtin}(op,\overline{e})]]{\rho }_n& =apply\_builtin(op,\overline{[[e_i]]{\rho }_n})\\ [[e]](\rho ,0)& =\perp \text{(budget rule)}\end{array}$$

The budget rule fires before any equation if the remaining steps are zero; otherwise the relevant equation applies and the recursive sub-denotations are evaluated with the budget decremented. Operationally this is EvalState::tick in crates/panproto-expr/src/eval.rs; when $\perp$ is returned the implementation surfaces ExprError::StepLimitExceeded(max_steps).

The auxiliary $\mathsf{matchArms}$ is the standard pattern-match search: try each $(p_i,b_i)$ in order, attempting to unify $p_i$ against the scrutinee value; on the first success bind the pattern variables into $\rho$ and evaluate $b_i$; on exhaustion raise NonExhaustiveMatch. The auxiliary $apply\_builtin$ is the partial function defined in crates/panproto-expr/src/builtin.rs.

Builtin side conditions

The builtins listed under reference/expression-language are individually total or partial. The partial ones return a non-$\perp$ error rather than $\perp$:

• Div, Mod with zero divisor: DivisionByZero.
• Integer arithmetic overflow: Overflow (i64::checked_*).
• *ToInt / *ToFloat on unparseable input: ParseError.
• List index out of bounds: IndexOutOfBounds; list operations past the configured maximum: ListLengthExceeded.
• Record access on a missing field: FieldNotFound.
• Match exhaustion: NonExhaustiveMatch.
• App of a non-function value: NotAFunction.

Errors are distinct from $\perp$. $\perp$ models resource exhaustion (StepLimitExceeded and DepthExceeded); errors model defined failure and propagate as Err(ExprError) from the implementation.

Soundness

The evaluator satisfies:

• Type preservation. If $\Gamma ⊢e:\tau$ and $\rho \models \Gamma$ and $\rho ⊢e\Downarrow v$ with $v\ne \perp$, then $v\in [[\tau ]]$.
• Totality (within the budget). For every well-typed $e$ and well-typed $\rho$, $[[e{]]}_{\rho }$ terminates in finitely many steps with either a value or $\perp$.
• Determinism. If $\rho ⊢e\Downarrow v_1$ and $\rho ⊢e\Downarrow v_2$ then $v_1=v_2$.

Type preservation is enforced by the type-checker in crates/panproto-expr/src/typecheck.rs and by builtin signatures rejecting ill-typed arguments. Totality follows from the budget rule. Determinism follows from the absence of mutation and IO.

What is intentionally not modelled

• Performance. Two expressions can have the same denotation but very different cost. The semantics fixes only what is computed, not how much it costs.
• Step-budget tuning. The budget is a parameter set at the outermost call. The semantics treats it as fixed; the language itself does not expose it.
• Floating-point determinism across architectures. Float operations follow IEEE 754, but bit-level reproducibility across hardware is not guaranteed.

See also

• Reference: expression-language for the builtin catalogue.
• How-to: apply field transforms for usage.
• Lens DSL for how panproto-expr appears inside lens specifications.