DSL Programs and Let-Expressions¶

This page covers program block syntax: program declarations and their effect signatures, the bind / observe / marginalize / let steps that make up a program body, the axis-role clause that configures structured priors and likelihoods, the let-expression language with its complete set of primitives, and factor expressions.

The grammar summary lives in the DSL overview; declarations of objects, morphisms, kernels, and combinators are detailed in DSL Declarations.

Program declarations¶

A program block defines a probabilistic program. The body is a sequence of steps (bind, observe, let, marginalize) followed by return. Each step is a Kleisli arrow on the accumulated random-variable context $\Phi$; the program denotes the composite $\Gamma \to \mathcal{G}(\tau_2)$ in Kern.

program my_prog : X -> Y
    sample mu <- LogitNormal(mu=0.0, sigma=1.0)
    sample x <- Normal(loc=mu, scale=1.0)

    return x

program with_params(a, b) : (X * Z) -> Y
    let w = a

    sample x <- f(w)
    sample y <- g(x, b)
    return y

The compiled program is a MonadicProgram; see the monadic programs guide for the runtime contract (rsample, log_joint, the observations dict).

Effect signatures¶

A program declaration may carry an effects = [...] entry in its option block listing a subset of {Sample, Score, Marginal, Pure}. The compiler verifies that the body's actual effects are a subset of the declared set; effects=[Pure] rejects any sample, score, or marginal binds.

program prior : X -> Y [effects=[Sample]]
    sample mu <- Normal(loc=0.0, scale=1.0)
    return mu

program deterministic : X -> X [effects=[Pure]]
    let y = x
    return y

See the compositional effects guide for the algebraic basis of the effect system.

QIEC typed computations¶

The typed computation layer is what a program block elaborates to; a define writes such a computation directly. Its header gives a value result and an instance row, while perform names an operation through a lexical effect instance:

effect Tap
    ping : Int -> Int

instance tap : Tap

define echo(value : Int) : Int !{tap} =
    let answer <- perform tap.ping(value)
    return answer

The stable computation terms are return, let ... <- perform ..., bare perform sequencing, a call of a named computation let x <- f[statics](args), handle ... with ... in, with instance x : E in allocating a scoped instance, and indexed case with an explicit motive. Rows contain lexical instance names, as in !{tap}; an open row has the form !{tap | rho lacks tap}. The tail and each lacks constraint are checked rather than treated as comments.

A call is checked against the callee's signature instantiated at the call's static arguments, and the module's call graph is checked one strongly connected component at a time, so mutually recursive computations need no forward declaration; a recursive computation must reach a case branch or an if arm that does not call again, which is what lets it stop. A scoped instance may not survive in its body's row: the checker reports qiec-instance-escape for a body that still performs on it. A handler's clauses may be authored in the source with => bodies, each resuming as often as its grade admits (0, aff, 1, or omega), and a foreign handler's clauses are process-local attachments. A program elaborates to such a computation; a program draws from another with sample x <- sub(args) (or sample (a, b) <- sub for a pair), which runs sub's steps in place under names of its own (sub's local z becomes x$z), and calls a computation with let x <- f(args).

Eight dynamic targets execute the full computation graph through generated target runtimes. Stan lowers closed monomorphic effect-free scalar computations as user-defined functions and refuses every other feature under qiec:capability:<feature>:<name>; BUGS and JAGS refuse a call under call:graph:<name>. A module with QIEC declarations but no computation the program reaches remains valid on every target. The complete syntax appears in QVR computation reference and probabilistic-program reference.

Kleisli bind syntax¶

The sample keyword introduces a draw, and <- separates its binding pattern from the distribution call:

sample x <- Normal(loc=0.0, scale=1.0)

This step introduces x as a random variable distributed according to the given family. Indexed samples, scored observations, and scoped marginalizations use the same <- separator with their respective keywords.

Indexed bind (plate)¶

sample v : A <- Family(args) declares v as an $A$-indexed family of independent $F$-distributed draws. Categorically v : A \to \mathcal{G}(K) where K is the per-fiber codomain taken from the family; equivalently a single arrow $\mathbf{1} \to \mathcal{G}(K^A)$ via the natural isomorphism $\mathbf{Kern}(\mathbf{1}, K^A) \cong \mathbf{Kern}(A, K)$.

