Terms

Stable value and computation terms.

terms

Stable value and computation terms for QIEC.

Terms contain no Python callables. Runtime values and handler bodies cross the boundary only through stable attachment and handler identifiers.

SCALE_FLOOR module-attribute

SCALE_FLOOR = 1e-07

The floor an exponentiated scale head of an :class:AffineMap or :class:TableMap is clamped at, which every backend applies alike.

LiteralData

LiteralData = None | bool | int | float | str | bytes | tuple[LiteralData, ...]

The host data a literal carries: a scalar, bytes, or a tuple of literal data.

ReductionOperator

ReductionOperator = Literal['sum', 'mean', 'max', 'min', 'logsumexp', 'prod']

The reductions of a whole tensor to one number.

RowwiseOperator

RowwiseOperator = Literal['softmax', 'log_softmax', 'cumsum', 'sort', 'normalize']

The operations along a tensor's last axis that keep its shape.

Value

Value = Var | LiteralValue | ConstructorValue | EvidenceValue | AttachmentRef | TransportValue | PrimitiveApplication | TupleValue | TensorValue | Projection | DistributionValue | LogDensity | SiteValue | Gather | WeightSum | SegmentSum | KernelMatrix | AffineMap | TableMap | Reduction | Rowwise | Comprehension

A value term: every pure, effect-free term a computation may mention.

Computation

Computation = Return | Bind | Perform | Handle | Case | If | Call | Resume | NewInstance

A computation term: every term that may perform effects or control flow.

Local dataclass

Local(name: str, type: TypeExpr)

A typed binder for a runtime value.

Locals are compared by identity of name and type together, so two binders of the same name at different types are distinct.

PARAMETER	DESCRIPTION
name	The binder's display name. TYPE: str
type	The type of every value bound to it. TYPE: TypeExpr

Var dataclass

Var(local: Local, tag: Literal['var'] = 'var')

Reference to a bound local.

PARAMETER	DESCRIPTION
local	The binder being referenced. TYPE: Local
tag	The serialization discriminator; always "var". TYPE: Literal['var'] DEFAULT: 'var'

LiteralValue dataclass

LiteralValue(value: LiteralData, type: TypeExpr, tag: Literal['literal'] = 'literal')

A literal host value at a primitive or tuple type.

PARAMETER	DESCRIPTION
value	The literal's data: None, a bool, int, float, str, bytes, or a tuple of literal data. TYPE: LiteralData
type	The literal's type. TYPE: TypeExpr
tag	The serialization discriminator; always "literal". TYPE: Literal['literal'] DEFAULT: 'literal'

ConstructorValue dataclass

ConstructorValue(constructor: ConstructorId, static_arguments: tuple[StaticArgument, ...], fields: tuple[Value, ...], result_type: TypeExpr, tag: Literal['constructor'] = 'constructor')

Application of a declared constructor to static and value arguments.

PARAMETER	DESCRIPTION
constructor	The stable identity of the constructor applied. TYPE: ConstructorId
static_arguments	The constructor's telescope instantiation, in binder order. TYPE: tuple[StaticArgument, ...]
fields	The field values, in declaration order. TYPE: tuple[Value, ...]
result_type	The indexed family type the application inhabits. TYPE: TypeExpr
tag	The serialization discriminator; always "constructor". TYPE: Literal['constructor'] DEFAULT: 'constructor'

EvidenceValue dataclass

EvidenceValue(evidence: EqualityEvidence, tag: Literal['evidence'] = 'evidence')

Kernel-checked equality evidence used as a value.

PARAMETER	DESCRIPTION
evidence	The evidence term. TYPE: EqualityEvidence
tag	The serialization discriminator; always "evidence". TYPE: Literal['evidence'] DEFAULT: 'evidence'

AttachmentRef dataclass

AttachmentRef(attachment: AttachmentId, type: TypeExpr, tag: Literal['attachment'] = 'attachment')

A stable reference to a runtime-owned host value.

PARAMETER	DESCRIPTION
attachment	The identity under which a runtime provider binds the host value. TYPE: AttachmentId
type	The type the bound value must inhabit. TYPE: TypeExpr
tag	The serialization discriminator; always "attachment". TYPE: Literal['attachment'] DEFAULT: 'attachment'

TransportValue dataclass

TransportValue(evidence: EqualityEvidence, value: Value, target_type: TypeExpr, tag: Literal['transport'] = 'transport')

Transport a value along kernel-checked equality evidence.

PARAMETER	DESCRIPTION
evidence	The equality the value is carried across. TYPE: EqualityEvidence
value	The value at the equality's left type. TYPE: Value
target_type	The type the transported value inhabits, which the equality's right side determines. TYPE: TypeExpr
tag	The serialization discriminator; always "transport". TYPE: Literal['transport'] DEFAULT: 'transport'

PrimitiveApplication dataclass

PrimitiveApplication(primitive: PrimitiveId, name: str, arguments: tuple[Value, ...], result_type: TypeExpr, origin: SourceOrigin, tag: Literal['primitive'] = 'primitive')

Application of a pure primitive from the closed registry.

The primitive is named nominally and its signature is fixed, so the checker validates the arguments against the registry and a backend renders the name it knows or refuses the capability; nothing is resolved by inspecting a runtime value.

PARAMETER	DESCRIPTION
primitive	The stable identity of the primitive applied. TYPE: PrimitiveId
name	The primitive's nominal name, as the registry spells it. TYPE: str
arguments	The value arguments, one per parameter. TYPE: tuple[Value, ...]
result_type	The primitive's result type. TYPE: TypeExpr
origin	The application's source location. TYPE: SourceOrigin
tag	The serialization discriminator; always "primitive". TYPE: Literal['primitive'] DEFAULT: 'primitive'

TupleValue dataclass

TupleValue(items: tuple[Value, ...], result_type: TypeExpr, tag: Literal['tuple'] = 'tuple')

Construction of a finite product from its components.

PARAMETER	DESCRIPTION
items	The component values, in order. TYPE: tuple[Value, ...]
result_type	The product type of the components. TYPE: TypeExpr
tag	The serialization discriminator; always "tuple". TYPE: Literal['tuple'] DEFAULT: 'tuple'

TensorValue dataclass

TensorValue(items: tuple[Value, ...], result_type: TypeExpr, tag: Literal['tensor'] = 'tensor')

Construction of a tensor from its entries along the outermost axis.

A rank-one tensor lists its elements; a tensor of higher rank lists the tensors one rank lower that are its slices, all of one shape, so a matrix literal is a tensor of row tensors.

PARAMETER	DESCRIPTION
items	The entries along the outermost axis, in order. TYPE: tuple[Value, ...]
result_type	The Tensor type constructed, whose leading dimension is the number of entries. TYPE: TypeExpr
tag	The serialization discriminator; always "tensor". TYPE: Literal['tensor'] DEFAULT: 'tensor'

Projection dataclass

Projection(value: Value, position: int, result_type: TypeExpr, tag: Literal['projection'] = 'projection')

Selection of one component of a finite product.

PARAMETER	DESCRIPTION
value	The product value projected from. TYPE: Value
position	The zero-based component selected. TYPE: int
result_type	The selected component's type. TYPE: TypeExpr
tag	The serialization discriminator; always "projection". TYPE: Literal['projection'] DEFAULT: 'projection'

PlateAxis dataclass

PlateAxis(name: str, size: IndexTerm, tag: Literal['plate_axis'] = 'plate_axis')

One axis of a plated distribution.

PARAMETER	DESCRIPTION
name	The axis's source name, the object it ranges over. TYPE: str
size	The axis's extent, an index term of the nat sort. TYPE: IndexTerm
tag	The serialization discriminator; always "plate_axis". TYPE: Literal['plate_axis'] DEFAULT: 'plate_axis'

PlateShape dataclass

PlateShape(batch: tuple[PlateAxis, ...] = (), event: tuple[PlateAxis, ...] = (), tag: Literal['plate_shape'] = 'plate_shape')

The plate a distribution is constructed over.

Batch axes replicate the distribution independently, one draw per position, each scored on its own; event axes join the draws along them into one event, scored together. The trailing event axes are the family's own event dimensions when it has any; any leading ones extend a scalar family's event.