object Item : FinSet 1000
sample duration_incr : Item <- HalfNormal(scale=1.0)
sample by_subject    : Subject <- Normal(loc=0.0, scale=sigma)

Indexed observe¶

observe r : N <- Family(args) accumulates a batched log-likelihood: a sub-probability kernel $\Phi \to \mathcal{G}_{\le 1}(\Phi)$ with score $\prod_{n \in N} p_F(r_{\mathrm{obs}}(n); \theta(n, \phi))$. The response buffer r is supplied at runtime via the observations dict passed to MonadicProgram.rsample, MonadicProgram.log_joint, or ELBO.forward. Family arguments may use bracket-indexed sections theta[N] to refer to plate variables.

observe cloze_resp : RespCloze <- Bernoulli(probs=intercept_cloze)

Scoped marginalize¶

marginalize c : A <- F(args) followed by an indented body introduces a coordinate c bound to a kernel F(args), optionally A-indexed, with the indented block as its integration scope. At the end of the scope the coordinate is pushed forward through the projection $\pi : \Phi \times C \to \Phi$, integrating it out by log-sum-exp on the log-likelihood (discrete) or fibrewise integration (continuous); c then falls out of scope.

marginalize class : Item <- Categorical(logits=class_logits)
    observe r : N <- Bernoulli(probs=theta[class[N]])

The grouped form with [over=G] and per-observe [via=<idx>] options is the fibred marginalization construct; see hierarchical programs.

Indexed gather in `let`¶

A let-expression of the form arr[idx] denotes the Kleisli pullback of a plate variable along a finite fibration. For a plate v : A -> B and an index morphism $\iota : N \to A$, the gather $\iota^* v = v \circ \iota$ is itself a Kern-morphism $N \to B$.

sample by_verb : Verb <- Normal(loc=0.0, scale=sigma)
let intercept_for_item = by_verb[verb_of_item]

Parametric programs¶

A program declaration whose parameter list contains typed parameters denotes a dependent family of kernels rather than a single kernel:

\[ \llbracket P \rrbracket \;:\; \prod_{p_1 : P_1} \cdots \prod_{p_k : P_k} \mathbf{Kern}\bigl(\mathrm{dom}(p), \mathrm{cod}(p)\bigr). \]

Three parameter universes are available:

Kind	Universe	Quantifies over
`FinSet`, `Space`, `Object`	object of the relevant subcategory	the carrier of a plate
`Real`, `Nat`	hom-object of scalar type	a hyperparameter value
`Mor[A, B]`	the hom-set $\mathbf{Kern}(A, B)$	a kernel passed in by name

Parametric programs are not compiled to runtime MonadicPrograms in isolation; the compiler stores them as templates and inlines them at each call site:

sample v <- template(arg1, arg2, ...)

At each call site the template's body is substituted (formal parameters to actual arguments) and α-renamed (internal latents are prefixed by v$, the return variable is renamed to v directly). The renamed step list is inlined into the caller, so distinct call sites contribute distinct factors to the parent's joint kernel: fresh latents per use, no inadvertent tying.

# Parametric random-intercepts template: one HalfNormal scale and
# a per-level Normal(loc=0, scale=sigma) plate, polymorphic over the grouping
# object G and the half-normal hyperparameter scale.
program random_intercepts (G : FinSet, scale : Real) : G -> 1
    sample sigma <- HalfNormal(scale=scale)
    sample v : G <- Normal(loc=0.0, scale=sigma)
    return v

Worked hierarchical examples (crossed random intercepts, grouped marginalization over discrete classes) live in the hierarchical programs guide.

Posterior blocks¶

A program name(latents) : domain -> codomain declaration denotes a deterministic post-conditioning kernel. The over = model entry in its option block marks the program as consuming the named model's latents; the consumed latents appear as data parameters in the parameter list. The effects=[Pure] signature rejects any sample, score, or marginal binds; the body is restricted to let (and marginalize over its own scope). Categorically it is a Kern-morphism $\text{Latents} \to \tau_{\mathrm{out}}$ that lifts to $\text{Data} \to \mathcal{G}(\tau_{\mathrm{out}})$ by post-composition with the model's posterior kernel $q(\theta \mid \mathrm{data})$.

object Logits4 : Real 4

program scored : Item -> Logits4
    sample raw_logits <- Normal(loc=0.0, scale=1.0)
    return raw_logits