PARAMETER	DESCRIPTION
batch	The independent replication axes, outermost first. TYPE: tuple[PlateAxis, ...] DEFAULT: ()
event	The joint axes, outermost first. TYPE: tuple[PlateAxis, ...] DEFAULT: ()
tag	The serialization discriminator; always "plate_shape". TYPE: Literal['plate_shape'] DEFAULT: 'plate_shape'

empty property

empty: bool

Whether the plate has no axes at all.

RETURNS	DESCRIPTION
bool	True when neither batch nor event axes are declared.

DistributionValue dataclass

DistributionValue(family: DistributionId, name: str, arguments: tuple[tuple[str, Value], ...], result_type: TypeExpr, origin: SourceOrigin, plate: PlateShape = PlateShape(), tag: Literal['distribution'] = 'distribution')

Construction of a distribution from a family of the semantic registry.

The family is named nominally and its parameters are supplied by name, so the term records which parameterization the source used and a backend renders the spelling it knows without inspecting values. A plate replicates the family over batch axes and joins draws along event axes; a parameter may then be a tensor whose leading dimensions follow a suffix of the plate's axes and broadcast over the rest.

PARAMETER	DESCRIPTION
family	The stable identity of the family applied. TYPE: DistributionId
name	The family's source name, as the registry spells it. TYPE: str
arguments	The parameters supplied, each named, in source order. TYPE: tuple[tuple[str, Value], ...]
result_type	The Sampleable type of the constructed distribution. TYPE: TypeExpr
origin	The construction's source location. TYPE: SourceOrigin
plate	The plate the distribution is constructed over; empty for one draw of the family. TYPE: PlateShape DEFAULT: PlateShape()
tag	The serialization discriminator; always "distribution". TYPE: Literal['distribution'] DEFAULT: 'distribution'

Gather dataclass

Gather(value: Value, index: Value, result_type: TypeExpr, tag: Literal['gather'] = 'gather')

Selection along the outermost axis of a tensor.

PARAMETER	DESCRIPTION
value	The tensor selected from. TYPE: Value
index	An Int selecting one slice, or a Tensor[Int] selecting a slice per entry. TYPE: Value
result_type	The selection's type: the slice type for an integer index, or a tensor of slices shaped like the index tensor. TYPE: TypeExpr
tag	The serialization discriminator; always "gather". TYPE: Literal['gather'] DEFAULT: 'gather'

WeightSum dataclass

WeightSum(value: Value, tag: Literal['weight_sum'] = 'weight_sum')

The total of a tensor of log weights.

PARAMETER	DESCRIPTION
value	A Tensor[LogWeight] of any shape, or a LogWeight. TYPE: Value
tag	The serialization discriminator; always "weight_sum". TYPE: Literal['weight_sum'] DEFAULT: 'weight_sum'

SegmentSum dataclass

SegmentSum(value: Value, index: Value, groups: IndexTerm, result_type: TypeExpr, tag: Literal['segment_sum'] = 'segment_sum')

Per-group totals of a vector of log weights.

PARAMETER	DESCRIPTION
value	A Tensor[LogWeight]([n]). TYPE: Value
index	A Tensor[Int]([n]) naming each entry's group. TYPE: Value
groups	The number of groups, an index term of the nat sort. TYPE: IndexTerm
result_type	Tensor[LogWeight]([groups]). TYPE: TypeExpr
tag	The serialization discriminator; always "segment_sum". TYPE: Literal['segment_sum'] DEFAULT: 'segment_sum'

KernelMatrix dataclass

KernelMatrix(inputs: Value, kernel: str, length_scale: float, jitter: float, result_type: TypeExpr, tag: Literal['kernel_matrix'] = 'kernel_matrix')

A positive-definite covariance over input locations.

PARAMETER	DESCRIPTION
inputs	A Tensor[Real]([n]) of locations. TYPE: Value
kernel	The kernel's name; "rbf" is the squared-exponential kernel. TYPE: str
length_scale	The kernel's length scale. TYPE: float
jitter	The diagonal added for numerical positive definiteness. TYPE: float
result_type	Tensor[Real]([n, n]). TYPE: TypeExpr
tag	The serialization discriminator; always "kernel_matrix". TYPE: Literal['kernel_matrix'] DEFAULT: 'kernel_matrix'

Reduction dataclass

Reduction(operator: ReductionOperator, value: Value, result_type: TypeExpr, tag: Literal['reduction'] = 'reduction')

A number summarizing every entry of a tensor.

PARAMETER	DESCRIPTION
operator	The reduction. TYPE: ReductionOperator
value	A tensor of reals, or of integers for sum, max, min, and prod. TYPE: Value
result_type	The element type. TYPE: TypeExpr
tag	The serialization discriminator; always "reduction". TYPE: Literal['reduction'] DEFAULT: 'reduction'

Rowwise dataclass

Rowwise(operator: RowwiseOperator, value: Value, result_type: TypeExpr, tag: Literal['rowwise'] = 'rowwise')

An operation along a tensor's last axis keeping its shape.

PARAMETER	DESCRIPTION
operator	The operation. TYPE: RowwiseOperator
value	A tensor of reals. TYPE: Value
result_type	The tensor's own type. TYPE: TypeExpr
tag	The serialization discriminator; always "rowwise". TYPE: Literal['rowwise'] DEFAULT: 'rowwise'

Comprehension dataclass

Comprehension(binder: Local, extent: IndexTerm, body: Value, result_type: TypeExpr, tag: Literal['comprehension'] = 'comprehension')

A tensor built by evaluating a body at every index of an axis.

PARAMETER	DESCRIPTION
binder	The Int local the body reads the index through. TYPE: Local
extent	The axis's extent, an index term of the nat sort. TYPE: IndexTerm
body	The entry at each index. TYPE: Value
result_type	Tensor[T]([extent]) for the body's type T, or, when the body is itself a tensor, the tensor with extent prepended. TYPE: TypeExpr
tag	The serialization discriminator; always "comprehension". TYPE: Literal['comprehension'] DEFAULT: 'comprehension'

AffineMap dataclass

AffineMap(weight: Value, bias: Value, sources: tuple[Value, ...], row_offset: int, rows: int, transform: Literal['identity', 'exp', 'exp_floor'], result_type: TypeExpr, tag: Literal['affine_map'] = 'affine_map')

One head of an affine parameter map, W x + b on a row block.

For i below rows the head's coordinate i is the sum over j of weight[row_offset + i, j] * x[j] plus bias[row_offset + i], where x concatenates the sources in order; exp exponentiates every coordinate afterwards, and exp_floor exponentiates and clamps each at the scale floor.

PARAMETER	DESCRIPTION
weight	A Tensor[Real]([total_rows, columns]). TYPE: Value
bias	A Tensor[Real]([total_rows]). TYPE: Value
sources	The conditioning row's factors in order, each a Real or a Tensor[Real]([width]). TYPE: tuple[Value, ...]
row_offset	The first row of the head's block. TYPE: int
rows	The block's height. TYPE: int
transform	"identity", "exp", or "exp_floor". TYPE: Literal['identity', 'exp', 'exp_floor']
result_type	Tensor[Real]([rows]), or Real for a one-row head. TYPE: TypeExpr
tag	The serialization discriminator; always "affine_map". TYPE: Literal['affine_map'] DEFAULT: 'affine_map'

TableMap dataclass

TableMap(table: Value, index: Value, row_offset: int, rows: int, transform: Literal['identity', 'exp', 'exp_floor'], result_type: TypeExpr, tag: Literal['table_map'] = 'table_map')

One head of a table-indexed parameter map, a row block of T[i].

A kernel over a finite domain reads its parameters from a table with one row per element of the domain: for i below rows the head's coordinate i is table[index, row_offset + i], with exp exponentiating every coordinate afterwards and exp_floor exponentiating and clamping each at the scale floor.