program class_probs(raw_logits) : Item -> Logits4 [effects=[Pure], over=scored]
    let probs = softmax(raw_logits)
    return probs

The data parameter raw_logits names the model latent the body consumes; the runtime supplies a per-sample snapshot of the model's trace.

Axis-role clause: `over` and `iid_over`¶

Every distribution-bearing form (kernel and latent-prior morphism declarations, sample / observe / marginalize steps) accepts two option-block keys that configure how the family's axes decompose: over and iid_over. Both live inside the bracketed option block, before any trailing ~ Family(...) initializer:

... [..., over=<axes>, iid_over=<axes>] ~ Family(args)

over=<axes> names the event axes: the axes on which the family's joint structure lives. The axis count must match the family's declared event_rank (0 for scalar families like Normal / Beta / Gamma; 1 for vector families like MultivariateNormal, Dirichlet, ConditionalGaussianProcess (named GP in QVR), or ConditionalHorseshoe; 2 for matrix families like MatrixNormal, Wishart, InverseWishart). A single axis is written bare (over=A); multiple axes use a bracketed list (over=[A, B]). The positional ordering of over axes corresponds positionally to the family's declared event-axis ordering (for asymmetric families like MatrixNormal, the first axis is the row axis, the second the column axis). The full event-rank table lives in continuous families.

iid_over=<axes> is an optional readability assertion naming the batch axes (the complement of over). Any axis not in over is batched by default, which categorically is a product of independent distributions on that axis. On a sample step, the : A annotation beside an over clause is the batch plate: sample rows : Doc <- Dirichlet(concentration=1.0) [over=Topic] draws one point of the Topic-simplex per document, while an annotation naming one of the over axes restates it. Without an over, the annotation on a vector family names the family's own axis when nothing else fixes it (sample pi : K <- Dirichlet(concentration=1.0) draws one K-simplex point) and the batch plate when the arguments fix the event otherwise (sample pc : Item <- Dirichlet(concentration=[1.0, 2.0, 3.0]) draws one three-simplex point per item).

A vector family's single parameter is named like every other family parameter. Write Dirichlet(concentration=[1.0, 2.0, 3.0]) for an explicit vector or Dirichlet(concentration=1.0) for a symmetric concentration at the dimension fixed by the step's plate or the program's declared codomain.

Axis names. Names resolve against the named factors of the surrounding morphism's dom and cod (or the type annotation : T on a sample / observe step). The reserved tokens dom and cod are shortcuts when that side is a single unfactored object; for a product-typed side, every factor must be named explicitly.