PARAMETER	DESCRIPTION
table	A Tensor[Real]([entries, total_rows]). TYPE: Value
index	An Int naming the row, the element of the domain. TYPE: Value
row_offset	The first column of the head's block. TYPE: int
rows	The block's width. TYPE: int
transform	"identity", "exp", or "exp_floor". TYPE: Literal['identity', 'exp', 'exp_floor']
result_type	Tensor[Real]([rows]), or Real for a one-column head. TYPE: TypeExpr
tag	The serialization discriminator; always "table_map". TYPE: Literal['table_map'] DEFAULT: 'table_map'

SiteValue dataclass

SiteValue(label: str, result_type: TypeExpr, tag: Literal['site'] = 'site')

A named sample site.

A site is the address a probabilistic step is observed and traced under. Its label is the source name of the step, which is stable data; the dynamic address a run adds comes from the request that carries it.

PARAMETER	DESCRIPTION
label	The site's source name. TYPE: str
result_type	The Site type of the value the site produces. TYPE: TypeExpr
tag	The serialization discriminator; always "site". TYPE: Literal['site'] DEFAULT: 'site'

LogDensity dataclass

LogDensity(sampleable: Value, value: Value, origin: SourceOrigin, batch: tuple[PlateAxis, ...] = (), tag: Literal['log_density'] = 'log_density')

Evaluation of a distribution's log density at a value.

PARAMETER	DESCRIPTION
sampleable	The distribution, of type Sampleable[A]. TYPE: Value
value	The point evaluated, of type A. TYPE: Value
origin	The evaluation's source location. TYPE: SourceOrigin
batch	The batch axes the density is kept apart over: empty for one LogWeight totalling every draw, else the batch axes of the plated construction sampleable must be, for one weight per position. TYPE: tuple[PlateAxis, ...] DEFAULT: ()
tag	The serialization discriminator; always "log_density". TYPE: Literal['log_density'] DEFAULT: 'log_density'

Return dataclass

Return(value: Value, tag: Literal['return'] = 'return')

Return a value with no effects.

PARAMETER	DESCRIPTION
value	The value produced. TYPE: Value
tag	The serialization discriminator; always "return". TYPE: Literal['return'] DEFAULT: 'return'

Bind dataclass

Bind(binder: Local, first: Computation, then: Computation, tag: Literal['bind'] = 'bind')

Sequence two computations, binding the first's result in the second.

PARAMETER	DESCRIPTION
binder	The local the first computation's result is bound to. TYPE: Local
first	The computation run first. TYPE: Computation
then	The computation run second, with binder in scope. TYPE: Computation
tag	The serialization discriminator; always "bind". TYPE: Literal['bind'] DEFAULT: 'bind'

Perform dataclass

Perform(request: EffectRequest, tag: Literal['perform'] = 'perform')

Perform one effect operation.

PARAMETER	DESCRIPTION
request	The operation, its instance, static arguments, value arguments, and result type. TYPE: EffectRequest
tag	The serialization discriminator; always "perform". TYPE: Literal['perform'] DEFAULT: 'perform'

Handle dataclass

Handle(instance: EffectInstanceId, handler: HandlerId, computation: Computation, static_arguments: tuple[StaticArgument, ...] = (), tag: Literal['handle'] = 'handle')

Run a computation under a handler installed for one effect instance.

PARAMETER	DESCRIPTION
instance	The effect instance whose operations the handler intercepts. TYPE: EffectInstanceId
handler	The stable identity of the handler installed. TYPE: HandlerId
computation	The handled computation. TYPE: Computation
static_arguments	The handler's telescope instantiation, in binder order. TYPE: tuple[StaticArgument, ...] DEFAULT: ()
tag	The serialization discriminator; always "handle". TYPE: Literal['handle'] DEFAULT: 'handle'

CaseMotive dataclass

CaseMotive(indices: Telescope, result_type: TypeExpr)

The result family of an indexed case expression.

PARAMETER	DESCRIPTION
indices	The binders abstracting the scrutinee's indices in result_type. TYPE: Telescope
result_type	The type every branch must produce, over indices. TYPE: TypeExpr

CaseBranch dataclass

CaseBranch(constructor: ConstructorId, static_arguments: tuple[StaticArgument, ...], fields: tuple[Local, ...], body: Computation, scope: StaticScopeId)

One stable GADT branch with no host-language closure.