Categorical reading. The axis-role clause preserves the distinction between joint-on-a-product-space (the family's event with possibly non-trivial correlation) and product-of-independents (iid batches across an axis), and between a flat MVN over $\dim(A) \cdot \dim(B)$ with dense covariance versus a MatrixNormal with Kronecker structure $V \otimes U$. There is no auto-substitution between families with different event ranks. Renaming or refactoring a morphism's type invalidates axis references at type-check time rather than silently rebinding.

Compile-time errors. Two diagnostics fire here:

"axis count does not match family event_rank": the family declares event_rank k but over lists j ≠ k axes. Common when migrating from a flat MultivariateNormal (event_rank 1) to a matrix MatrixNormal (event_rank 2).
"unknown axis name(s) A in over": an over name is not a factor of the morphism's dom or cod. Resolve by renaming, or by using dom / cod if the side is a single unfactored object.

# Vector prior: 5-dim MVN over the codomain axis.
sample mu : Real 5 <- MultivariateNormal(loc=zeros, scale_tril=L) [over=cod]

# Matrix prior on a morphism: Kronecker MatrixNormal.
morphism W : Real 32 -> Real 64 [role=latent, over=[dom, cod]]
    ~ MatrixNormal(loc=loc, row_covariance=row_scale, col_covariance=col_scale)

# Per-row Dirichlet on a transition kernel: each row is a K-dim
# simplex independently, rows are iid.
morphism T : Real K -> Real K [role=latent, over=cod, iid_over=dom]
    ~ Dirichlet(concentration=alpha)

# MVN response per observation row.
observe y : N <- MultivariateNormal(loc=mu_hat, scale_tril=scale_tril) [over=cod]

Let expressions (arithmetic, primitives, and collections)¶

Inside a program block or a define computation, let bindings support arithmetic with standard operator precedence, unary negation, checked tensor primitives, and finite collection operations:

# arithmetic: +, -, *, /
let eta = mu + sigma * z_raw + lambda * shared_factor
let adjusted = (1.0 - lapse) * p_raw + 0.5 * lapse
let mean = (x + y + z) / 3.0
let negated = -raw_score

# built-in primitives
let prob = sigmoid(eta)
let positive = softplus(raw)
let log_rate = log(rate)
let magnitude = abs(x - 0.5)
let monotone = cumsum(increments)
let weights = softmax(logits)
let centered = map(xs, x -> x - mean)

Each let-builtin denotes a deterministic measurable map, lifted into the Kleisli category as a Dirac kernel.

Checked primitive reference¶

The checked registry defines the portable QIEC expression set. Operators and calls are resolved by argument type before execution or transpilation. Reductions act on the entire supplied tensor; rowwise operations act on its last axis. For a contraction over a named axis, use a typed contraction declaration.

Conversions and weights: real, int, weight, weight_value.

Arithmetic and comparisons: +, -, *, /, %, ==, !=, <, <=, >, >=, &&, ||; and the call forms pow, abs, min, and max.

Pointwise transcendentals: exp, expm1, log, log1p, log2, log10, sqrt, rsqrt, square, abs, sign, reciprocal, sin, cos, tan, asin, acos, atan, sinh, cosh, asinh, acosh, atanh, floor, ceil, round, trunc, erf, erfc, erfinv, lgamma, digamma.

Activations: relu, relu6, elu, selu, gelu, silu, mish, softplus, logsigmoid, softsign, sigmoid, and tanh.

Tensor reductions: sum, mean, min, max, prod, logsumexp.

Last-axis operations: softmax, log_softmax, cumsum, sort, normalize.

Finite collections: map, fold, length, and logsumexp_over are pure. traverse sequences a named computation and therefore appears on the right side of <-. See the collection reference for their typing and shape rules.

The eager PyTorch compiler also exposes the native-only operations alpha_dropout, amax, amin, argmax, argmin, celu, clamp, cummax, cummin, cumprod, dropout, flip, glu, hardshrink, hardsigmoid, hardswish, hardtanh, layer_norm, leaky_relu, neg, norm, prelu, rms_norm, rrelu, softmin, softshrink, std, swish, tanhshrink, threshold, and var. These are an attachment boundary, not portable QIEC primitives. If a program uses one, qvr check reports qiec-builtin:host-only rather than silently omitting the program from the checked module. Use qvr check --target TARGET before relying on a transpiler.

The capability registry lives in quivers.dsl.pure_builtins. Each entry records its eager implementation and arities, purity, shape action, checked QIEC form, and supported execution routes; eager dispatch and checked name resolution are derived from it. Calls resolve against this registry before module-scope callables. User-defined callable arity is checked at compile time.

Factor expressions: assembling indexed tensors¶

The factor expression in a let body builds a finite-domain-indexed tensor by evaluating a body once per tuple of index values. Categorically it is the left adjoint of indexing: while arr[i, j, ...] is the elimination rule for I_1 × ... × I_n -> body_type (Kleisli pullback of a plate variable along a finite fibration), factor is the introduction rule.

Uniform form¶

factor v_1 : I_1, v_2 : I_2, ..., v_n : I_n in <body>

denotes the tensor of shape (|I_1|, ..., |I_n|, *body_shape) whose value at position (i_1, ..., i_n) is <body> evaluated with v_k := i_k. The binder variables are integer-valued and visible only inside the body.

object Verb : FinSet 40
object Class : FinSet 4
# Per-verb, per-class scoring table: shape (40, 4).
let cell = factor v : Verb, cls : Class in coef[v, cls] * weight[cls]

Pattern-match form (single-axis)¶

When each cell of a single-axis factor carries a structurally different expression, the case form lets you state the per-index expressions side-by-side:

let class_probs = factor cls : Class in {
    0 -> (1.0 - prob_dur) * (1.0 - prob_telic_nodur),
    1 -> (1.0 - prob_dur) *        prob_telic_nodur,
    2 ->        prob_dur  * (1.0 - prob_telic_dur),
    3 ->        prob_dur  *        prob_telic_dur,
}

The case labels must cover {0, ..., |Index|-1} exactly; the compiler rejects gaps, duplicates, or out-of-range labels at compile time. Braces and comma separators delimit the cases. This is the natural syntax for structured categorical priors: each cell of a Class-shape probability vector is built from a different combination of upstream scalar latents.

Inline distributions¶

Bind and observe steps support inline distribution construction with any mix of literal and variable arguments. More than forty registered families accept literal-or-variable arguments at any position:

# all-literal (fixed): Unit -> codomain
sample x <- Normal(loc=0.0, scale=1.0)
sample p <- Beta(concentration1=2.0, concentration0=5.0)

# all-variable (direct): variables -> codomain
sample y <- Normal(loc=mu, scale=sigma)
sample b <- Bernoulli(probs=theta)

# mixed literal / variable: any combination works
sample h_cand <- Normal(loc=reset_hidden, scale=0.5)
sample z <- Normal(loc=0.0, scale=learned_scale)
sample r <- TruncatedNormal(mu=mu, sigma=sigma, low=0.0, high=1.0)

# negative literals
sample z <- Normal(loc=-1.5, scale=0.3)

A representative subset of the inline-distribution registry (the full set is documented in continuous families):

Family	Parameters	Codomain
`Normal`	`loc`, `scale`	`Real N`
`LogitNormal`	`mu`, `sigma`	`Real N [low=0, high=1]`
`Uniform`	`low`, `high`	`Real N [low=..., high=...]`
`Bernoulli`	`probs`	`FinSet 2`
`Beta`	`concentration1`, `concentration0`	`Real N [low=0, high=1]`
`Exponential`	`rate`	`Real N [low=0]`
`HalfCauchy`	`scale`	`Real N [low=0]`
`HalfNormal`	`scale`	`Real N [low=0]`
`LogNormal`	`loc`, `scale`	`Real N [low=0]`
`Gamma`	`concentration`, `rate`	`Real N [low=0]`
`Dirichlet`	`concentration`	`Simplex K`
`TruncatedNormal`	`mu`, `sigma`, `low`, `high`	`Real N [low=..., high=...]`
`MultivariateNormal`	`loc`, `scale_tril`	`Real N` (event_rank 1)
`MatrixNormal`	`loc`, `row_scale`, `col_scale`	`Real R C` (event_rank 2)
`LKJCholesky`	`concentration`	`CholeskyFactor K`
`Wishart`, `InverseWishart`	`df`, `scale_tril`	`Covariance K`
`Horseshoe`	`scale`	`Real N` (sparse-shrinkage prior)

Every parameter position in every family accepts either a literal value or a previously-bound variable. When all arguments are literals, a fixed distribution is created; when any argument is a variable, the family is resolved at runtime against the current trace's values.

For conditional distributions (input-conditional, learned-parameter form), use a morphism f : A -> B ~ Family declaration instead.

Examples¶

Simple discrete model¶

object X : FinSet 3
object Y : FinSet 4
morphism f : X -> Y [role=latent]
morphism g : Y -> Y [role=latent]

define fg = f >> g

export fg

Continuous conditional model¶

object Cond : FinSet 2
object Latent : Real 3
object Obs : Real 5

morphism prior : Cond -> Latent ~ Normal
morphism likelihood : Latent -> Obs ~ Normal
define posterior = prior >> likelihood

export posterior

Probabilistic program with observations¶

object Data : FinSet 1
object Y : Real 2

program regression : Data -> Y
    sample theta <- LogitNormal(mu=0.0, sigma=1.0)
    sample y <- Normal(loc=theta, scale=0.5)

    observe _ <- Normal(loc=y, scale=0.1)

    return y

Init recipe end-to-end¶

object D : FinSet 1
object In : Real 8
object Out : Real 4

# Default: weights initialised from a small-scale randn.
morphism W_default : In -> Out [role=latent, scale=0.1]

# Algebra-guided: init pulled from Algebra.init_spec, applied
# through the active algebra's bijector.  Under product_fuzzy
# (the default), the raw parameter is set to logit(ln(2) / depth);
# samples land near the algebra's neutral element on draw zero.
morphism W_auto : In -> Out [role=latent, init=auto]

export W_auto

For more examples, see the Examples Gallery. For a formal account of what .qvr programs mean, see the Denotational Semantics.