PARAMETER	DESCRIPTION
constructor	The constructor this branch matches. TYPE: ConstructorId
static_arguments	The constructor's static arguments as bound by the pattern, in binder order. TYPE: tuple[StaticArgument, ...]
fields	The locals binding the constructor's fields, in declaration order. TYPE: tuple[Local, ...]
body	The computation run when the branch is selected. TYPE: Computation
scope	The static scope identity under which the branch's skolems and equality evidence are minted. TYPE: StaticScopeId

Case dataclass

Case(scrutinee: Value, motive: CaseMotive, branches: tuple[CaseBranch, ...], tag: Literal['case'] = 'case')

Case analysis over an indexed family value.

PARAMETER	DESCRIPTION
scrutinee	The value analyzed. TYPE: Value
motive	The result family, over the scrutinee's indices. TYPE: CaseMotive
branches	One branch per constructor considered; coverage is checked against the exact applied family. TYPE: tuple[CaseBranch, ...]
tag	The serialization discriminator; always "case". TYPE: Literal['case'] DEFAULT: 'case'

Call dataclass

Call(callee: ComputationId, name: str, static_arguments: tuple[StaticArgument, ...], arguments: tuple[Value, ...], result_type: TypeExpr, effects: EffectRow, origin: SourceOrigin, tag: Literal['call'] = 'call')

Application of a named computation.

The callee is a stable identifier rather than an inlined body, which is what lets a recursive or mutually recursive call graph serialize as a finite tree.

PARAMETER	DESCRIPTION
callee	The stable identity of the computation called. TYPE: ComputationId
name	The callee's display name, for diagnostics and traces. TYPE: str
static_arguments	The callee's telescope instantiation, in binder order. TYPE: tuple[StaticArgument, ...]
arguments	The value arguments, one per callee parameter. TYPE: tuple[Value, ...]
result_type	The callee's result type under the instantiation. TYPE: TypeExpr
effects	The callee's effect row under the instantiation. TYPE: EffectRow
origin	The call site's source location. TYPE: SourceOrigin
tag	The serialization discriminator; always "call". TYPE: Literal['call'] DEFAULT: 'call'

Resume dataclass

Resume(value: Value, origin: SourceOrigin, tag: Literal['resume'] = 'resume')

Invocation of the enclosing handler clause's continuation.

The resumption is not a value and cannot be stored, so it is a term of its own rather than a call to a bound name. That is what makes a clause's grade checkable by counting invocations along the paths through its body.

PARAMETER	DESCRIPTION
value	The value returned to the suspended computation as the operation's result. TYPE: Value
origin	The resumption's source location. TYPE: SourceOrigin
tag	The serialization discriminator; always "resume". TYPE: Literal['resume'] DEFAULT: 'resume'

NewInstance dataclass

NewInstance(instance: EffectInstanceId, effect: EffectRef, body: Computation, origin: SourceOrigin, tag: Literal['new_instance'] = 'new_instance')

Lexically scoped allocation of an effect instance.

The identity is derived from the module, the enclosing computation, the lexical path, and the applied interface, so the same allocation site yields the same instance on every run while two sites of the same interface stay distinct.

PARAMETER	DESCRIPTION
instance	The scope-derived stable identity of the allocated instance. TYPE: EffectInstanceId
effect	The applied interface the instance provides. TYPE: EffectRef
body	The computation within which the instance is in scope. TYPE: Computation
origin	The allocation's source location. TYPE: SourceOrigin
tag	The serialization discriminator; always "new_instance". TYPE: Literal['new_instance'] DEFAULT: 'new_instance'

If dataclass

If(condition: Value, then: Computation, otherwise: Computation, tag: Literal['if'] = 'if')

Branch on a Boolean value.

Both branches must produce the same type; the row of the whole is the union of the branches' rows. This is what lets a recursive computation stop, since a value-level select would evaluate both branches and never terminate.

PARAMETER	DESCRIPTION
condition	The Boolean value branched on. TYPE: Value
then	The computation run when the condition holds. TYPE: Computation
otherwise	The computation run when it does not. TYPE: Computation
tag	The serialization discriminator; always "if". TYPE: Literal['if'] DEFAULT: 'if'