Quivers Indexed Effect Core¶
The stable kernel every QVR module checks against and every transpiler reads. The package re-exports the modules below.
qiec
¶
Quivers Indexed Effect Core (QIEC) reference kernel.
QIEC is a small typed value/computation IR for indexed families and algebraic effects. It is deliberately independent of the QVR surface grammar and the target probabilistic IR: the compiler may lower into QIEC incrementally, while Didactic and Panproto check its first-order indexed-family projection.
ABORT
module-attribute
¶
Abort[P]: the prelude interface for stopping with a payload of type P.
ABORT_ABORT
module-attribute
¶
ABORT_ABORT = _operation_id(ABORT, 'abort')
Abort.abort: stop the computation with an error payload.
ABORT_EFFECT
module-attribute
¶
ABORT_EFFECT = EffectDef(ABORT, (_P_BINDER,), (OperationDef(ABORT_ABORT, 'abort', (_A_BINDER,), (ArgumentDef('error', PAYLOAD),), A),))
The declaration of :data:ABORT; :func:abort_effect applies it.
BUILTIN_EFFECTS
module-attribute
¶
BUILTIN_EFFECTS = (RANDOM_EFFECT, SCORE_EFFECT, STATE_EFFECT, ABORT_EFFECT, CHOOSE_EFFECT, WEIGHT_EFFECT, COMPUTE_EFFECT, PARAM_EFFECT)
Every prelude interface declaration, which every module may name without declaring.
CHOOSE
module-attribute
¶
Choose: the prelude interface for nondeterministic choice.
CHOOSE_CHOOSE
module-attribute
¶
CHOOSE_CHOOSE = _operation_id(CHOOSE, 'choose')
Choose.choose: pick one of a collection of alternatives.
CHOOSE_EFFECT
module-attribute
¶
CHOOSE_EFFECT = EffectDef(CHOOSE, (), (OperationDef(CHOOSE_CHOOSE, 'choose', (_A_BINDER,), (ArgumentDef('alternatives', CHOICES_A),), A),))
The declaration of :data:CHOOSE.
COMPUTE
module-attribute
¶
Compute[X, A]: the prelude interface for a host computation; see :data:COMPUTE_EFFECT.
COMPUTE_APPLY
module-attribute
¶
COMPUTE_APPLY = _operation_id(COMPUTE, 'apply')
Compute.apply: run the host computation on an argument of type X.
COMPUTE_EFFECT
module-attribute
¶
COMPUTE_EFFECT = EffectDef(COMPUTE, (_X_BINDER, _ANSWER_BINDER), (OperationDef(COMPUTE_APPLY, 'apply', (), (ArgumentDef('argument', INPUT),), ANSWER),))
Compute[X, A]: a host computation as an effect interface.
A morphism, a closure, or any other process-local function a program
depends on is not a kernel value; performing apply on an instance of
this interface asks the handler installed for it, which a runtime
provider supplies, so the dependence is explicit in the row.
PARAM
module-attribute
¶
Param: the prelude interface for learned parameter lookup; see :data:PARAM_EFFECT.
PARAM_EFFECT
module-attribute
¶
PARAM_EFFECT = EffectDef(PARAM, (), (OperationDef(PARAM_GET, 'get', (_A_BINDER,), (ArgumentDef('name', STRING),), A),))
Param: learned parameter lookup as an effect.
A host computation reads each learned tensor it depends on by name
through get, so a handler between it and the parameter store can
answer with a perturbed value, as a prior lift does, or record the read.
PARAM_GET
module-attribute
¶
PARAM_GET = _operation_id(PARAM, 'get')
Param.get: read a learned parameter by name.
RANDOM
module-attribute
¶
Random: the prelude interface for drawing a value at a sample site.
RANDOM_EFFECT
module-attribute
¶
RANDOM_EFFECT = EffectDef(RANDOM, (), (OperationDef(RANDOM_SAMPLE, 'sample', (_A_BINDER,), (ArgumentDef('site', SITE_A), ArgumentDef('sampleable', SAMPLEABLE_A)), A),))
The declaration of :data:RANDOM.
RANDOM_SAMPLE
module-attribute
¶
RANDOM_SAMPLE = _operation_id(RANDOM, 'sample')
Random.sample: draw a value of type A at a site from a Sampleable[A].
SCORE
module-attribute
¶
Score: the prelude interface for adding a log-density contribution.
SCORE_ADD
module-attribute
¶
SCORE_ADD = _operation_id(SCORE, 'add')
Score.add: add one LogWeight to the running score.
SCORE_EFFECT
module-attribute
¶
SCORE_EFFECT = EffectDef(SCORE, (), (OperationDef(SCORE_ADD, 'add', (), (ArgumentDef('weight', LOG_WEIGHT),), UNIT),))
The declaration of :data:SCORE.
SEARCH_REDUCTIONS
module-attribute
¶
The semiring additions :func:search_handler may combine its shots by.
STATE_EFFECT
module-attribute
¶
STATE_EFFECT = EffectDef(STATE_EFFECT_REF, (_S_BINDER,), (OperationDef(STATE_GET, 'get', (), (), STATE), OperationDef(STATE_PUT, 'put', (), (ArgumentDef('value', STATE),), UNIT)))
The declaration of :data:STATE_EFFECT_REF; :func:state_effect applies it.
STATE_EFFECT_REF
module-attribute
¶
State[S]: the prelude interface for one mutable cell of type S.
STATE_GET
module-attribute
¶
STATE_GET = _operation_id(STATE_EFFECT_REF, 'get')
State.get: read the cell.
STATE_PUT
module-attribute
¶
STATE_PUT = _operation_id(STATE_EFFECT_REF, 'put')
State.put: overwrite the cell.
WEIGHT
module-attribute
¶
Weight[K]: the prelude interface for accumulating a semiring weight of type K.
WEIGHT_ADD
module-attribute
¶
WEIGHT_ADD = _operation_id(WEIGHT, 'add')
Weight.add: fold one weight into the running total in the handler's semiring.
WEIGHT_EFFECT
module-attribute
¶
WEIGHT_EFFECT = EffectDef(WEIGHT, (_K_BINDER,), (OperationDef(WEIGHT_ADD, 'add', (), (ArgumentDef('weight', K),), UNIT),))
The declaration of :data:WEIGHT; :func:weight_effect applies it.
BUILTIN_TYPE_CONSTRUCTORS
module-attribute
¶
BUILTIN_TYPE_CONSTRUCTORS: dict[str, TypeConstructorRef] = {'Site': SITE_CONSTRUCTOR, 'Sampleable': SAMPLEABLE_CONSTRUCTOR, 'Tensor': TENSOR_CONSTRUCTOR, 'LogWeight': LOG_WEIGHT.constructor}
The canonical names a source type may refer to without declaring them.
ELEMENT
module-attribute
¶
ELEMENT = TypeVariable('a')
The type variable :data:ELEMENT_BINDER binds.
ELEMENT_BINDER
module-attribute
¶
ELEMENT_BINDER = TypeBinder('a')
The element-type binder a of the canonical constructors' telescopes.
LOG_WEIGHT
module-attribute
¶
LOG_WEIGHT = TypeApplication(builtin_constructor('LogWeight'))
LogWeight: a log-density contribution.
SAMPLEABLE_CONSTRUCTOR
module-attribute
¶
SAMPLEABLE_CONSTRUCTOR = builtin_constructor('Sampleable', ELEMENT_BINDER)
Sampleable[A]: a distribution over values of type A.
SHAPE_BINDER
module-attribute
¶
SHAPE_BINDER = IndexBinder('shape', ShapeSort())
The shape-index binder of :data:TENSOR_CONSTRUCTOR's telescope.
SITE_CONSTRUCTOR
module-attribute
¶
SITE_CONSTRUCTOR = builtin_constructor('Site', ELEMENT_BINDER)
Site[A]: a named sample site whose value has type A.
TENSOR_CONSTRUCTOR
module-attribute
¶
TENSOR_CONSTRUCTOR = builtin_constructor('Tensor', ELEMENT_BINDER, SHAPE_BINDER)
Tensor[A](shape): an array of A with a static shape index.
EMPTY_ROW
module-attribute
¶
EMPTY_ROW = EffectRow()
The row of a computation that performs no effects.
FAMILIES
module-attribute
¶
FAMILIES: Mapping[str, DistributionFamily] = MappingProxyType({item.name: item for item in _FAMILIES})
Every family by source name.
The mapping is closed: a name absent here is not a distribution family, and no backend may invent one.
QIEC_ABI
module-attribute
¶
The kernel ABI tag a module records, so a reader can reject a module built against another kernel.
IMPLEMENTATIONS
module-attribute
¶
IMPLEMENTATIONS: Mapping[str, Callable[..., object]] = MappingProxyType({signature.name: implementation for signature, implementation in _ENTRIES})
The reference evaluator's implementation of every primitive, by name.
PRIMITIVES
module-attribute
¶
PRIMITIVES: Mapping[str, PrimitiveSignature] = MappingProxyType({signature.name: signature for signature, _ in _ENTRIES})
Every primitive by name.
The mapping is closed: a name absent here is not a primitive, and no backend may resolve one dynamically.
QIEC_WIRE_FORMAT
module-attribute
¶
The format tag every encoded document carries, checked on decoding.
SCALE_FLOOR
module-attribute
¶
The floor an exponentiated scale head of an :class:AffineMap or
:class:TableMap is clamped at, which every backend applies alike.
BOOL
module-attribute
¶
BOOL = TypeApplication(TypeConstructorRef.builtin('Bool'))
The Boolean type.
REAL
module-attribute
¶
REAL = TypeApplication(TypeConstructorRef.builtin('Real'))
The real-number type.
STRING
module-attribute
¶
STRING = TypeApplication(TypeConstructorRef.builtin('String'))
The string type.
UNIT
module-attribute
¶
UNIT = TypeApplication(TypeConstructorRef.builtin('Unit'))
The unit type, inhabited by None alone.
EntryKind
¶
How an entry point is declared: with define or with program.
HostValue
¶
HostValue = bool | int | float | str | Tensor | tuple['HostValue', ...] | Mapping[str, 'HostValue']
A value the reference machine takes or returns: a scalar, a tensor, a tuple, or a record of such values.
EvaluationTraceHook
¶
A callback receiving each evaluator event's name and detail mapping.
OperationClause
¶
A host implementation of one handler operation clause.
It receives the request, the delimited continuation, and the clause's
runtime services, and returns the clause's answer, a :class:Forward, or a
:class:TailResume.
ResponseHook
¶
A callback applied to the reply a forwarded request receives.
It returns the value the resumed computation receives in place of the reply.
ReturnClause
¶
A host implementation of a handler's return clause.
It receives the handled computation's final value and the clause's runtime services, and returns the handler's answer.
RuntimeValidator
¶
A predicate a host value must pass to inhabit a QIEC type.
It returns False to reject the value; True or None accepts it.
EqualityEvidence
¶
EqualityEvidence = Reflexivity | BranchGiven
Kernel-generated evidence of a static equality: reflexivity or a branch's given.
RuntimeProviderFactory
¶
RuntimeProviderFactory = Callable[[Mapping[str, object]], RuntimeProvider]
Build a runtime provider from the options its configuration entry records.
TraceObserver
¶
A callback receiving each event an execution emits, in order.
ParameterConstraint
¶
A symbolic constraint on a parameter value, such as "positive",
"unit_interval", "simplex", "positive_definite", or
"dependent" when the admissible values depend on other parameters. A
compositional family's parameters use "sampleable" for a distribution
it is built from and "transform" for a named bijector chain; an atom's
"numeric" value is an integer or a real, and fixes which the atom
samples.
SupportKind
¶
A symbolic description of where samples live, in the same vocabulary as the parameter constraints.
AddressRelation
¶
How an effect request relates to its source site.
"preserve" marks the request as written; "split" and
"duplicate" mark a request a handler derived from it; "eliminate"
marks one a handler discharged.
IndexSort
¶
IndexSort = NatSort | ShapeSort | ContextSort | UserIndexSort
The sort of an index binder: naturals, shapes, contexts, or a declared sort.
Kind
¶
Kind = TypeKind | EffectKind | RowKind | ArrowKind
The kind of a static binder: a type, an effect, a row, or an arrow between kinds.
Telescope
¶
Telescope = tuple[TelescopeBinder, ...]
The static binders a declaration takes, in order; later binders may mention earlier ones.
TelescopeBinder
¶
TelescopeBinder = TypeBinder | IndexBinder | EffectBinder
One binder of a declaration telescope: a type, an index, or an effect binder.
PrimitiveCapability
¶
PrimitiveCapability = Literal['arithmetic', 'comparison', 'boolean', 'string', 'conversion', 'math', 'special', 'activation', 'weight']
The feature a target must support to render a primitive.
ParameterRole
¶
ParameterRole = Literal['domain', 'scalar', 'data', 'observation', 'fibration', 'weight', 'bias', 'table', 'kernel-input']
How a program parameter is supplied.
domain parameters carry the value the program is applied to, one per
real factor of its domain; scalar ones are its declared parameters;
data ones are free names its steps read; observation ones are the
values observe steps score; fibration ones map observation rows to
groups; weight and bias are the numbers of a declared morphism's
affine parameter map and table those of a morphism over a finite
domain, one row per element; kernel-input holds a kernel's input
locations.
SiteKind
¶
What a program step does at its site.
JsonValue
¶
A JSON document as json.loads returns it and json.dumps accepts it.
Computation
¶
A computation term: every term that may perform effects or control flow.
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
¶
The reductions of a whole tensor to one number.
RowwiseOperator
¶
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.
IndexTerm
¶
IndexTerm = IndexVariable | IndexLiteral | IndexConstructor | ShapeIndex
A static index: a variable, a literal, a constructor application, or a shape.
StaticArgument
¶
StaticArgument = TypeExpr | IndexTerm | EffectRef | EffectVariable
Anything a telescope binder may be instantiated at: a type, an index, or an effect.
TypeExpr
¶
TypeExpr = TypeVariable | TypeApplication | FunctionType | EqualityType
A type: a variable, a constructor application, a function type, or an equality.
Aborted
dataclass
¶
The default answer of an abort handler, wrapping the abort payload.
| PARAMETER | DESCRIPTION |
|---|---|
error
|
The payload the computation aborted with.
TYPE:
|
ExtraValuePolicy
¶
Bases: str, Enum
What a handler does with a supplied value no sample site consumed.
IGNORE discards it; ERROR rejects the run when the handled
computation returns.
MissingValuePolicy
¶
Bases: str, Enum
What a condition handler does with a sample site it has no observation for.
FORWARD passes the request to an outer handler; ERROR rejects it.
ReplayPolicy
¶
Bases: str, Enum
Whether a replayed value is scored as well as clamped.
CLAMP_AND_SCORE sends the replayed value's log density to a Score
instance; CLAMP_NO_SCORE and INTERVENE replay it without scoring.
ScoreAccumulator
dataclass
¶
Mutable result owned by one installed Score handler.
| PARAMETER | DESCRIPTION |
|---|---|
total
|
The running combination of every contribution so far, starting at the handler's identity.
TYPE:
|
contributions
|
Every contribution in the order it was added.
TYPE:
|
StateCell
dataclass
¶
The mutable cell owned by one installed State handler.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The current state.
TYPE:
|
TraceEvent
dataclass
¶
TraceEvent(address: tuple[str, tuple[tuple[str, str | int], ...], tuple[int, ...]], instance: EffectInstanceId, operation: OperationId, arguments: tuple[object, ...], result: object, mode: str)
One recorded request and the value produced for it.
| PARAMETER | DESCRIPTION |
|---|---|
address
|
The request's dynamic key: its static site, address frames, and resumption path.
TYPE:
|
instance
|
The effect instance the request was performed on.
TYPE:
|
operation
|
The operation requested.
TYPE:
|
arguments
|
The evaluated value arguments.
TYPE:
|
result
|
The value produced for the request.
TYPE:
|
mode
|
How the value was produced, such as
TYPE:
|
TraceRecorder
dataclass
¶
TraceRecorder(events: list[TraceEvent] = list())
Ordered trace; repeated dynamic addresses remain observable as events.
| PARAMETER | DESCRIPTION |
|---|---|
events
|
The recorded events, in order; empty to start.
TYPE:
|
record
¶
record(request: RuntimeRequest, result: object, *, mode: str) -> object
Record one request and the value produced for it.
| PARAMETER | DESCRIPTION |
|---|---|
request
|
The request being answered and its arguments.
TYPE:
|
result
|
The value produced for the request.
TYPE:
|
mode
|
How the value was produced.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
The value, unchanged, after recording. Returned so the caller can use this in place of the value it passed. |
Source code in src/quivers/qiec/builtins.py
WeightAccumulator
dataclass
¶
Mutable result owned by one installed Weight handler.
| PARAMETER | DESCRIPTION |
|---|---|
total
|
The running combination of every contribution so far, starting at the handler's identity.
TYPE:
|
contributions
|
Every contribution in the order it was added.
TYPE:
|
CheckContext
dataclass
¶
CheckContext(locals: tuple[Local, ...] = (), givens: tuple[BranchGiven, ...] = (), static_scopes: tuple[StaticScopeId, ...] = (), static_variables: tuple[StaticVariableId, ...] = (), resumption: ResumptionType | None = None)
What is in scope at one point in a term being checked.
| PARAMETER | DESCRIPTION |
|---|---|
locals
|
Value bindings, innermost last.
TYPE:
|
givens
|
Equality evidence introduced by enclosing case branches, which is what makes an index refinement usable in the branch body.
TYPE:
|
static_scopes
|
Static scopes already entered. Tracked so a branch cannot reuse an enclosing scope's identity and silently capture its variables.
TYPE:
|
static_variables
|
Rigid variables currently active, tracked for the same reason.
TYPE:
|
resumption
class-attribute
instance-attribute
¶
resumption: ResumptionType | None = None
The continuation, when checking a handler clause body.
None everywhere else, which is what makes resume outside a
clause a checker error rather than a term with no meaning.
extend
¶
extend(local: Local) -> CheckContext
Return this context with one more value binding.
| PARAMETER | DESCRIPTION |
|---|---|
local
|
The binding to add.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
CheckContext
|
A context carrying the new binding innermost. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the name is already bound. Rebinding is rejected rather than shadowed, so a name denotes one value throughout a body. |
Source code in src/quivers/qiec/checking.py
with_givens
¶
with_givens(givens: tuple[BranchGiven, ...]) -> CheckContext
Return this context with further equality evidence in scope.
| PARAMETER | DESCRIPTION |
|---|---|
givens
|
Evidence a case branch introduces by matching a constructor.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
CheckContext
|
A context in which that evidence may be appealed to. |
Source code in src/quivers/qiec/checking.py
with_static_scope
¶
with_static_scope(scope: StaticScopeId, variables: tuple[StaticVariableId, ...] = ()) -> CheckContext
Return this context inside a fresh static scope.
| PARAMETER | DESCRIPTION |
|---|---|
scope
|
Identity of the scope being entered.
TYPE:
|
variables
|
Rigid variables the scope introduces.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
CheckContext
|
A context recording the scope and its variables as active. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the scope or one of its variables is already active. Reuse would let a branch's rigid variable be confused with an enclosing one, which is what keeps branch refinements from leaking out of the branch. |
Source code in src/quivers/qiec/checking.py
with_resumption
¶
with_resumption(resumption: ResumptionType) -> CheckContext
Return this context inside a handler clause body.
| PARAMETER | DESCRIPTION |
|---|---|
resumption
|
The continuation the clause body may invoke.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
CheckContext
|
A context in which |
Source code in src/quivers/qiec/checking.py
local_type
¶
local_type(name: str) -> TypeExpr | None
The type of a value binding in scope.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The bound name to resolve.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeExpr or None
|
The binding's type, or None when the name is not bound here.
The innermost binding wins, though |
Source code in src/quivers/qiec/checking.py
given
¶
given(equality: EqualityId) -> BranchGiven | None
The equality evidence with a given identity, if in scope.
| PARAMETER | DESCRIPTION |
|---|---|
equality
|
The identity to resolve.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
BranchGiven or None
|
The evidence, or None when it is not in scope, which is how an appeal to a refinement outside its branch is caught. |
Source code in src/quivers/qiec/checking.py
ComputationSignature
dataclass
¶
ComputationSignature(id: ComputationId, name: str, telescope: Telescope, parameters: tuple[TypeExpr, ...], result: TypeExpr, effects: EffectRow)
What a call needs to know about a computation it invokes.
A signature rather than a declaration, and deliberately so: a call resolves against this, not against the callee's body. That is what lets every signature be collected before any body is checked, which in turn makes a forward call and mutual recursion ordinary rather than requiring a forward declaration.
| PARAMETER | DESCRIPTION |
|---|---|
id
|
The declaration's stable identity, which the call carries.
TYPE:
|
name
|
The authored name, used in diagnostics.
TYPE:
|
telescope
|
Static binders the computation takes.
TYPE:
|
parameters
|
Value parameter types, in order, before instantiation.
TYPE:
|
result
|
The result type before instantiation.
TYPE:
|
effects
|
The row the computation performs, before instantiation.
TYPE:
|
KernelError
¶
Bases: TypeError
A static QIEC kernel rejection.
Carries a stable diagnostic code alongside its message. The code is attached where the rejection is raised, because only that site knows which condition fired; classifying by message text afterwards is a guess that silently changes whenever the prose is reworded.
| PARAMETER | DESCRIPTION |
|---|---|
message
|
What was rejected, in prose, for a human reader.
TYPE:
|
code
|
A member of the published code set. Defaults to
TYPE:
|
Source code in src/quivers/qiec/checking.py
KernelRegistry
dataclass
¶
KernelRegistry(families: dict[FamilyId, FamilyDecl] = dict(), constructors: dict[ConstructorId, ConstructorDecl] = dict(), effects: dict[EffectId, EffectDef] = dict(), operations: dict[OperationId, tuple[EffectDef, OperationDef]] = dict(), handlers: dict[HandlerId, HandlerDef] = dict(), type_constructors: dict[TypeId, TypeConstructorRef] = dict(), computations: dict[ComputationId, ComputationSignature] = dict(), instance_names: dict[EffectInstanceId, str] = dict())
Resolved declarations used by the reference checker.
Every table is keyed by stable identity, so a lookup never depends on a display name.
| PARAMETER | DESCRIPTION |
|---|---|
families
|
Indexed data families by identity.
TYPE:
|
constructors
|
Family constructors by identity.
TYPE:
|
effects
|
Effect interfaces by identity. |
operations
|
Each operation by identity, paired with the interface declaring it.
TYPE:
|
handlers
|
Handler declarations by identity.
TYPE:
|
type_constructors
|
Type constructors by identity, recording the telescope each is known with.
TYPE:
|
computations
|
Named computation signatures by identity.
TYPE:
|
instance_names
|
The source name of each lexical effect instance, for rendering rows in diagnostics.
TYPE:
|
validate_static
¶
validate_static(term: StaticArgument, scope: StaticScope | None = None) -> None
Validate a static term against every declaration known here.
| PARAMETER | DESCRIPTION |
|---|---|
term
|
The static term to check.
TYPE:
|
scope
|
Binders in scope at the term's position. None means the empty scope, so any variable reference is out of scope.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the term is ill-kinded, references an unbound static variable, or applies a known declaration wrongly. |
Source code in src/quivers/qiec/checking.py
validate_type
¶
validate_type(type_: TypeExpr, scope: StaticScope | None = None) -> None
Validate a value type against every declaration known here.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
The value type to check.
TYPE:
|
scope
|
Binders in scope at the type's position. None means the empty scope.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the type is ill-kinded or references an unbound variable. |
Source code in src/quivers/qiec/checking.py
validate_effect_row
¶
validate_effect_row(row: EffectRow) -> None
Validate all concrete interface applications in an effect row.
| PARAMETER | DESCRIPTION |
|---|---|
row
|
The row whose entries to check. An open tail carries no application and so is not checked here.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If an entry applies its interface wrongly. |
Source code in src/quivers/qiec/checking.py
validate_computation_type
¶
validate_computation_type(type_: ComputationType) -> None
Validate both strata of a computation type.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
The computation type whose effect row and result type to check.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If either stratum is ill-formed. |
Source code in src/quivers/qiec/checking.py
register_family
¶
register_family(family: FamilyDecl) -> None
Record an indexed family declaration.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family to register, with its uniform parameters and its refinable indices.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If a family with this identity is already registered, if two of its binders share a name, or if its type constructor disagrees with one already recorded. |
Source code in src/quivers/qiec/checking.py
register_constructor
¶
register_constructor(constructor: ConstructorDecl) -> None
Record a constructor against the family that declares it.
| PARAMETER | DESCRIPTION |
|---|---|
constructor
|
The constructor to register. Its family must already be registered and must list this constructor.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the constructor is already registered, if its family is unknown or does not declare it, if it returns the wrong number of result indices, if its telescope shadows a family binder, or if a field type or result index is ill-formed. |
Source code in src/quivers/qiec/checking.py
register_effect
¶
register_effect(effect: EffectDef) -> None
Record an effect interface and index its operations.
Each operation's signature is checked in a scope carrying the interface binders and then its own, and may mention the interface being declared.
| PARAMETER | DESCRIPTION |
|---|---|
effect
|
The interface to register.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the interface or one of its operations is already registered, if a binder is shadowed, or if an argument or result type is ill-formed. |
Source code in src/quivers/qiec/checking.py
register_handler
¶
register_handler(handler: HandlerDef) -> None
Record a handler against the interface it handles.
Coverage is checked here rather than at construction, because it is a claim about the interface's operations and only the registry knows those.
| PARAMETER | DESCRIPTION |
|---|---|
handler
|
The handler signature to register.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the handler is already registered, if its telescope shadows a binder, if its input, output, or introduced row is ill-formed, if the interface it names is unknown or wrongly applied, if a clause covers an operation the interface does not declare, or if the handler claims totality while leaving an operation uncovered, or if an authored clause body fails to check, answers the wrong type, or resumes more often than its grade allows. |
Source code in src/quivers/qiec/checking.py
register_computation
¶
register_computation(signature: ComputationSignature) -> None
Record a computation's signature so calls can resolve to it.
Signatures are registered before any body is checked. A call therefore resolves whether the callee is declared above or below it, and mutual recursion needs no forward declaration.
| PARAMETER | DESCRIPTION |
|---|---|
signature
|
The signature to record.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If a computation with this identity is already registered, if its telescope shadows a binder, or if a parameter type, the result type, or the declared row is ill-formed. A duplicate identity is rejected rather than overwritten, since a call carrying that identity would otherwise resolve to whichever declaration happened to register last. |
Source code in src/quivers/qiec/checking.py
computation
¶
computation(computation: ComputationId) -> ComputationSignature
The registered signature with a given identity.
| PARAMETER | DESCRIPTION |
|---|---|
computation
|
The identity to resolve.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ComputationSignature
|
The registered signature. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If no computation is registered under that identity, which is how a call to an undeclared name is caught. |
Source code in src/quivers/qiec/checking.py
constructor
¶
constructor(constructor: ConstructorId) -> ConstructorDecl
The registered constructor with a given identity.
| PARAMETER | DESCRIPTION |
|---|---|
constructor
|
The identity to resolve.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ConstructorDecl
|
The registered declaration. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If no constructor is registered under that identity. The
underlying |
Source code in src/quivers/qiec/checking.py
handler
¶
handler(handler: HandlerId) -> HandlerDef
The registered handler with a given identity.
| PARAMETER | DESCRIPTION |
|---|---|
handler
|
The identity to resolve.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
HandlerDef
|
The registered signature. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If no handler is registered under that identity. |
Source code in src/quivers/qiec/checking.py
operation
¶
operation(operation: OperationId) -> tuple[EffectDef, OperationDef]
The operation with a given identity, and its owning interface.
| PARAMETER | DESCRIPTION |
|---|---|
operation
|
The identity to resolve.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[EffectDef, OperationDef]
|
The interface that declares the operation, and the operation itself. The interface comes back too because checking a request needs both. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If no operation is registered under that identity. |
Source code in src/quivers/qiec/checking.py
family_for_type
¶
family_for_type(type_: TypeApplication) -> FamilyDecl
The indexed family a type application is an instance of.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
The applied type whose family to find.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
FamilyDecl
|
The family whose type constructor the application names. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the application is ill-formed, or names a constructor no registered family declares, which is how a case analysis on a non-family type is rejected. |
Source code in src/quivers/qiec/checking.py
ResumptionType
dataclass
¶
The continuation available inside one handler clause body.
A resumption is not a value and cannot be stored, so it is not a local binding. It is a capability of the position instead: available inside a clause body and nowhere else.
| PARAMETER | DESCRIPTION |
|---|---|
result
|
What the resumed operation supplies, so a
TYPE:
|
answer
|
What resuming produces, which is the clause's own answer type.
TYPE:
|
effects
|
The row resuming performs.
TYPE:
|
StaticScope
dataclass
¶
StaticScope(types: tuple[tuple[str, Kind], ...] = (), indices: tuple[tuple[str, IndexSort], ...] = (), effects: tuple[str, ...] = ())
The three disjoint namespaces visible in a declaration body.
| PARAMETER | DESCRIPTION |
|---|---|
types
|
Type binders in scope, each with its kind.
TYPE:
|
indices
|
Index binders in scope, each with its sort.
TYPE:
|
effects
|
Effect binder names in scope.
TYPE:
|
names
property
¶
Every static name bound here, across all three namespaces.
| RETURNS | DESCRIPTION |
|---|---|
frozenset[str]
|
The union of the type, index, and effect binder names. The namespaces are disjoint by construction, so this is what shadowing is tested against. |
extend
¶
extend(telescope: Telescope, *, subject: str) -> StaticScope
Return this scope widened by a telescope's binders.
| PARAMETER | DESCRIPTION |
|---|---|
telescope
|
Binders to add. Each must be a type, index, or effect binder.
TYPE:
|
subject
|
What is being extended, named in any diagnostic so the error points at the declaration rather than at the scope.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
StaticScope
|
A scope carrying the original binders and the new ones. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If a binder is of an unknown class, or if its name is already bound. Shadowing is rejected rather than resolved so a static name always denotes one thing within a declaration. |
Source code in src/quivers/qiec/checking.py
type_kind
¶
type_kind(name: str) -> Kind | None
The kind of a type binder in scope.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The binder name to resolve.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Kind or None
|
The binder's kind, or None when |
Source code in src/quivers/qiec/checking.py
index_sort
¶
index_sort(name: str) -> IndexSort | None
The sort of an index binder in scope.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The binder name to resolve.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
IndexSort or None
|
The binder's sort, or None when |
Source code in src/quivers/qiec/checking.py
BranchPattern
dataclass
¶
BranchPattern(constructor: ConstructorId | None, guarded: bool = False)
The shape of one case branch, as coverage sees it.
| PARAMETER | DESCRIPTION |
|---|---|
constructor
|
The constructor the branch matches, or
TYPE:
|
guarded
|
Whether the branch carries a guard that may reject a matching value, which keeps it from counting toward completeness.
TYPE:
|
BranchRefinement
dataclass
¶
BranchRefinement(skolems: tuple[str, ...], givens: tuple[BranchGiven, ...], reachability: Reachability = UNKNOWN)
Rigid skolems and local equalities available inside one branch.
| PARAMETER | DESCRIPTION |
|---|---|
skolems
|
The names of the branch's rigid static variables.
TYPE:
|
givens
|
The equalities the branch's constructor makes available.
TYPE:
|
reachability
|
Whether the givens are jointly satisfiable, as far as the unifier decides.
TYPE:
|
CoverageResult
dataclass
¶
CoverageResult(status: CoverageStatus, missing: tuple[ConstructorId, ...] = (), duplicates: tuple[ConstructorId, ...] = ())
The outcome of checking branch patterns against a family.
| PARAMETER | DESCRIPTION |
|---|---|
status
|
Whether the patterns cover the family.
TYPE:
|
missing
|
Constructors no pattern matches.
TYPE:
|
duplicates
|
Constructors more than one pattern matches.
TYPE:
|
CoverageStatus
¶
Bases: str, Enum
Whether a set of branch patterns covers a family.
Reachability
¶
Bases: str, Enum
Whether a branch can be entered, as far as its equalities decide.
ConstructorDecl
dataclass
¶
ConstructorDecl(id: ConstructorId, family: FamilyId, name: str, telescope: Telescope, fields: tuple[FieldDef, ...], result_indices: tuple[StaticArgument, ...])
One GADT constructor.
Constructor-local telescope binders are rigid skolems while a branch is
checked. result_indices may mention those binders and thereby refine
the scrutinee indices.
| PARAMETER | DESCRIPTION |
|---|---|
id
|
Stable identity.
TYPE:
|
family
|
The family this constructor belongs to, which must list it.
TYPE:
|
name
|
Source name.
TYPE:
|
telescope
|
Binders local to the constructor. These become rigid skolems while a branch matching it is checked.
TYPE:
|
fields
|
The values the constructor carries, uniquely named.
TYPE:
|
result_indices
|
What the constructor fixes the family's indices to. One per family index, and may mention the local telescope, which is how matching refines the scrutinee's type.
TYPE:
|
__post_init__
¶
Reject a constructor whose telescope or fields are malformed.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the telescope is malformed or two fields share a name. |
Source code in src/quivers/qiec/declarations.py
FamilyDecl
dataclass
¶
FamilyDecl(id: FamilyId, name: str, parameters: Telescope, indices: Telescope, constructors: tuple[ConstructorId, ...], closed: bool = True)
A closed or opaque indexed data family.
parameters are uniform across every constructor. indices may be
refined by constructor results and therefore are kept separate even when
both are represented by index binders.
| PARAMETER | DESCRIPTION |
|---|---|
id
|
Stable identity.
TYPE:
|
name
|
Source name, used for display and for the derived type constructor.
TYPE:
|
parameters
|
Binders uniform across every constructor.
TYPE:
|
indices
|
Binders a constructor result may refine. Each must be marked refinable, which is what separates them from parameters.
TYPE:
|
constructors
|
The constructors this family declares, without repetition.
TYPE:
|
closed
|
Whether the constructor list is exhaustive. A closed family admits coverage checking; an opaque one does not.
TYPE:
|
type_constructor
property
¶
type_constructor: TypeConstructorRef
The type constructor this family introduces.
| RETURNS | DESCRIPTION |
|---|---|
TypeConstructorRef
|
A constructor whose identity is derived from the family's, taking the parameters and indices together as its telescope. Deriving rather than storing it keeps the two from drifting apart. |
__post_init__
¶
Reject a family whose binders or constructors are malformed.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If either telescope is malformed, a name is shared between a parameter and an index, an index is not marked refinable, or a constructor is listed twice. |
Source code in src/quivers/qiec/declarations.py
FieldDef
dataclass
¶
FieldDef(name: str, type: TypeExpr)
One named, typed field of a constructor.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The field's display name.
TYPE:
|
type
|
The field's type, which may mention the constructor's telescope.
TYPE:
|
DistributionBackend
¶
Bases: Protocol
What a host must supply to sample and score a family.
sample
¶
Draw one value.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family's source name.
TYPE:
|
arguments
|
The named parameters as host values.
TYPE:
|
rng
|
The generator to draw from.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
The drawn host value. |
Source code in src/quivers/qiec/distributions.py
log_prob
¶
Evaluate the log density at a value.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family's source name.
TYPE:
|
arguments
|
The named parameters as host values.
TYPE:
|
value
|
The point evaluated.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
float
|
The log density. |
Source code in src/quivers/qiec/distributions.py
log_mass
¶
The log of the total mass of a construction.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family's source name.
TYPE:
|
arguments
|
The named parameters as host values.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
float
|
Zero for a probability measure; the log mass of a restriction
or of a mixture of restrictions, which |
Source code in src/quivers/qiec/distributions.py
ReferenceBackend
¶
Plain-Python sampling and scoring for every family of the registry.
The scalar core lives beside the backend and the structured and
compositional families in :mod:quivers.qiec.reference_families; a
family outside the tables is reported by name rather than approximated,
so a host provider can be installed for it.
families
property
¶
The families this backend implements.
| RETURNS | DESCRIPTION |
|---|---|
frozenset[str]
|
The family names. |
sample
¶
Draw one value from an implemented family.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family's source name.
TYPE:
|
arguments
|
The named parameters as host values.
TYPE:
|
rng
|
The generator to draw from.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
The drawn value: a float, an int, a bool, or a tuple of floats. |
| RAISES | DESCRIPTION |
|---|---|
DistributionError
|
If the family is not implemented here or a parameter is missing or malformed. |
Source code in src/quivers/qiec/distributions.py
log_prob
¶
Evaluate the log density of an implemented family.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family's source name.
TYPE:
|
arguments
|
The named parameters as host values.
TYPE:
|
value
|
The point evaluated.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
float
|
The log density, |
| RAISES | DESCRIPTION |
|---|---|
DistributionError
|
If the family is not implemented here or a parameter or the point is malformed. |
Source code in src/quivers/qiec/distributions.py
log_mass
¶
The log of the total mass of a construction.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family's source name.
TYPE:
|
arguments
|
The named parameters as host values.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
float
|
The family's log mass, zero for every probability family. |
| RAISES | DESCRIPTION |
|---|---|
DistributionError
|
If the family is not implemented here. |
Source code in src/quivers/qiec/distributions.py
RuntimeDistribution
dataclass
¶
RuntimeDistribution(family: str, arguments: Mapping[str, object], batch: tuple[int, ...] = (), event: tuple[int, ...] = (), ranks: Mapping[str, int] = MappingProxyType({}), natural: tuple[int, ...] = ())
A constructed distribution, as host data.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family's source name.
TYPE:
|
arguments
|
The named parameters as host values; frozen on construction.
TYPE:
|
batch
|
The plate's batch extents, outermost first; each position is an independent draw scored on its own.
TYPE:
|
event
|
The plate's extended event extents, outermost first; draws along them join one event and are scored together.
TYPE:
|
ranks
|
Each parameter's own tensor rank, from the family registry, so an argument carrying plate dimensions can be told from one that does not.
TYPE:
|
natural
|
The family's own event extents, so a scalar given for a tensor parameter can be broadcast to the shape the family expects.
TYPE:
|
plated
property
¶
Whether the distribution is constructed over a plate.
| RETURNS | DESCRIPTION |
|---|---|
bool
|
|
__post_init__
¶
Freeze the arguments so a distribution value cannot drift.
Source code in src/quivers/qiec/distributions.py
at
¶
at(position: tuple[int, ...]) -> RuntimeDistribution
The distribution at one position of the plate, unplated.
| PARAMETER | DESCRIPTION |
|---|---|
position
|
A position of the leading plate axes, outermost first; fewer positions than axes leave the remaining axes in place.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeDistribution
|
The family with its arguments selected at the position and the selected axes dropped from the plate. |
| RAISES | DESCRIPTION |
|---|---|
DistributionError
|
If the position has more entries than the plate has axes. |
Source code in src/quivers/qiec/distributions.py
sample
¶
Draw one value through the installed backend.
| PARAMETER | DESCRIPTION |
|---|---|
rng
|
The generator to draw from; the module generator by default,
which :func:
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
The drawn host value: one draw of the family, or nested tuples of draws over the plate's batch and event axes. |
| RAISES | DESCRIPTION |
|---|---|
DistributionError
|
If the backend cannot sample the family. |
Source code in src/quivers/qiec/distributions.py
log_mass
¶
The log of the distribution's total mass through the installed backend.
| RETURNS | DESCRIPTION |
|---|---|
float
|
Zero for a probability measure; over a plate, the sum of the masses at every position, since the plate's draw is their product. |
Source code in src/quivers/qiec/distributions.py
log_prob
¶
Evaluate the log density at a value through the installed backend.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The point evaluated; over a plate, nested tuples of points shaped like the plate.
TYPE:
|
keep_batch
|
Whether to keep one weight per batch position rather than total them.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
The log density as a float, or, with |
| RAISES | DESCRIPTION |
|---|---|
DistributionError
|
If the backend cannot score the family, or the point is not shaped like the plate. |
Source code in src/quivers/qiec/distributions.py
ArgumentDef
dataclass
¶
ArgumentDef(name: str, type: TypeExpr)
One named, typed value argument of an operation.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The argument's display name.
TYPE:
|
type
|
The argument's type, which may mention the operation's telescope.
TYPE:
|
ComputationType
dataclass
¶
EffectDef
dataclass
¶
EffectDef(ref: EffectRef, telescope: Telescope, operations: tuple[OperationDef, ...])
An operation interface.
Identity is nominal: the declaration is fixed by its module and its
own name, carried in ref. Static arguments distinguish applications
of the interface without changing which declaration they apply.
| PARAMETER | DESCRIPTION |
|---|---|
ref
|
The declaration's own reference, which must be unsaturated: a declaration names the interface, and applying it is what supplies arguments.
TYPE:
|
telescope
|
Static binders the interface takes.
TYPE:
|
operations
|
The declared operations, unique by both identity and name.
TYPE:
|
__post_init__
¶
Validate the declaration against its operations.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the telescope is malformed, if |
Source code in src/quivers/qiec/effects.py
apply
¶
apply(arguments: tuple[StaticArgument, ...]) -> EffectRef
Instantiate the interface telescope as a concrete effect.
| PARAMETER | DESCRIPTION |
|---|---|
arguments
|
Static arguments to saturate the telescope with.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRef
|
The saturated application, carrying this declaration's identity together with the arguments given. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If an argument is of the wrong static class for its binder. |
ValueError
|
If the argument count does not match the telescope, or an argument is ill-kinded. |
Source code in src/quivers/qiec/effects.py
matches
¶
matches(effect: EffectRef) -> bool
Whether a concrete effect is a well-kinded application here.
| PARAMETER | DESCRIPTION |
|---|---|
effect
|
The saturated application to test.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
bool
|
True when |
Source code in src/quivers/qiec/effects.py
operation
¶
operation(operation: OperationId) -> OperationDef
The declared operation with a given identity.
| PARAMETER | DESCRIPTION |
|---|---|
operation
|
The identity to resolve.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
OperationDef
|
The matching declaration. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If this interface declares no such operation, which is how a request naming an operation another effect owns is caught. |
Source code in src/quivers/qiec/effects.py
EffectRequest
dataclass
¶
EffectRequest(instance: EffectInstanceId, effect: EffectRef, operation: OperationId, static_arguments: tuple[StaticArgument, ...], arguments: tuple[Value, ...], result_type: TypeExpr, origin: SiteProvenance, tag: Literal['effect_request'] = 'effect_request')
A typed request allocated before filtering or handler dispatch.
| PARAMETER | DESCRIPTION |
|---|---|
instance
|
The effect instance the request is addressed to.
TYPE:
|
effect
|
The instance's interface application.
TYPE:
|
operation
|
The operation requested.
TYPE:
|
static_arguments
|
The operation's telescope instantiation, in binder order.
TYPE:
|
arguments
|
The value arguments, one per operation argument.
TYPE:
|
result_type
|
The type of the value the operation returns under the instantiation.
TYPE:
|
origin
|
Where the request was written and how it was reached.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
EffectRow
dataclass
¶
EffectRow(entries: tuple[RowEntry, ...] = (), tail: RowVariable | None = None)
A finite map from lexical instance IDs to interfaces plus a tail.
Entries are sorted by stable identifier at construction time, so row equality is insensitive to source order. Two instances of the same interface remain distinct entries.
| PARAMETER | DESCRIPTION |
|---|---|
entries
|
The instances the row names, each with its interface; any order is accepted and normalized.
TYPE:
|
tail
|
A row variable standing for further entries, or
TYPE:
|
__post_init__
¶
Sort the entries and reject a row that cannot be well formed.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If one lexical instance appears twice, or if the row is open and its tail does not prove it lacks every explicit entry. Without that proof the tail could later be instantiated to a row repeating an instance already named here. |
Source code in src/quivers/qiec/effects.py
lookup
¶
lookup(instance: EffectInstanceId) -> EffectRef | None
The interface an instance implements in this row.
| PARAMETER | DESCRIPTION |
|---|---|
instance
|
The lexical instance to resolve.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRef or None
|
The interface when the row carries the instance explicitly, and None otherwise. An open tail is not consulted, so None means absent from the explicit entries rather than absent from every instantiation of the row. |
Source code in src/quivers/qiec/effects.py
contains
¶
contains(instance: EffectInstanceId) -> bool
Whether the row carries an explicit entry for an instance.
| PARAMETER | DESCRIPTION |
|---|---|
instance
|
The lexical instance to test.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
bool
|
True when an explicit entry names the instance. |
Source code in src/quivers/qiec/effects.py
add
¶
Return this row extended with one entry.
| PARAMETER | DESCRIPTION |
|---|---|
entry
|
The instance and interface to add. Re-adding an entry the row already carries returns the row unchanged, so the operation is idempotent.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRow
|
The extended row. When the row is open, its tail gains a lacks
constraint for the new instance, which keeps the invariant
|
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the row already binds this instance to a different interface, since one lexical instance implements one interface. |
Source code in src/quivers/qiec/effects.py
without
¶
without(instance: EffectInstanceId) -> EffectRow
Return this row with one instance discharged.
| PARAMETER | DESCRIPTION |
|---|---|
instance
|
The lexical instance to remove, as a handler does when it handles every operation of that instance.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRow
|
The row without that entry, keeping the tail as it was. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If the row carries no explicit entry for the instance. This is an error rather than a no-op because discharging an effect the row never had indicates the caller has the wrong row. |
Source code in src/quivers/qiec/effects.py
union
¶
Union two rows, preserving a compatible open tail.
| PARAMETER | DESCRIPTION |
|---|---|
other
|
The row to merge in.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRow
|
A row carrying every entry of both. When both are open their tails are merged, and the surviving tail is constrained to lack every explicit instance on either side. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the two rows bind one instance to different interfaces, or if their tails are distinct variables and so cannot merge. |
Source code in src/quivers/qiec/effects.py
HandlerClauseDef
dataclass
¶
HandlerClauseDef(operation: OperationId, grade: ResumptionGrade, parameters: tuple[Local, ...] = (), body: Computation | None = None)
One operation a handler covers, and how it may resume.
| PARAMETER | DESCRIPTION |
|---|---|
operation
|
The operation this clause handles.
TYPE:
|
grade
|
How often the clause may invoke its continuation. The grade is part of the clause contract and is checked against the body.
TYPE:
|
parameters
|
Binders for the operation's value arguments, in declaration order. The body refers to the request's arguments through these.
TYPE:
|
body
|
What the clause does.
TYPE:
|
HandlerDef
dataclass
¶
HandlerDef(id: HandlerId, name: str, effect: EffectRef, clauses: tuple[HandlerClauseDef, ...], input_type: TypeExpr, output_type: TypeExpr, introduced: EffectRow = EMPTY_ROW, total: bool = True, forwards_unknown: bool = False, telescope: Telescope = (), return_clause: HandlerReturnClauseDef | None = None, implementation: Literal['authored', 'foreign'] = 'foreign')
Serializable type-and-coverage signature for a handler.
An authored handler carries its clause bodies in the stable core; a
foreign handler's bodies are runtime attachments keyed by id.
| PARAMETER | DESCRIPTION |
|---|---|
id
|
The handler's stable identity.
TYPE:
|
name
|
The handler's display name.
TYPE:
|
effect
|
The interface application the handler handles.
TYPE:
|
clauses
|
One clause per operation the handler covers.
TYPE:
|
input_type
|
The result type of the computation the handler accepts.
TYPE:
|
output_type
|
The type of the handler's answer.
TYPE:
|
introduced
|
The effects the handler's own clauses perform, which the residual row of a handled computation gains. |
total
|
Whether the clauses cover every operation of
TYPE:
|
forwards_unknown
|
Whether an operation no clause covers is forwarded outward rather
than rejected; incompatible with
TYPE:
|
telescope
|
The static parameters the handler abstracts over, in order.
TYPE:
|
return_clause
|
How the handler answers the computation's return, or
TYPE:
|
implementation
|
TYPE:
|
__post_init__
¶
Validate the clause set against the coverage claim.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the telescope is malformed, if two clauses cover the same operation, if the handler claims to be both total and forwarding, or if its bodies disagree with its declared implementation. A total handler covering every operation has nothing left to forward. An authored handler missing a body has nowhere for that operation's behavior to live, and a body on a foreign handler would be ignored in favour of its runtime provider; both are worse than being rejected. |
Source code in src/quivers/qiec/effects.py
clause
¶
clause(operation: OperationId) -> HandlerClauseDef | None
The clause covering an operation, if this handler has one.
| PARAMETER | DESCRIPTION |
|---|---|
operation
|
The operation to look for.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
HandlerClauseDef or None
|
The clause, or None when the operation is uncovered. For a forwarding handler None means the request passes through rather than that it is an error. |
Source code in src/quivers/qiec/effects.py
HandlerReturnClauseDef
dataclass
¶
HandlerReturnClauseDef(binder: Local, body: Computation)
What a handler does with a value its computation returns.
Separate from an operation clause because it answers a different thing: an operation clause responds to a request and may resume, while this responds to the computation finishing and has no continuation to invoke.
| PARAMETER | DESCRIPTION |
|---|---|
binder
|
Names the returned value inside the body.
TYPE:
|
body
|
What the handler produces from it. There is no signature-only form: a handler that answers returns at all has to say how.
TYPE:
|
OperationDef
dataclass
¶
OperationDef(id: OperationId, name: str, telescope: Telescope, arguments: tuple[ArgumentDef, ...], result_type: TypeExpr)
One result-indexed request constructor in an effect interface.
| PARAMETER | DESCRIPTION |
|---|---|
id
|
Stable identity, derived from the owning effect and this operation's name.
TYPE:
|
name
|
Source name, as written in the effect declaration.
TYPE:
|
telescope
|
Static binders this operation introduces on top of the interface's own. They may not shadow the interface binders.
TYPE:
|
arguments
|
Value arguments the request carries, named uniquely.
TYPE:
|
result_type
|
What resuming the request supplies, possibly mentioning the binders above.
TYPE:
|
__post_init__
¶
Validate the telescope and the argument names.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the telescope is malformed, or two arguments share a name. |
Source code in src/quivers/qiec/effects.py
ResumptionGrade
¶
Bases: str, Enum
Quantitative use allowed for a handler-clause resumption.
RowEntry
dataclass
¶
RowEntry(instance: EffectInstanceId, effect: EffectRef)
One lexical effect instance and the interface it implements.
| PARAMETER | DESCRIPTION |
|---|---|
instance
|
The lexical instance. Two instances of one interface stay
distinct, so this rather than
TYPE:
|
effect
|
The saturated interface application the instance implements.
TYPE:
|
RowSubstitution
dataclass
¶
RowSubstitution(bindings: tuple[tuple[RowVariableId, EffectRow], ...] = ())
A finite, occurs-checked substitution for stable row variables.
| PARAMETER | DESCRIPTION |
|---|---|
bindings
|
What each row variable stands for. At most one binding per variable, and no binding whose row is tailed by the variable it replaces.
TYPE:
|
__post_init__
¶
Reject a substitution that is ambiguous or immediately cyclic.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If one variable is bound twice, or if a variable is bound to a row whose own tail is that same variable. The second is the occurs check at depth one; deeper cycles are caught while applying the substitution. |
Source code in src/quivers/qiec/effects.py
lookup
¶
lookup(variable: RowVariable) -> EffectRow | None
The row a variable stands for under this substitution.
| PARAMETER | DESCRIPTION |
|---|---|
variable
|
The variable to resolve, matched on its identity rather than its display name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRow or None
|
The bound row, or None when the variable is unbound and so remains an open tail. |
Source code in src/quivers/qiec/effects.py
apply
¶
Replace this row's tail, and any tail it resolves to.
| PARAMETER | DESCRIPTION |
|---|---|
row
|
The row to substitute into. A closed row is returned as is.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRow
|
The row with its tail resolved as far as the bindings reach. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the bindings are cyclic, or if resolving a tail would introduce an instance that tail was proven to lack. |
Source code in src/quivers/qiec/effects.py
RowUnification
dataclass
¶
RowUnification(row: EffectRow, substitution: RowSubstitution = RowSubstitution())
The common row two rows unify to, and how their tails were bound.
| PARAMETER | DESCRIPTION |
|---|---|
row
|
The unified row.
TYPE:
|
substitution
|
The bindings that carry each input row to
TYPE:
|
RowVariable
dataclass
¶
RowVariable(name: str, identity: RowVariableId, lacks: tuple[EffectInstanceId, ...] = ())
The open tail of an effect row, with the instances it excludes.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
Display name, used in diagnostics only. Two variables with the same identity and different names are the same variable.
TYPE:
|
identity
|
Stable identity. Equality and hashing are taken from this rather
than from
TYPE:
|
lacks
|
Instances the tail is proven not to contain. Sorted at construction, so equality is insensitive to the order given.
TYPE:
|
__post_init__
¶
Sort the lacks constraints and reject a malformed variable.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If |
Source code in src/quivers/qiec/effects.py
proves_lacks
¶
proves_lacks(instance: EffectInstanceId) -> bool
Whether this tail is known not to contain instance.
| PARAMETER | DESCRIPTION |
|---|---|
instance
|
The lexical instance to test.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
bool
|
True when the constraint is carried, which is what permits an
explicit entry for |
Source code in src/quivers/qiec/effects.py
__eq__
¶
Compare by identity and constraints, ignoring the display name.
| PARAMETER | DESCRIPTION |
|---|---|
other
|
The value to compare against.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
bool
|
True when |
Source code in src/quivers/qiec/effects.py
__hash__
¶
Hash the fields that __eq__ compares.
| RETURNS | DESCRIPTION |
|---|---|
int
|
A hash of the identity and the lacks constraints. |
merge
¶
merge(other: RowVariable) -> RowVariable
Unify two occurrences, accumulating their lacks constraints.
| PARAMETER | DESCRIPTION |
|---|---|
other
|
Another occurrence of the same variable.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RowVariable
|
One variable carrying the union of both constraint sets, which is sound because each occurrence's constraints hold of the single variable they both name. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the two variables have different identities, and so are not occurrences of one variable at all. |
Source code in src/quivers/qiec/effects.py
with_lacks
¶
with_lacks(instances: tuple[EffectInstanceId, ...]) -> RowVariable
Return this variable with further instances excluded.
| PARAMETER | DESCRIPTION |
|---|---|
instances
|
Instances to add to the constraint set. Instances already excluded are absorbed rather than repeated.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RowVariable
|
A variable of the same identity carrying the wider constraint. |
Source code in src/quivers/qiec/effects.py
EntryParameter
didactic-model
¶
Bases: Model
One value parameter of an entry point.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The parameter's name.
TYPE:
|
type
|
Its type, rendered in the surface spelling.
TYPE:
|
role
|
How a program parameter is supplied (its data, an observation, a
fibration, a scalar, or the program's domain);
TYPE:
|
EntryPoint
didactic-model
¶
EntryPoint(*, name: str, kind: EntryKind, parameters: tuple[EntryParameter, ...], statics: tuple[str, ...], effects: tuple[str, ...], result: str, sites: tuple[str, ...])
Bases: Model
An executable entry point of a checked module.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The entry's source name.
TYPE:
|
kind
|
Whether it is a
TYPE:
|
parameters
|
Its value parameters, in order.
TYPE:
|
statics
|
The names of the static binders its telescope takes, in order.
TYPE:
|
effects
|
The effect instances its body performs, rendered as
TYPE:
|
result
|
Its result type, rendered.
TYPE:
|
sites
|
The labels of a program's sample sites, which a run may condition on; empty for a computation.
TYPE:
|
EntryRun
dataclass
¶
EntryRun(entry: EntryPoint, value: HostValue, log_joint: float | None, result: ExecutionResult)
What invoking an entry point produced.
| PARAMETER | DESCRIPTION |
|---|---|
entry
|
The entry invoked.
TYPE:
|
value
|
The validated host value the entry returned.
TYPE:
|
log_joint
|
The log joint density a program run accumulated, or
TYPE:
|
result
|
The underlying execution result, with its trace.
TYPE:
|
to_data
¶
Render the run as JSON-compatible data.
| RETURNS | DESCRIPTION |
|---|---|
dict[str, object]
|
The execution result's data, with the entry's kind and, for a program, the log joint. |
Source code in src/quivers/qiec/entries.py
AttachmentBinding
dataclass
¶
AttachmentBinding(value: object, type: TypeExpr, validator: RuntimeValidator, duplicable: bool = False)
One host value attached to an otherwise serializable core term.
duplicable is a semantic assertion about the host value, not merely a
promise that copy.copy happens to work. Multi-shot resumptions reject
captured attachment values unless this bit was supplied explicitly.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The host value.
TYPE:
|
type
|
The type the value inhabits.
TYPE:
|
validator
|
The predicate that checks a host value against
TYPE:
|
duplicable
|
Whether an unrestricted resumption may capture the value.
TYPE:
|
ClauseComputation
dataclass
¶
ClauseComputation(computation: Computation, bindings: tuple[tuple[Local, object], ...] = ())
Ask the evaluator to run a structural clause body outside the handler.
Host values introduced by a handler must first be installed through
:meth:ClauseContext.attach; arbitrary callback closures do not enter the
computation tree.
| PARAMETER | DESCRIPTION |
|---|---|
computation
|
The stable computation to run.
TYPE:
|
bindings
|
Locals the computation refers to, each with its evaluated value.
TYPE:
|
ClauseContext
¶
ClauseContext(evaluator: Evaluator, environment: Mapping[Local, object], outer_stack: tuple[ContinuationFrame, ...], resumption_path: tuple[int, ...], request: RuntimeRequest | None)
Disciplined runtime services available to an attached handler clause.
| PARAMETER | DESCRIPTION |
|---|---|
evaluator
|
The evaluator running the clause.
TYPE:
|
environment
|
The bindings in scope at the handler.
TYPE:
|
outer_stack
|
The continuation frames outside the handler.
TYPE:
|
resumption_path
|
The ordinal of each resumption taken to reach the clause.
TYPE:
|
request
|
The request the clause answers, or
TYPE:
|
Source code in src/quivers/qiec/evaluator.py
request
property
¶
request: RuntimeRequest | None
The request this clause is answering.
| RETURNS | DESCRIPTION |
|---|---|
RuntimeRequest or None
|
The request, or None in a return clause, which answers a completed computation rather than an operation. |
attachments
property
¶
attachments: RuntimeAttachments
The host values available to this clause.
| RETURNS | DESCRIPTION |
|---|---|
RuntimeAttachments
|
The evaluator's attachment table. |
evaluate
¶
evaluate(computation: Computation) -> object
Evaluate a clause body in the outer handler context.
A delimiter prevents the clause body from consuming the continuation outside the handled expression. Effects performed here can reach only handlers outside the matched handler, which is the chosen deep-handler semantics.
| PARAMETER | DESCRIPTION |
|---|---|
computation
|
The clause body to run.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
What the body produced. |
Source code in src/quivers/qiec/evaluator.py
attach
¶
attach(value: object, type: TypeExpr, *, role: str, validator: RuntimeValidator = _accept, duplicable: bool = False) -> AttachmentRef
Install a generated host value under a deterministic runtime ID.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The host value to attach.
TYPE:
|
type
|
The type the core ascribes to it.
TYPE:
|
role
|
What the value is for, which enters its derived identity.
TYPE:
|
validator
|
Checks the value inhabits the type.
TYPE:
|
duplicable
|
Whether the value may be copied by a multi-shot resumption.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
AttachmentRef
|
A reference usable in a core term. The identity derives from the run, the request, and the role rather than being generated, so a trace can name the same attachment twice. |
Source code in src/quivers/qiec/evaluator.py
ContinuationFrame
¶
One frame of the reference evaluator's explicit continuation stack.
The evaluator creates and consumes every frame. A handler clause sees
frames only through the :class:ClauseContext and :class:Resumption
the evaluator hands it, and never inspects or builds one itself; the
class exists so those two constructors can name the stack they capture.
EvaluationError
¶
Bases: RuntimeError
Base class for failures at the typed-core/runtime boundary.
Evaluator
¶
Evaluator(attachments: RuntimeAttachments | None = None, *, handler_manifest: HandlerManifest | None = None, trace_hook: EvaluationTraceHook | None = None, module: QiecModule | None = None, fuel: int | None = None, type_validator: Callable[[TypeExpr], RuntimeValidator | None] | None = None)
Execute QIEC computations with explicit runtime attachments.
| PARAMETER | DESCRIPTION |
|---|---|
attachments
|
The host values and handlers available; empty by default.
TYPE:
|
handler_manifest
|
Checked handler definitions every attached handler must match
exactly on each :meth:
TYPE:
|
trace_hook
|
Called with each execution event's name and payload, or
TYPE:
|
module
|
The module whose named computations calls resolve to and whose
authored handlers
TYPE:
|
fuel
|
The number of machine steps a run may take before failing with
:class:
TYPE:
|
type_validator
|
Supplies the host validator for a type at an authored handler's
boundaries: the values it is resumed with, the handled
computation's result, and its answer.
TYPE:
|
Source code in src/quivers/qiec/evaluator.py
evaluate
¶
evaluate(computation: Computation, environment: Mapping[Local, object] | None = None) -> object
Evaluate a closed or explicitly supplied computation.
| PARAMETER | DESCRIPTION |
|---|---|
computation
|
The computation to run.
TYPE:
|
environment
|
Values for the computation's free locals. None means it is closed.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
What the computation produced. |
| RAISES | DESCRIPTION |
|---|---|
EvaluationError
|
If a request reaches no handler, a handler is missing from the manifest, a resumption exceeds its grade, or a host value fails validation. |
Source code in src/quivers/qiec/evaluator.py
evaluate_checked
¶
evaluate_checked(computation: Computation, registry: KernelRegistry, environment: Mapping[Local, object] | None = None) -> object
Kernel-check a computation and fail closed on handler attachments.
| PARAMETER | DESCRIPTION |
|---|---|
computation
|
The computation to run.
TYPE:
|
registry
|
Declarations to check it against.
TYPE:
|
environment
|
Values for its free locals.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
What the computation produced. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the computation does not check. |
EvaluationError
|
If execution fails, as in |
Source code in src/quivers/qiec/evaluator.py
evaluate_validated
¶
evaluate_validated(computation: Computation, registry: KernelRegistry, environment: Mapping[Local, object] | None = None) -> object
Run a computation a module validation has already checked.
validate_module checks every body of a module against its
registry; a caller holding that registry runs such a body
without checking it again. The handler manifest is still held
against the attachments.
| PARAMETER | DESCRIPTION |
|---|---|
computation
|
The computation to run, a body of the validated module.
TYPE:
|
registry
|
The registry the module validated against.
TYPE:
|
environment
|
Values for its free locals.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
What the computation produced. |
| RAISES | DESCRIPTION |
|---|---|
EvaluationError
|
If execution fails, as in |
Source code in src/quivers/qiec/evaluator.py
evaluate_value
¶
Erase and evaluate a checked QIEC value.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The value to evaluate.
TYPE:
|
environment
|
Values for its free locals.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
The host representation of the value. |
Source code in src/quivers/qiec/evaluator.py
Forward
dataclass
¶
Forward(on_response: ResponseHook | None = None)
Forward a request to an outer handler, optionally observing its reply.
| PARAMETER | DESCRIPTION |
|---|---|
on_response
|
Called with the outer handler's answer before it reaches the
resumed computation, or
TYPE:
|
FuelExhaustedError
¶
Bases: EvaluationError
The step budget ran out before the computation finished.
General recursion is allowed to diverge, so a budget is the only way a caller can bound a run. Exhaustion is reported as an ordinary evaluation failure rather than a host recursion error, which the machine's explicit stack never raises.
| PARAMETER | DESCRIPTION |
|---|---|
steps
|
The budget that was exhausted; kept on the error as
TYPE:
|
Source code in src/quivers/qiec/evaluator.py
HandlerManifest
dataclass
¶
HandlerManifest(definitions: Mapping[HandlerId, HandlerDef])
Immutable checked handler definitions accepted by an evaluator.
Construct this from a :class:KernelRegistry after its declarations have
passed kernel registration. Runtime clause objects are then accepted only
when their complete structural definitions equal the manifest entry, not
merely when their stable IDs collide.
| PARAMETER | DESCRIPTION |
|---|---|
definitions
|
The checked handler definitions by identity.
TYPE:
|
__post_init__
¶
Freeze the definitions behind a read-only view.
The manifest is what a runtime resolves a handler through, so it is copied and wrapped rather than aliased: a caller mutating the mapping it passed in would otherwise change which handler a running computation reaches.
Source code in src/quivers/qiec/evaluator.py
from_registry
classmethod
¶
from_registry(registry: KernelRegistry) -> HandlerManifest
Build a manifest from a checked registry.
| PARAMETER | DESCRIPTION |
|---|---|
registry
|
A registry whose handlers have already been checked.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
HandlerManifest
|
A manifest over those handlers. |
Source code in src/quivers/qiec/evaluator.py
InvalidHandlerError
¶
Bases: EvaluationError
A runtime handler contradicts its checked structural signature.
MissingAttachmentError
¶
Bases: EvaluationError
A stable runtime reference has no value or handler attachment.
NonDuplicableContinuationError
¶
Bases: ResumptionUsageError
An unrestricted clause captured state that cannot safely be copied.
Resumption
¶
Resumption(evaluator: Evaluator, request: RuntimeRequest, grade: ResumptionGrade, captured_environment: Mapping[Local, object], captured_stack: tuple[ContinuationFrame, ...], outer_stack: tuple[ContinuationFrame, ...], validator: RuntimeValidator, path: tuple[int, ...])
Dynamically checked, delimited continuation supplied to one clause.
| PARAMETER | DESCRIPTION |
|---|---|
evaluator
|
The evaluator that captured the continuation.
TYPE:
|
request
|
The request whose result the continuation awaits.
TYPE:
|
grade
|
How often the clause may invoke the continuation.
TYPE:
|
captured_environment
|
The bindings in scope at the request.
TYPE:
|
captured_stack
|
The continuation frames between the request and the handler.
TYPE:
|
outer_stack
|
The continuation frames outside the handler.
TYPE:
|
validator
|
The predicate every resumed value must pass.
TYPE:
|
path
|
The ordinal of each resumption taken to reach the clause.
TYPE:
|
Source code in src/quivers/qiec/evaluator.py
grade
property
¶
grade: ResumptionGrade
The grade this resumption is held to.
| RETURNS | DESCRIPTION |
|---|---|
ResumptionGrade
|
The declared grade, checked statically and again here. |
calls
property
¶
How many times this resumption has been invoked so far.
| RETURNS | DESCRIPTION |
|---|---|
int
|
The count, which the grade bounds. |
__call__
¶
Resume the suspended computation with a value.
The static analysis already rejects a clause that can exceed its grade. This guard stays because it protects against a foreign handler, whose body the analysis never saw, and against a compiler bug: a grade is what lets a runtime discard a continuation, so exceeding it is not recoverable.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
What the resumed operation supplies.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
What the resumed computation produced. |
| RAISES | DESCRIPTION |
|---|---|
ResumptionUsageError
|
If the grade is zero, or an affine or linear resumption is invoked more than once. |
NonDuplicableContinuationError
|
If an unrestricted resumption would have to copy a captured value that is not duplicable. |
RuntimeValidationError
|
If the value does not inhabit the operation's result type. |
Source code in src/quivers/qiec/evaluator.py
ResumptionUsageError
¶
Bases: EvaluationError
A handler clause used its resumption outside the declared grade.
RuntimeAttachments
dataclass
¶
RuntimeAttachments(values: dict[AttachmentId, AttachmentBinding] = dict(), handlers: dict[HandlerId, RuntimeHandler] = dict())
Process-local values and handlers keyed by stable core identifiers.
| PARAMETER | DESCRIPTION |
|---|---|
values
|
Attached host values by attachment identity.
TYPE:
|
handlers
|
Runtime handlers by handler identity.
TYPE:
|
bind_value
¶
bind_value(attachment: AttachmentId, value: object, type: TypeExpr, *, validator: RuntimeValidator = _accept, duplicable: bool = False) -> AttachmentRef
Attach a host value and return its stable core reference.
| PARAMETER | DESCRIPTION |
|---|---|
attachment
|
The identity the core term refers to the value by.
TYPE:
|
value
|
The host value.
TYPE:
|
type
|
The type the core ascribes to it.
TYPE:
|
validator
|
Checks the value really inhabits that type. The default accepts anything, for a value the static check already settles.
TYPE:
|
duplicable
|
Whether the value may be copied. This is an assertion about the value, not a guess: a multi-shot resumption capturing a non-duplicable attachment is refused, because copying it would give two continuations a shared mutable thing.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
AttachmentRef
|
The core reference to use in a term. |
| RAISES | DESCRIPTION |
|---|---|
InvalidHandlerError
|
If the identity is already bound to a different value, type, validator, or duplicability. Rebinding is refused rather than overwriting, since a term already built would silently start meaning something else. |
RuntimeValidationError
|
If the validator rejects the value. |
Source code in src/quivers/qiec/evaluator.py
bind_handler
¶
bind_handler(handler: RuntimeHandler) -> HandlerId
Attach executable clauses to their structural handler identity.
| PARAMETER | DESCRIPTION |
|---|---|
handler
|
The executable handler, already checked against its declaration.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
HandlerId
|
The identity it was bound under. |
| RAISES | DESCRIPTION |
|---|---|
InvalidHandlerError
|
If a different handler is already bound to that identity. |
Source code in src/quivers/qiec/evaluator.py
RuntimeClause
dataclass
¶
RuntimeClause(invoke: OperationClause, result_validator: RuntimeValidator)
Executable operation clause and validator for the resumed value.
| PARAMETER | DESCRIPTION |
|---|---|
invoke
|
The clause body, called with the request, its resumption, and a clause context.
TYPE:
|
result_validator
|
The predicate every value resumed through this clause must pass.
TYPE:
|
RuntimeConstructor
dataclass
¶
RuntimeConstructor(constructor: object, static_arguments: tuple[object, ...], fields: tuple[object, ...], result_type: TypeExpr)
Erased runtime representation of a checked constructor value.
| PARAMETER | DESCRIPTION |
|---|---|
constructor
|
The constructor's stable identity.
TYPE:
|
static_arguments
|
The constructor's telescope instantiation, as evaluated static data.
TYPE:
|
fields
|
The evaluated field values, in declaration order.
TYPE:
|
result_type
|
The family type the value inhabits.
TYPE:
|
RuntimeHandler
dataclass
¶
RuntimeHandler(definition: HandlerDef, clauses: Mapping[OperationId, RuntimeClause], return_clause: ReturnClause = _identity_return, input_validator: RuntimeValidator = _accept, output_validator: RuntimeValidator = _accept, duplicable_context: bool = False, mutable_context: bool = False, fork_context: Callable[['RuntimeHandler'], 'RuntimeHandler'] | None = None, context_factory: Callable[[], 'RuntimeHandler'] | None = None, on_enter: Callable[[], None] | None = None, on_exit: Callable[[], None] | None = None, on_drop: Callable[[], None] | None = None)
Executable attachment for a structural :class:HandlerDef.
The checked definition contains coverage, grades, input/output types, and introduced effects. This attachment contains only process-local code and state. It is never serialized as QIEC.
| PARAMETER | DESCRIPTION |
|---|---|
definition
|
The checked declaration this attachment implements.
TYPE:
|
clauses
|
One runtime clause per covered operation, by identity.
TYPE:
|
return_clause
|
How the handler answers the computation's return; the identity return by default.
TYPE:
|
input_validator
|
The predicate the handled computation's result must pass.
TYPE:
|
output_validator
|
The predicate the handler's answer must pass.
TYPE:
|
duplicable_context
|
Whether an unrestricted resumption may capture an installation of this handler.
TYPE:
|
mutable_context
|
Whether an installation carries state; such a handler needs a
TYPE:
|
fork_context
|
Builds an independent copy of an installation for another shot; required when the context is both mutable and duplicable.
TYPE:
|
context_factory
|
Builds a fresh installation each time the handler is installed.
TYPE:
|
on_enter
|
Called when an installation is entered.
TYPE:
|
on_exit
|
Called once when the handled computation completes.
TYPE:
|
on_drop
|
Called once when the handled computation is abandoned instead;
exclusive with
TYPE:
|
__post_init__
¶
Check the executable clauses against the checked declaration.
| RAISES | DESCRIPTION |
|---|---|
InvalidHandlerError
|
If the runtime implements an operation the declaration does not cover, or leaves a declared one unimplemented. Both directions matter: an extra clause would never be dispatched to, and a missing one would fail only when that operation was first performed, perhaps long after the handler was installed. |
Source code in src/quivers/qiec/evaluator.py
RuntimeRequest
dataclass
¶
RuntimeRequest(core: EffectRequest, arguments: tuple[object, ...], resumption_path: tuple[int, ...], dynamic_path: tuple[DynamicAddressFrame, ...] = ())
An evaluated request supplied to a process-local handler clause.
| PARAMETER | DESCRIPTION |
|---|---|
core
|
The stable request as written, before evaluation.
TYPE:
|
arguments
|
The evaluated value arguments, in order.
TYPE:
|
resumption_path
|
The ordinal of each resumption taken to reach this request.
TYPE:
|
dynamic_path
|
The call and local-instance frames live when the request was performed, outermost first, so one site reached through two recursive iterations yields two addresses.
TYPE:
|
instance
property
¶
instance: EffectInstanceId
The lexical instance this request was performed on.
| RETURNS | DESCRIPTION |
|---|---|
EffectInstanceId
|
The instance, which decides which handler answers. |
operation
property
¶
operation: OperationId
The operation requested.
| RETURNS | DESCRIPTION |
|---|---|
OperationId
|
The operation, which decides which clause answers. |
address
property
¶
Return the static, dynamic, and multi-shot address components.
| RETURNS | DESCRIPTION |
|---|---|
tuple[str, tuple[tuple[str, str | int], ...], tuple[int, ...]]
|
The source site, the dynamic address frames, and the resumption path. One request site reached twice, under a loop or under a resumed continuation, yields two addresses, which is what lets a trace name each occurrence separately. |
RuntimeTypeMismatch
¶
Bases: EvaluationError
A host result failed the validator for its QIEC result type.
TailResume
dataclass
¶
Resume a clause's continuation in place, on the machine's own stack.
A foreign clause that answers with this resumes once, exactly as an
authored resume(value) in tail position does: the captured frames
return to the machine's stack and the handler's return clause applies
when the computation completes. Unlike calling the resumption from
the clause, which drives the continuation in a nested host call that
stays pending until it returns, this leaves no host frame behind, so a
multi-shot resumption captured later inside the same handler may run
the continuation any number of times.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
What the resumed operation supplies.
TYPE:
|
UnhandledEffectError
¶
UnhandledEffectError(request: EffectRequest)
Bases: EvaluationError
No enclosing lexical handler accepts an effect request.
| PARAMETER | DESCRIPTION |
|---|---|
request
|
The request nothing handled; kept on the error as
TYPE:
|
Source code in src/quivers/qiec/evaluator.py
UnknownComputationError
¶
Bases: EvaluationError
A call names a computation the evaluator was not given a body for.
BranchGiven
dataclass
¶
BranchGiven(id: EqualityId, equality: EqualityType, tag: Literal['branch_given'] = 'branch_given')
Evidence granted by a case branch's constructor refinement.
| PARAMETER | DESCRIPTION |
|---|---|
id
|
The stable identity of the given, derived from the branch scope.
TYPE:
|
equality
|
The proposition the branch's constructor makes available.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
Reflexivity
dataclass
¶
Reflexivity(equality: EqualityType, tag: Literal['reflexivity'] = 'reflexivity')
Evidence that an equality holds because both sides are the same term.
| PARAMETER | DESCRIPTION |
|---|---|
equality
|
The proposition witnessed, whose sides must be equal.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
CoreRuntimeProvider
dataclass
¶
Primitive validators plus explicitly configured structural handlers.
options.handlers maps authored handler names to either
{"kind": "passthrough"}, {"kind": "state", "initial": ...},
or {"kind": "scripted", "responses": {"op": [...]}}. The source
handler still controls types, coverage, and resumption grades; options
supply only process-local clause behavior and state.
| PARAMETER | DESCRIPTION |
|---|---|
options
|
JSON-compatible configuration; frozen on construction.
TYPE:
|
name
|
The provider's name, reported in traces and result labels.
TYPE:
|
__post_init__
¶
attach
¶
attach(module: QiecModule, attachments: RuntimeAttachments) -> None
Bind one structural handler per configured authored handler.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The validated module whose handlers the configuration names.
TYPE:
|
attachments
|
The per-invocation table receiving the constructed handlers.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If |
Source code in src/quivers/qiec/execution.py
591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 | |
validator_for
¶
validator_for(type_: TypeExpr) -> RuntimeValidator | None
Supply the primitive validator for a closed runtime type.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
The closed QIEC type an argument or result must inhabit.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeValidator | None
|
The core validator, or |
Source code in src/quivers/qiec/execution.py
ExecutionDiagnostic
dataclass
¶
ExecutionDiagnostic(code: str, message: str, computation: str | None = None, origin: SourceOrigin | None = None, severity: Literal['error', 'warning', 'note'] = 'error')
A stable failure at the source-to-host execution boundary.
| PARAMETER | DESCRIPTION |
|---|---|
code
|
The stable diagnostic code, such as
TYPE:
|
message
|
The human-readable explanation.
TYPE:
|
computation
|
The named computation involved, if any.
TYPE:
|
origin
|
The source location involved, if any.
TYPE:
|
severity
|
TYPE:
|
to_data
¶
Render the diagnostic as JSON-compatible data.
| RETURNS | DESCRIPTION |
|---|---|
dict[str, object]
|
The code, severity, message, computation name, and origin (or
|
Source code in src/quivers/qiec/execution.py
ExecutionFailure
¶
ExecutionFailure(diagnostic: ExecutionDiagnostic)
Bases: EvaluationError
Raised with a serializable diagnostic when named execution cannot run.
| PARAMETER | DESCRIPTION |
|---|---|
diagnostic
|
The failure, kept on the error as
TYPE:
|
Source code in src/quivers/qiec/execution.py
ExecutionResult
dataclass
¶
ExecutionResult(computation: str, value: object, result_type: TypeExpr, runtime: str, trace: tuple[ExecutionTraceEvent, ...])
The checked value and trace produced by one named invocation.
| PARAMETER | DESCRIPTION |
|---|---|
computation
|
The name of the computation run.
TYPE:
|
value
|
The validated host result.
TYPE:
|
result_type
|
The computation's result type under its specialization.
TYPE:
|
runtime
|
The label of the runtime configuration used.
TYPE:
|
trace
|
Every event the invocation emitted, in order.
TYPE:
|
to_data
¶
Render the result as JSON-compatible data.
| RETURNS | DESCRIPTION |
|---|---|
dict[str, object]
|
|
Source code in src/quivers/qiec/execution.py
ExecutionTraceEvent
dataclass
¶
ExecutionTraceEvent(sequence: int, event: str, computation: str, detail: Mapping[str, object] = dict())
One stable event emitted by a named QIEC invocation.
| PARAMETER | DESCRIPTION |
|---|---|
sequence
|
The event's position in the invocation's trace, from zero.
TYPE:
|
event
|
The stable event name, such as
TYPE:
|
computation
|
The name of the computation being run.
TYPE:
|
detail
|
JSON-compatible event data; frozen on construction.
TYPE:
|
__post_init__
¶
to_data
¶
Render the event as JSON-compatible data.
| RETURNS | DESCRIPTION |
|---|---|
dict[str, object]
|
The sequence number, event name, computation name, and detail mapping, with every detail value made JSON-compatible. |
Source code in src/quivers/qiec/execution.py
ExecutionTraceRecorder
dataclass
¶
ExecutionTraceRecorder(events: list[ExecutionTraceEvent] = list())
Collect events while also satisfying the :class:TraceObserver API.
| PARAMETER | DESCRIPTION |
|---|---|
events
|
The recorded events, in order; empty to start.
TYPE:
|
__call__
¶
__call__(event: ExecutionTraceEvent) -> None
Record one event.
| PARAMETER | DESCRIPTION |
|---|---|
event
|
The event the invocation just emitted.
TYPE:
|
RuntimeConfiguration
dataclass
¶
RuntimeConfiguration(selections: tuple[RuntimeSelection, ...] = (RuntimeSelection('core'),), providers: tuple[RuntimeProvider, ...] = ())
Complete, explicit runtime selection for one or more invocations.
| PARAMETER | DESCRIPTION |
|---|---|
selections
|
Providers to build by name for every invocation; the core provider alone by default.
TYPE:
|
providers
|
Already-built provider objects, appended after the selections when used from Python.
TYPE:
|
label
property
¶
A +-joined label naming every selected and supplied provider.
| RETURNS | DESCRIPTION |
|---|---|
str
|
The provider names in order, or |
instantiate
¶
instantiate() -> tuple[RuntimeProvider, ...]
Build every named provider and append the programmatic ones.
| RETURNS | DESCRIPTION |
|---|---|
tuple[RuntimeProvider, ...]
|
The providers in selection order, followed by |
| RAISES | DESCRIPTION |
|---|---|
ExecutionFailure
|
With code |
Source code in src/quivers/qiec/execution.py
to_data
¶
Render the configuration as JSON-compatible data.
| RETURNS | DESCRIPTION |
|---|---|
dict[str, object]
|
The named selections with their options, and the names of any programmatic providers. |
Source code in src/quivers/qiec/execution.py
RuntimeProvider
¶
Bases: Protocol
An explicit source of process-local handlers and type validators.
attach
¶
attach(module: QiecModule, attachments: RuntimeAttachments) -> None
Bind this provider's handlers into a fresh attachment table.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The validated module whose handlers and effects are being served.
TYPE:
|
attachments
|
The per-invocation table receiving runtime handlers.
TYPE:
|
Source code in src/quivers/qiec/execution.py
validator_for
¶
validator_for(type_: TypeExpr) -> RuntimeValidator | None
Supply a host validator for a runtime type, if this provider has one.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
The closed QIEC type an argument or result must inhabit.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeValidator | None
|
A predicate over host values, or |
Source code in src/quivers/qiec/execution.py
RuntimeSelection
dataclass
¶
One named provider and its JSON-compatible construction options.
| PARAMETER | DESCRIPTION |
|---|---|
provider
|
The registered or entry-point name of the provider; must be non-empty.
TYPE:
|
options
|
The options passed to the provider's factory; frozen on construction.
TYPE:
|
__post_init__
¶
Reject empty provider names and freeze the options.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If |
Source code in src/quivers/qiec/execution.py
DistributionFamily
dataclass
¶
DistributionFamily(name: str, parameters: tuple[FamilyParameter, ...], support: SupportKind, element: TypeExpr, event_rank: int, event_source: str | None, discrete: bool, reparameterizable: bool, compositional: bool, targets: Mapping[str, str] = dict(), finite_support: tuple[object, ...] | None = None, relaxes: tuple[str, tuple[object, ...]] | None = None)
The semantic record of one distribution family.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The family's source name, such as
TYPE:
|
parameters
|
The parameters, in the order a positional application supplies
them. Alternative parameterizations, such as
TYPE:
|
support
|
Where samples live.
TYPE:
|
element
|
The scalar type of one sample element.
TYPE:
|
event_rank
|
The rank of one sample: 0 for a scalar family, 1 for a vector family, 2 for a matrix family.
TYPE:
|
event_source
|
The parameter whose trailing
TYPE:
|
discrete
|
Whether samples are discrete.
TYPE:
|
reparameterizable
|
Whether a sample can be drawn as a differentiable function of the parameters.
TYPE:
|
compositional
|
Whether the family is built from other distributions or morphisms rather than from tensor parameters alone.
TYPE:
|
targets
|
The spelling each transpile target uses for the family.
TYPE:
|
finite_support
|
The finite set of values a sample ranges over, when the family has one independent of its parameters.
TYPE:
|
relaxes
|
The discrete family a continuous relaxation stands in for, and the atoms of that family's support as the relaxation's samples spell them: a marginalization over the relaxation enumerates those atoms under the discrete family's masses, as the torch runtime does.
TYPE:
|
id
property
¶
id: DistributionId
The family's stable identity.
| RETURNS | DESCRIPTION |
|---|---|
DistributionId
|
An identity derived from the |
parameter_names
property
¶
The parameter names in positional order.
| RETURNS | DESCRIPTION |
|---|---|
tuple[str, ...]
|
The names. |
__post_init__
¶
Freeze the target spellings and check the parameter names.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If two parameters share a name, or |
Source code in src/quivers/qiec/families.py
parameter
¶
parameter(name: str) -> FamilyParameter
Look up a parameter by name.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The parameter's name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
FamilyParameter
|
The parameter. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If the family has no such parameter. |
Source code in src/quivers/qiec/families.py
FamilyParameter
dataclass
¶
FamilyParameter(name: str, constraint: ParameterConstraint, rank: int)
One parameter of a distribution family.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The parameter's name, as the source spells it by keyword.
TYPE:
|
constraint
|
The symbolic constraint on admissible values.
TYPE:
|
rank
|
The tensor rank of one parameter value: 0 for a scalar, 1 for a vector, 2 for a matrix.
TYPE:
|
AttachmentId
dataclass
¶
ComputationId
dataclass
¶
ConstructorId
dataclass
¶
DistributionId
dataclass
¶
DynamicAddressFrame
dataclass
¶
One serializable component of a dynamic effect address.
| PARAMETER | DESCRIPTION |
|---|---|
scope
|
What kind of frame this is, such as a call, a handler clause, a resumption, or a local instance.
TYPE:
|
key
|
The frame's position within its scope: a name or an ordinal.
TYPE:
|
EffectInstanceId
dataclass
¶
EqualityId
dataclass
¶
FamilyId
dataclass
¶
OperationId
dataclass
¶
PrimitiveId
dataclass
¶
RowVariableId
dataclass
¶
SiteProvenance
dataclass
¶
SiteProvenance(origin: SourceOrigin, dynamic_path: tuple[DynamicAddressFrame, ...] = (), resumption_path: tuple[int, ...] = (), relation: AddressRelation = 'preserve', parents: tuple[SiteId, ...] = ())
Static and dynamic provenance of an effect request.
| PARAMETER | DESCRIPTION |
|---|---|
origin
|
The source site the request was written at.
TYPE:
|
dynamic_path
|
The address frames entered to reach this occurrence of the site, outermost first.
TYPE:
|
resumption_path
|
The ordinal of each resumption taken to reach this occurrence, so a site reached twice under a multi-shot handler yields two keys.
TYPE:
|
relation
|
How this request relates to the source site:
TYPE:
|
parents
|
The static sites a derived request was generated from.
TYPE:
|
static_site
property
¶
static_site: SiteId
The source site this request was written at.
| RETURNS | DESCRIPTION |
|---|---|
SiteId
|
The static identity, shared by every dynamic occurrence of the request. |
dynamic_key
¶
A hashable key distinguishing occurrences of one static site.
| RETURNS | DESCRIPTION |
|---|---|
tuple[str, tuple[tuple[str, str | int], ...], tuple[int, ...]]
|
The static site, the dynamic address frames, and the resumption path. One site reached twice, under a loop or under a resumed continuation, yields two keys, which is what lets a trace name each occurrence separately. |
Source code in src/quivers/qiec/identifiers.py
to_data
¶
Return the serializable form of this provenance.
| RETURNS | DESCRIPTION |
|---|---|
dict[str, object]
|
The origin, the static site, and the dynamic address. The static site is written out alongside the origin it derives from so a reader need not re-derive it. |
Source code in src/quivers/qiec/identifiers.py
SourceOrigin
dataclass
¶
SourceOrigin(module: str, structural_path: tuple[str | int, ...], role: str, source_protocol: str, file: str | None = None, line: int | None = None, column: int | None = None)
Stable structural source origin with optional diagnostic coordinates.
structural_path is the protocol path after parsing and name
resolution. Line and column are diagnostic metadata and therefore do not
participate in :meth:site_id.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module the site belongs to.
TYPE:
|
structural_path
|
The path of names and positions from the module root to the site.
TYPE:
|
role
|
What the site is, such as
TYPE:
|
source_protocol
|
The source language or protocol the path is expressed in.
TYPE:
|
file
|
The file the site was read from, if any.
TYPE:
|
line
|
The one-based line of the site, if known.
TYPE:
|
column
|
The one-based column of the site, if known.
TYPE:
|
site_id
¶
site_id() -> SiteId
The stable identity of the source site this origin describes.
| RETURNS | DESCRIPTION |
|---|---|
SiteId
|
An identity derived from the protocol, module, structural path, and role. The file, line, and column are deliberately excluded, so reformatting a source file does not change the identity of the sites within it. |
Source code in src/quivers/qiec/identifiers.py
to_data
¶
Return the serializable form of this origin.
| RETURNS | DESCRIPTION |
|---|---|
dict[str, object]
|
Every field, including the diagnostic coordinates. Those do
not enter |
Source code in src/quivers/qiec/identifiers.py
StableId
dataclass
¶
A namespaced, SHA-256-derived kernel identifier.
The human-readable declaration name is intentionally not stored in the
identifier. Renaming display labels must not silently alter equality;
callers choose the declaration path supplied to :meth:derive and record
renames explicitly in a migration map.
| PARAMETER | DESCRIPTION |
|---|---|
digest
|
The 64-character lowercase hex SHA-256 digest; usually produced by
:meth:
TYPE:
|
__post_init__
¶
Reject a digest that is not 64 lowercase hex characters.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the digest is the wrong length or contains a character
outside |
Source code in src/quivers/qiec/identifiers.py
derive
classmethod
¶
Derive an identifier from the values that determine it.
| PARAMETER | DESCRIPTION |
|---|---|
parts
|
The determining values, in order. Order matters, so two identifiers built from the same values differently arranged are distinct.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Self
|
The derived identifier. The ABI version and the namespace are mixed in, so an identifier from one namespace can never equal one from another, and a future ABI change re-derives rather than silently reusing. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If a part has no canonical encoding. |
Source code in src/quivers/qiec/identifiers.py
parse
classmethod
¶
Read an identifier back from its wire form.
| PARAMETER | DESCRIPTION |
|---|---|
text
|
The wire form,
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Self
|
The parsed identifier. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the text carries another namespace's prefix, or the remainder is not a valid digest. Parsing is namespace-checked so a handler identifier cannot be read as an effect one. |
Source code in src/quivers/qiec/identifiers.py
__str__
¶
The wire form of this identifier.
| RETURNS | DESCRIPTION |
|---|---|
str
|
|
to_data
¶
Return the stable wire representation.
| RETURNS | DESCRIPTION |
|---|---|
str
|
The same string as |
StaticScopeId
dataclass
¶
StaticVariableId
dataclass
¶
ArrowKind
dataclass
¶
ContextSort
dataclass
¶
A logic-program context indexed by a stable signature name.
| PARAMETER | DESCRIPTION |
|---|---|
signature
|
The name of the signature whose contexts inhabit this sort.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
EffectBinder
dataclass
¶
A telescope binder for an effect argument.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The binder's display name.
TYPE:
|
refinable
|
Whether case analysis may refine the bound argument.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
EffectKind
dataclass
¶
The kind of effect interfaces.
| PARAMETER | DESCRIPTION |
|---|---|
tag
|
The serialization discriminator; always
TYPE:
|
IndexBinder
dataclass
¶
IndexBinder(name: str, sort: IndexSort, refinable: bool = False, tag: Literal['index'] = 'index')
A telescope binder for an index argument.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The binder's display name.
TYPE:
|
sort
|
The closed index sort of the bound argument.
TYPE:
|
refinable
|
Whether case analysis may refine the bound argument; true for a family's indices and false for its uniform parameters.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
NatSort
dataclass
¶
The sort of natural-number indices.
| PARAMETER | DESCRIPTION |
|---|---|
tag
|
The serialization discriminator; always
TYPE:
|
RowKind
dataclass
¶
The kind of effect rows.
| PARAMETER | DESCRIPTION |
|---|---|
tag
|
The serialization discriminator; always
TYPE:
|
ShapeSort
dataclass
¶
The sort of shapes, optionally restricted to a fixed rank.
| PARAMETER | DESCRIPTION |
|---|---|
rank
|
The number of dimensions, or None for any rank. A binder of unspecified rank accepts a shape of any rank, which is what makes a rank-polymorphic signature expressible.
TYPE:
|
tag
|
Discriminator for the index-sort union.
TYPE:
|
__post_init__
¶
Reject a negative rank.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If |
TypeBinder
dataclass
¶
A telescope binder for a type or effect-kinded static argument.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The binder's display name.
TYPE:
|
kind
|
The kind of the bound argument. |
refinable
|
Whether case analysis may refine the bound argument; true for a family's indices and false for its uniform parameters.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
TypeKind
dataclass
¶
The kind of types.
| PARAMETER | DESCRIPTION |
|---|---|
tag
|
The serialization discriminator; always
TYPE:
|
UserIndexSort
dataclass
¶
UserIndexSort(name: str, constructors: tuple[str, ...], arities: tuple[int, ...] = (), tag: Literal['user'] = 'user')
A closed user-defined index datatype.
Constructor names are part of the sort identity. Open index sorts are deliberately absent from the first kernel because they make coverage unstable under separate compilation.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The sort's name, part of its identity.
TYPE:
|
constructors
|
Constructor names, unique and part of the identity. Two sorts with the same name and different constructors are different sorts, which is what keeps coverage decidable.
TYPE:
|
arities
|
Argument count per constructor, positionally aligned with
TYPE:
|
tag
|
Discriminator for the index-sort union.
TYPE:
|
__post_init__
¶
Default the arities and reject a malformed sort.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the name is empty, there are no constructors, a constructor name repeats, the arities do not align with the constructors, or an arity is negative. |
Source code in src/quivers/qiec/kinds.py
constructor_arity
¶
The number of arguments one constructor takes.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The constructor name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
int
|
Its arity, zero for a nullary constructor. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the sort has no such constructor. The sort is closed, so an unknown name is an error rather than an open extension. |
Source code in src/quivers/qiec/kinds.py
NamedComputation
dataclass
¶
NamedComputation(id: ComputationId, name: str, telescope: Telescope, parameters: tuple[Local, ...], body: Computation, type: ComputationType, origin: SourceOrigin)
One named QVR computation and its checked QIEC type.
| PARAMETER | DESCRIPTION |
|---|---|
id
|
The computation's stable identity, which calls refer to.
TYPE:
|
name
|
The display name; must be non-empty and unique within the module.
TYPE:
|
telescope
|
The static parameters the computation abstracts over, in order.
TYPE:
|
parameters
|
The value parameters, in order; their names must be distinct and must not reuse a telescope binder's name.
TYPE:
|
body
|
The computation's body, with the parameters in scope.
TYPE:
|
type
|
The checked effect row and result type of
TYPE:
|
origin
|
Where the computation was declared.
TYPE:
|
__post_init__
¶
Reject a computation whose names collide or are absent.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the name is empty, the telescope is malformed, two parameters share a name, or a parameter shadows a static binder. Shadowing is rejected so a name inside the body denotes one thing. |
Source code in src/quivers/qiec/module.py
NamedEffectInstance
dataclass
¶
NamedEffectInstance(name: str, entry: RowEntry, origin: SourceOrigin)
A source name for one deterministically allocated lexical instance.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The name requests resolve through; must be non-empty.
TYPE:
|
entry
|
The allocated instance and its interface application.
TYPE:
|
origin
|
Where the instance was declared.
TYPE:
|
__post_init__
¶
Reject an unnamed instance.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the source name is empty. The name is how a request resolves to this instance, so an empty one names nothing. |
Source code in src/quivers/qiec/module.py
QiecModule
dataclass
¶
QiecModule(module: str, source_protocol: str, index_sorts: tuple[UserIndexSort, ...] = (), families: tuple[FamilyDecl, ...] = (), constructors: tuple[ConstructorDecl, ...] = (), effects: tuple[EffectDef, ...] = (), instances: tuple[NamedEffectInstance, ...] = (), handlers: tuple[HandlerDef, ...] = (), computations: tuple[NamedComputation, ...] = (), entries: tuple[ProgramEntry, ...] = (), gap: str = '', abi: str = QIEC_ABI)
A complete, serializable QIEC compilation unit.
source_protocol records the exact source route that produced the
module. The wire envelope separately records :data:QIEC_ABI, so neither
endpoint can be guessed during deserialization or compiler integration.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module's name, from which every stable identity in it derives.
TYPE:
|
source_protocol
|
The source route that produced the module.
TYPE:
|
index_sorts
|
The user-defined closed index sorts.
TYPE:
|
families
|
The indexed data families.
TYPE:
|
constructors
|
The family constructors.
TYPE:
|
effects
|
The effect interfaces.
TYPE:
|
instances
|
The module-scoped named effect instances.
TYPE:
|
handlers
|
The handler declarations.
TYPE:
|
computations
|
The named computations.
TYPE:
|
entries
|
The program entry points, each naming one of the computations.
TYPE:
|
gap
|
The diagnostic of a program the module lowered without, because it uses a construct whose elaboration is not yet defined; empty when every program elaborated.
TYPE:
|
abi
|
The kernel ABI the module is expressed against; must equal
:data:
TYPE:
|
__post_init__
¶
Reject a module whose identity or ABI is missing or wrong.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the module name or source protocol is empty, or the ABI is not the one this kernel speaks. The ABI is checked here as well as at the wire envelope so a module built in process cannot claim a version it was not built for. |
Source code in src/quivers/qiec/module.py
206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 | |
PrimitiveSignature
dataclass
¶
PrimitiveSignature(name: str, parameters: tuple[TypeExpr, ...], result: TypeExpr, capability: PrimitiveCapability)
One primitive's name, types, and the capability a backend needs for it.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The stable nominal name, such as
TYPE:
|
parameters
|
The argument types, in order.
TYPE:
|
result
|
The result type.
TYPE:
|
capability
|
The feature a target must support to render the primitive.
TYPE:
|
id
property
¶
id: PrimitiveId
The primitive's stable identity.
| RETURNS | DESCRIPTION |
|---|---|
PrimitiveId
|
An identity derived from the |
DeductionRun
dataclass
¶
DeductionRun(weight: object, result: ExecutionResult)
The outcome of running a deduction on the reference machine.
| PARAMETER | DESCRIPTION |
|---|---|
weight
|
The inside weight of the goal in the deduction's semiring: a log weight, a Boolean, or a count.
TYPE:
|
result
|
The machine's full result, with its trace.
TYPE:
|
ProgramRun
dataclass
¶
ProgramRun(value: object, log_joint: float, result: ExecutionResult)
What running a program on the reference machine produced.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The value the program returned.
TYPE:
|
log_joint
|
The log joint density: every replayed site's log density under its distribution plus every observation's and score's weight.
TYPE:
|
result
|
The underlying execution result, with its trace.
TYPE:
|
ProgramEntry
dataclass
¶
ProgramEntry(name: str, computation: ComputationId, parameters: tuple[ProgramParameter, ...], return_names: tuple[str, ...], return_labels: tuple[str, ...] | None, sites: tuple[ProgramSite, ...], random_instance: EffectInstanceId, score_instance: EffectInstanceId, telescope: Telescope = (), tag: Literal['program_entry'] = 'program_entry')
The typed entry point a program declaration elaborates to.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The program's source name.
TYPE:
|
computation
|
The identity of the named computation holding its body.
TYPE:
|
parameters
|
The computation's parameters with their roles, in order.
TYPE:
|
return_names
|
The names the program returns, in order.
TYPE:
|
return_labels
|
The labels of a labelled return tuple, or
TYPE:
|
sites
|
The program's probabilistic steps, in source order, those of marginalization scopes included.
TYPE:
|
random_instance
|
The lexical
TYPE:
|
score_instance
|
The lexical
TYPE:
|
telescope
|
The static binders the computation takes: one index binder per extent of an input the program's steps leave open, which a run reads off the data it is given.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
ProgramParameter
dataclass
¶
ProgramParameter(name: str, role: ParameterRole, type: TypeExpr, axes: tuple[str, ...] = (), tag: Literal['program_parameter'] = 'program_parameter')
One parameter of an elaborated program.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The parameter's name, which is the computation parameter's.
TYPE:
|
role
|
How the parameter is supplied.
TYPE:
|
type
|
Its type.
TYPE:
|
axes
|
The name of each dimension of a tensor-typed parameter, the object or extent it ranges over; empty for a scalar.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
ProgramSite
dataclass
¶
ProgramSite(name: str, kind: SiteKind, family: str, batch: tuple[PlateAxis, ...] = (), event: tuple[PlateAxis, ...] = (), tag: Literal['program_site'] = 'program_site')
One probabilistic step of an elaborated program.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The site's label, the name the step binds or scores.
TYPE:
|
kind
|
Whether the step samples, observes, or marginalizes.
TYPE:
|
family
|
The distribution family the step draws from.
TYPE:
|
batch
|
The plate's batch axes.
TYPE:
|
event
|
The plate's event axes.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
DistributionError
¶
Bases: ValueError
A distribution could not be constructed, sampled, or scored.
SerializationError
¶
Bases: ValueError
A value is not in the stable QIEC wire language.
StaticSubstitution
dataclass
¶
StaticSubstitution(types: tuple[tuple[str, TypeExpr], ...] = (), indices: tuple[tuple[str, IndexTerm], ...] = (), effects: tuple[tuple[str, EffectRef | EffectVariable], ...] = ())
A deterministic substitution split by static namespace.
| PARAMETER | DESCRIPTION |
|---|---|
types
|
Bindings from type-variable names to types.
TYPE:
|
indices
|
Bindings from index-variable names to index terms.
TYPE:
|
effects
|
Bindings from effect-variable names to interface applications or other effect variables.
TYPE:
|
__post_init__
¶
Reject a substitution that binds one name twice.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If a name repeats within a namespace. Two bindings for one name would make the result depend on lookup order. |
Source code in src/quivers/qiec/substitution.py
type
¶
type(name: str) -> TypeExpr | None
What a type binder of this name is bound to.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The binder name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeExpr or None
|
The bound type, or None when this substitution says nothing about the name, in which case the variable stands. |
Source code in src/quivers/qiec/substitution.py
index
¶
index(name: str) -> IndexTerm | None
What an index binder of this name is bound to.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The binder name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
IndexTerm or None
|
The bound index, or None when the name is unbound here. |
Source code in src/quivers/qiec/substitution.py
effect
¶
effect(name: str) -> EffectRef | EffectVariable | None
What an effect binder of this name is bound to.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The binder name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRef or EffectVariable or None
|
The bound interface application or effect variable, or None when the name is unbound here. |
Source code in src/quivers/qiec/substitution.py
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
TYPE:
|
bias
|
A
TYPE:
|
sources
|
The conditioning row's factors in order, each a
TYPE:
|
row_offset
|
The first row of the head's block.
TYPE:
|
rows
|
The block's height.
TYPE:
|
transform
|
TYPE:
|
result_type
|
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
type
|
The type the bound value must inhabit.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
first
|
The computation run first.
TYPE:
|
then
|
The computation run second, with
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
name
|
The callee's display name, for diagnostics and traces.
TYPE:
|
static_arguments
|
The callee's telescope instantiation, in binder order.
TYPE:
|
arguments
|
The value arguments, one per callee parameter.
TYPE:
|
result_type
|
The callee's result type under the instantiation.
TYPE:
|
effects
|
The callee's effect row under the instantiation.
TYPE:
|
origin
|
The call site's source location.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
motive
|
The result family, over the scrutinee's indices.
TYPE:
|
branches
|
One branch per constructor considered; coverage is checked against the exact applied family.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
static_arguments
|
The constructor's static arguments as bound by the pattern, in binder order.
TYPE:
|
fields
|
The locals binding the constructor's fields, in declaration order.
TYPE:
|
body
|
The computation run when the branch is selected.
TYPE:
|
scope
|
The static scope identity under which the branch's skolems and equality evidence are minted.
TYPE:
|
CaseMotive
dataclass
¶
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
TYPE:
|
extent
|
The axis's extent, an index term of the nat sort.
TYPE:
|
body
|
The entry at each index.
TYPE:
|
result_type
|
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
static_arguments
|
The constructor's telescope instantiation, in binder order.
TYPE:
|
fields
|
The field values, in declaration order.
TYPE:
|
result_type
|
The indexed family type the application inhabits.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
name
|
The family's source name, as the registry spells it.
TYPE:
|
arguments
|
The parameters supplied, each named, in source order.
TYPE:
|
result_type
|
The
TYPE:
|
origin
|
The construction's source location.
TYPE:
|
plate
|
The plate the distribution is constructed over; empty for one draw of the family.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
EvidenceValue
dataclass
¶
EvidenceValue(evidence: EqualityEvidence, tag: Literal['evidence'] = 'evidence')
Kernel-checked equality evidence used as a value.
| PARAMETER | DESCRIPTION |
|---|---|
evidence
|
The evidence term.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
Gather
dataclass
¶
Selection along the outermost axis of a tensor.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The tensor selected from.
TYPE:
|
index
|
An
TYPE:
|
result_type
|
The selection's type: the slice type for an integer index, or a tensor of slices shaped like the index tensor.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
handler
|
The stable identity of the handler installed.
TYPE:
|
computation
|
The handled computation.
TYPE:
|
static_arguments
|
The handler's telescope instantiation, in binder order.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
then
|
The computation run when the condition holds.
TYPE:
|
otherwise
|
The computation run when it does not.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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
TYPE:
|
kernel
|
The kernel's name;
TYPE:
|
length_scale
|
The kernel's length scale.
TYPE:
|
jitter
|
The diagonal added for numerical positive definiteness.
TYPE:
|
result_type
|
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
TYPE:
|
type
|
The literal's type.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
type
|
The type of every value bound to it.
TYPE:
|
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
TYPE:
|
value
|
The point evaluated, of type
TYPE:
|
origin
|
The evaluation's source location.
TYPE:
|
batch
|
The batch axes the density is kept apart over: empty for one
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
effect
|
The applied interface the instance provides.
TYPE:
|
body
|
The computation within which the instance is in scope.
TYPE:
|
origin
|
The allocation's source location.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
size
|
The axis's extent, an index term of the nat sort.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
event
|
The joint axes, outermost first.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
empty
property
¶
Whether the plate has no axes at all.
| RETURNS | DESCRIPTION |
|---|---|
bool
|
|
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:
|
name
|
The primitive's nominal name, as the registry spells it.
TYPE:
|
arguments
|
The value arguments, one per parameter.
TYPE:
|
result_type
|
The primitive's result type.
TYPE:
|
origin
|
The application's source location.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
position
|
The zero-based component selected.
TYPE:
|
result_type
|
The selected component's type.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
value
|
A tensor of reals, or of integers for
TYPE:
|
result_type
|
The element type.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
origin
|
The resumption's source location.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
Return
dataclass
¶
Return(value: Value, tag: Literal['return'] = 'return')
Return a value with no effects.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The value produced.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
value
|
A tensor of reals.
TYPE:
|
result_type
|
The tensor's own type.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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
TYPE:
|
index
|
A
TYPE:
|
groups
|
The number of groups, an index term of the nat sort.
TYPE:
|
result_type
|
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
result_type
|
The
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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
TYPE:
|
index
|
An
TYPE:
|
row_offset
|
The first column of the head's block.
TYPE:
|
rows
|
The block's width.
TYPE:
|
transform
|
TYPE:
|
result_type
|
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
TensorValue
dataclass
¶
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:
|
result_type
|
The
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
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:
|
value
|
The value at the equality's left type.
TYPE:
|
target_type
|
The type the transported value inhabits, which the equality's right side determines.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
TupleValue
dataclass
¶
Var
dataclass
¶
Var(local: Local, tag: Literal['var'] = 'var')
Reference to a bound local.
| PARAMETER | DESCRIPTION |
|---|---|
local
|
The binder being referenced.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
WeightSum
dataclass
¶
WeightSum(value: Value, tag: Literal['weight_sum'] = 'weight_sum')
The total of a tensor of log weights.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
A
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
EffectRef
dataclass
¶
EffectRef(id: EffectId, name: str, arguments: tuple[StaticArgument, ...] = (), tag: Literal['effect_ref'] = 'effect_ref')
One closed effect interface application.
| PARAMETER | DESCRIPTION |
|---|---|
id
|
The stable identity of the interface declaration.
TYPE:
|
name
|
The interface's display name.
TYPE:
|
arguments
|
The arguments instantiating the interface's telescope, in order.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
__eq__
¶
Compare a concrete interface application by stable identity.
| PARAMETER | DESCRIPTION |
|---|---|
other
|
The value to compare against.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
bool
|
True when both name the same declaration and supply equal static arguments. The display name is ignored, and identity is nominal, so two applications of one interface differ only by their arguments. |
Source code in src/quivers/qiec/types.py
__hash__
¶
Hash the fields __eq__ compares.
| RETURNS | DESCRIPTION |
|---|---|
int
|
A hash of the declaration identity and the arguments. |
EffectVariable
dataclass
¶
EffectVariable(name: str, identity: StaticVariableId | None = None, tag: Literal['effect_variable'] = 'effect_variable')
A variable standing for an effect interface application.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The variable's display name.
TYPE:
|
identity
|
The rigid identity of a case branch's skolem, or
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
__eq__
¶
Compare by identity when either side is rigid, else by name.
| PARAMETER | DESCRIPTION |
|---|---|
other
|
The value to compare against.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
bool
|
True when both denote the same effect variable. A rigid variable never equals a free one, which is what keeps a branch's skolem from unifying with an enclosing binder. |
Source code in src/quivers/qiec/types.py
__hash__
¶
Hash the fields __eq__ compares.
| RETURNS | DESCRIPTION |
|---|---|
int
|
A hash of the identity when the variable is rigid, and of the name otherwise. |
Source code in src/quivers/qiec/types.py
EqualityType
dataclass
¶
EqualityType(kind: Kind | IndexSort, left: StaticArgument, right: StaticArgument, tag: Literal['equality_type'] = 'equality_type')
The proposition that two static arguments are equal.
| PARAMETER | DESCRIPTION |
|---|---|
kind
|
The kind or index sort both sides inhabit. |
left
|
The left side of the equation.
TYPE:
|
right
|
The right side of the equation.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
FunctionType
dataclass
¶
FunctionType(parameter: TypeExpr, result: TypeExpr, tag: Literal['function_type'] = 'function_type')
A pure function type.
Effectful codomains are represented explicitly by
:class:quivers.qiec.effects.ComputationType, keeping the value and
computation strata separate.
| PARAMETER | DESCRIPTION |
|---|---|
parameter
|
The argument type.
TYPE:
|
result
|
The result type.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
IndexConstructor
dataclass
¶
IndexConstructor(name: str, arguments: tuple[IndexTerm, ...], sort: IndexSort, tag: Literal['index_constructor'] = 'index_constructor')
A fully applied constructor of a user-defined index sort.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The constructor's name, which must belong to
TYPE:
|
arguments
|
The constructor's index arguments, in order.
TYPE:
|
sort
|
The sort the constructor builds.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
__post_init__
¶
Check the constructor belongs to its sort and is fully applied.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the sort is not a user-defined one, if it declares no such constructor, or if the argument count differs from the declared arity. A partially applied index constructor is rejected rather than curried, since an index is a value of its sort and a partial application is not one. |
Source code in src/quivers/qiec/types.py
IndexLiteral
dataclass
¶
IndexLiteral(value: int | str, sort: IndexSort, tag: Literal['index_literal'] = 'index_literal')
A closed index literal.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
A natural number for the nat sort, or a nullary constructor name for a user-defined index sort.
TYPE:
|
sort
|
The sort the literal inhabits.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
__post_init__
¶
Check the literal inhabits the sort it claims.
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If a |
Source code in src/quivers/qiec/types.py
IndexVariable
dataclass
¶
IndexVariable(name: str, sort: IndexSort, identity: StaticVariableId | None = None, tag: Literal['index_variable'] = 'index_variable')
A variable standing for an index term.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The variable's display name.
TYPE:
|
sort
|
The closed index sort of the terms it stands for.
TYPE:
|
identity
|
The rigid identity of a case branch's skolem, or
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
__eq__
¶
Compare by identity when either side is rigid, else by name.
A variable carrying a StaticVariableId is rigid: a case branch's
skolem, distinct from every other even where the names agree. One
without is a declaration binder, which two occurrences share by
name. Comparing a rigid variable to a free one is therefore
false, which is what stops a branch's skolem from unifying with
an enclosing binder.
| PARAMETER | DESCRIPTION |
|---|---|
other
|
The value to compare against.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
bool
|
True when both denote the same variable at the same sort. |
Source code in src/quivers/qiec/types.py
__hash__
¶
Hash the fields __eq__ compares.
| RETURNS | DESCRIPTION |
|---|---|
int
|
A hash of the sort with the identity when rigid, and with the name otherwise, so equal variables hash alike. |
Source code in src/quivers/qiec/types.py
ShapeIndex
dataclass
¶
ShapeIndex(dimensions: tuple[IndexTerm, ...], tag: Literal['shape_index'] = 'shape_index')
A shape given by its dimensions.
| PARAMETER | DESCRIPTION |
|---|---|
dimensions
|
One index term per dimension, outermost first.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
TypeApplication
dataclass
¶
TypeApplication(constructor: TypeConstructorRef, arguments: tuple[StaticArgument, ...] = (), tag: Literal['type_application'] = 'type_application')
A type constructor applied to static arguments.
| PARAMETER | DESCRIPTION |
|---|---|
constructor
|
The constructor applied.
TYPE:
|
arguments
|
The arguments instantiating the constructor's telescope, in order; empty for a nullary constructor.
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
TypeConstructorRef
dataclass
¶
A fully qualified type constructor and its kinding telescope.
| PARAMETER | DESCRIPTION |
|---|---|
id
|
The constructor's stable identity, which alone determines equality.
TYPE:
|
name
|
The constructor's display name.
TYPE:
|
telescope
|
The binders the constructor's arguments instantiate, in order.
TYPE:
|
builtin
classmethod
¶
builtin(name: str) -> TypeConstructorRef
A constructor for one of the language's own types.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The builtin's name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeConstructorRef
|
A nullary constructor whose identity derives from the
|
Source code in src/quivers/qiec/types.py
__eq__
¶
Compare semantic identity, excluding diagnostic presentation data.
| PARAMETER | DESCRIPTION |
|---|---|
other
|
The value to compare against.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
bool
|
True when both name the same declaration. The display name and the telescope are presentation, so a constructor read back under a different spelling is still the same type. |
Source code in src/quivers/qiec/types.py
__hash__
¶
Hash the identity __eq__ compares.
| RETURNS | DESCRIPTION |
|---|---|
int
|
A hash of the declaration identity alone. |
TypeVariable
dataclass
¶
TypeVariable(name: str, kind: Kind = TYPE, identity: StaticVariableId | None = None, tag: Literal['type_variable'] = 'type_variable')
A variable standing for a type or effect-kinded static argument.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The variable's display name.
TYPE:
|
kind
|
The kind of the arguments it stands for. |
identity
|
The rigid identity of a case branch's skolem, or
TYPE:
|
tag
|
The serialization discriminator; always
TYPE:
|
__eq__
¶
Compare by identity when either side is rigid, else by name.
A variable carrying a StaticVariableId is rigid: a case branch's
skolem, distinct from every other even where the names agree. One
without is a declaration binder, which two occurrences share by
name. Comparing a rigid variable to a free one is therefore
false, which is what stops a branch's skolem from unifying with
an enclosing binder.
| PARAMETER | DESCRIPTION |
|---|---|
other
|
The value to compare against.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
bool
|
True when both denote the same variable at the same kind. |
Source code in src/quivers/qiec/types.py
__hash__
¶
Hash the fields __eq__ compares.
| RETURNS | DESCRIPTION |
|---|---|
int
|
A hash of the kind with the identity when rigid, and with the name otherwise, so equal variables hash alike. |
Source code in src/quivers/qiec/types.py
StructuralRuntimeProvider
dataclass
¶
StructuralRuntimeProvider(runtimes: tuple[RuntimeHandler, ...], term_types: frozenset[TypeId], name: str = 'structural')
Bases: RuntimeProvider
PyTorch components and validators for one structural invocation.
| PARAMETER | DESCRIPTION |
|---|---|
runtimes
|
The host handlers implementing the module's structural computations.
TYPE:
|
term_types
|
Type identities whose host values are structural :class:
TYPE:
|
name
|
The provider name recorded in execution results and traces.
TYPE:
|
attach
¶
attach(module: QiecModule, attachments: RuntimeAttachments) -> None
Attach each host computation handler.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The checked module, unused because the handlers were selected while constructing this provider.
TYPE:
|
attachments
|
The invocation's attachment table.
TYPE:
|
Source code in src/quivers/qiec/structural_runtime.py
validator_for
¶
validator_for(type_: TypeExpr) -> RuntimeValidator | None
Return the validator for structural terms and torch values.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
The closed QIEC type a host argument or result must inhabit.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeValidator | None
|
A predicate for scalar weights, structural terms, tensors, and
structural products, or |
Source code in src/quivers/qiec/structural_runtime.py
abort_effect
¶
Construct the concrete Abort[error_type] interface.
| PARAMETER | DESCRIPTION |
|---|---|
error_type
|
The type to instantiate the interface's binder at.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRef
|
The saturated application. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the argument is not a type. |
ValueError
|
If it is ill-kinded. |
Source code in src/quivers/qiec/builtins.py
abort_handler
¶
abort_handler(*, on_abort: Callable[[object], object] = Aborted, result_validator: RuntimeValidator = lambda _value: True, error_type: TypeExpr = PAYLOAD, input_type: TypeExpr = ANSWER, output_type: TypeExpr = ANSWER, output_validator: RuntimeValidator = lambda _value: True, duplicable_context: bool = False, key: str = 'abort') -> RuntimeHandler
Handle Abort.abort without resuming the discarded continuation.
| PARAMETER | DESCRIPTION |
|---|---|
on_abort
|
Receives the payload when the computation aborts and supplies
the handler's answer; wraps it in
TYPE:
|
result_validator
|
The abort operation's result validator; never exercised, since the clause does not resume.
TYPE:
|
error_type
|
The payload type an abort carries.
TYPE:
|
input_type
|
What the handled computation returns.
TYPE:
|
output_type
|
What the handler answers with.
TYPE:
|
output_validator
|
Checks the handler's answer.
TYPE:
|
duplicable_context
|
Whether the handler's own state may be copied for a multi-shot resumption. Asserted rather than inferred: copying a handler owning mutable state would let two shots share it.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
Source code in src/quivers/qiec/builtins.py
2273 2274 2275 2276 2277 2278 2279 2280 2281 2282 2283 2284 2285 2286 2287 2288 2289 2290 2291 2292 2293 2294 2295 2296 2297 2298 2299 2300 2301 2302 2303 2304 2305 2306 2307 2308 2309 2310 2311 2312 2313 2314 2315 2316 2317 2318 2319 2320 2321 2322 2323 2324 2325 2326 2327 2328 2329 2330 2331 2332 2333 2334 2335 2336 2337 2338 2339 2340 2341 2342 2343 2344 2345 2346 2347 2348 2349 2350 2351 2352 2353 2354 2355 2356 2357 2358 2359 2360 2361 2362 2363 2364 2365 2366 2367 2368 2369 | |
add_weights
¶
Add two log weights, entrywise over tensors of them.
| PARAMETER | DESCRIPTION |
|---|---|
left
|
A float, or nested tuples of floats.
TYPE:
|
right
|
A float, or nested tuples of floats shaped like
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
The entrywise sum; a scalar broadcasts over a tensor. |
| RAISES | DESCRIPTION |
|---|---|
RuntimeTypeMismatch
|
If two tensors differ in shape. |
Source code in src/quivers/qiec/builtins.py
block_handler
¶
block_handler(hidden: Callable[[object], bool], *, score_instance: EffectInstanceId, result_validator: RuntimeValidator, weight_validator: RuntimeValidator = lambda _value: True, draw: Callable[[object, object, RuntimeRequest], object] | None = None, answer_type: TypeExpr = ANSWER, key: str = 'block') -> RuntimeHandler
Answer hidden sites locally so no outer handler sees them.
A hidden site is drawn and scored here, exactly as the default scoring draw would; every other site forwards.
| PARAMETER | DESCRIPTION |
|---|---|
hidden
|
Whether a site is hidden from the handlers outside this one.
TYPE:
|
score_instance
|
The lexical
TYPE:
|
result_validator
|
Checks the value a resumption carries inhabits the operation's result type.
TYPE:
|
weight_validator
|
Checks each log-density contribution.
TYPE:
|
draw
|
Supplies the drawn value for a hidden site, given the site, the sampleable, and the request. None uses the sampleable's own sampling interface.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
Source code in src/quivers/qiec/builtins.py
3112 3113 3114 3115 3116 3117 3118 3119 3120 3121 3122 3123 3124 3125 3126 3127 3128 3129 3130 3131 3132 3133 3134 3135 3136 3137 3138 3139 3140 3141 3142 3143 3144 3145 3146 3147 3148 3149 3150 3151 3152 3153 3154 3155 3156 3157 3158 3159 3160 3161 3162 3163 3164 3165 3166 3167 3168 3169 3170 3171 3172 3173 3174 3175 3176 3177 3178 3179 3180 3181 3182 3183 3184 3185 3186 3187 3188 3189 3190 3191 3192 3193 3194 3195 3196 3197 3198 3199 3200 3201 3202 3203 3204 3205 3206 3207 3208 3209 3210 3211 3212 3213 3214 | |
choose_handler
¶
choose_handler(choice_validator: RuntimeValidator, *, combine: Callable[[list[object]], object] | None = None, combine_validator: RuntimeValidator | None = None, answer_type: TypeExpr = ANSWER, answer_validator: RuntimeValidator = lambda _value: True, key: str = 'choose') -> RuntimeHandler
Enumerate finite choices using an unrestricted deep resumption.
| PARAMETER | DESCRIPTION |
|---|---|
choice_validator
|
Checks each alternative resumed with.
TYPE:
|
combine
|
Folds the per-alternative results into the handler's answer;
TYPE:
|
combine_validator
|
Checks the combined answer; required with a custom
TYPE:
|
answer_type
|
What the handled computation returns; the handler answers with
TYPE:
|
answer_validator
|
Checks the handled computation's answer.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If |
Source code in src/quivers/qiec/builtins.py
2372 2373 2374 2375 2376 2377 2378 2379 2380 2381 2382 2383 2384 2385 2386 2387 2388 2389 2390 2391 2392 2393 2394 2395 2396 2397 2398 2399 2400 2401 2402 2403 2404 2405 2406 2407 2408 2409 2410 2411 2412 2413 2414 2415 2416 2417 2418 2419 2420 2421 2422 2423 2424 2425 2426 2427 2428 2429 2430 2431 2432 2433 2434 2435 2436 2437 2438 2439 2440 2441 2442 2443 2444 2445 2446 2447 2448 2449 2450 2451 2452 2453 2454 2455 2456 2457 2458 2459 2460 2461 2462 2463 2464 2465 2466 2467 2468 2469 2470 2471 2472 2473 2474 2475 2476 2477 2478 2479 2480 2481 2482 2483 2484 2485 | |
compute_handler
¶
compute_handler(function: Callable[[object, ClauseContext], object], *, effect: EffectRef, result_validator: RuntimeValidator, introduced: EffectRow = EffectRow(), answer_type: TypeExpr = ANSWER, key: str = 'compute') -> RuntimeHandler
Serve a Compute instance with a host function.
| PARAMETER | DESCRIPTION |
|---|---|
function
|
The host function, called with the request's argument and the
clause context, through which it may perform effects the
TYPE:
|
effect
|
The applied
TYPE:
|
result_validator
|
Checks the function's result inhabits the operation's result type.
TYPE:
|
introduced
|
Effects the host function performs. |
answer_type
|
What the handler answers with.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
Source code in src/quivers/qiec/builtins.py
3217 3218 3219 3220 3221 3222 3223 3224 3225 3226 3227 3228 3229 3230 3231 3232 3233 3234 3235 3236 3237 3238 3239 3240 3241 3242 3243 3244 3245 3246 3247 3248 3249 3250 3251 3252 3253 3254 3255 3256 3257 3258 3259 3260 3261 3262 3263 3264 3265 3266 3267 3268 3269 3270 3271 3272 3273 3274 3275 3276 3277 3278 3279 3280 3281 3282 3283 3284 3285 3286 3287 3288 3289 3290 3291 3292 3293 3294 | |
condition_handler
¶
condition_handler(observations: Mapping[object, object], *, score_instance: EffectInstanceId, result_validator: RuntimeValidator, weight_validator: RuntimeValidator = lambda _value: True, missing: MissingValuePolicy = FORWARD, extra: ExtraValuePolicy = ERROR, answer_type: TypeExpr = ANSWER, key: str = 'condition') -> RuntimeHandler
Supply likelihood observations and emit their densities as Score.
Unobserved sites forward to the next Random handler. The explicit
introduced Score row distinguishes likelihood observation from intervention
and unscored replay.
| PARAMETER | DESCRIPTION |
|---|---|
observations
|
The values to condition on, keyed by site.
TYPE:
|
score_instance
|
The lexical
TYPE:
|
result_validator
|
Checks an observed value inhabits the request's result type.
TYPE:
|
weight_validator
|
Checks each log-density contribution.
TYPE:
|
missing
|
Whether a sample request at a site with no observation is forwarded outward or rejected.
TYPE:
|
extra
|
What to do, when the handled computation returns, with an observation at a site the computation never sampled.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
Source code in src/quivers/qiec/builtins.py
1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599 1600 1601 1602 1603 1604 1605 1606 1607 1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628 1629 | |
draw_handler
¶
draw_handler(result_validator: RuntimeValidator, *, draw: Callable[[object, object, RuntimeRequest], object] | None = None, answer_type: TypeExpr = ANSWER, duplicable_context: bool = False, key: str = 'draw') -> RuntimeHandler
Interpret Random.sample by drawing exactly once.
| PARAMETER | DESCRIPTION |
|---|---|
result_validator
|
Checks the value a resumption carries inhabits the operation's result type.
TYPE:
|
draw
|
Supplies the drawn value, given the site, the sampleable, and the request. None uses the sampleable's own reparameterised or plain sampling interface.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
duplicable_context
|
Whether the handler's own state may be copied for a multi-shot resumption. Asserted rather than inferred: copying a handler owning mutable state would let two shots share it.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
Source code in src/quivers/qiec/builtins.py
684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 | |
draw_scoring_handler
¶
draw_scoring_handler(*, score_instance: EffectInstanceId, result_validator: RuntimeValidator, weight_validator: RuntimeValidator = lambda _value: True, draw: Callable[[object, object, RuntimeRequest], object] | None = None, answer_type: TypeExpr = ANSWER, key: str = 'draw-scoring') -> RuntimeHandler
Interpret Random.sample by drawing once and scoring the draw.
The draw's log density under its own sampleable is sent to a Score
instance, so a run whose latent sites are drawn accumulates the joint
density of the draw, which is what a trace of the run reports.
| PARAMETER | DESCRIPTION |
|---|---|
score_instance
|
The lexical
TYPE:
|
result_validator
|
Checks the value a resumption carries inhabits the operation's result type.
TYPE:
|
weight_validator
|
Checks each log-density contribution.
TYPE:
|
draw
|
Supplies the drawn value, given the site, the sampleable, and the request. None uses the sampleable's own sampling interface.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
Source code in src/quivers/qiec/builtins.py
2834 2835 2836 2837 2838 2839 2840 2841 2842 2843 2844 2845 2846 2847 2848 2849 2850 2851 2852 2853 2854 2855 2856 2857 2858 2859 2860 2861 2862 2863 2864 2865 2866 2867 2868 2869 2870 2871 2872 2873 2874 2875 2876 2877 2878 2879 2880 2881 2882 2883 2884 2885 2886 2887 2888 2889 2890 2891 2892 2893 2894 2895 2896 2897 2898 2899 2900 2901 2902 2903 2904 2905 2906 2907 2908 2909 2910 2911 2912 2913 2914 2915 2916 2917 2918 2919 2920 2921 2922 2923 2924 2925 2926 2927 2928 2929 | |
enumerate_handler
¶
enumerate_handler(result_validator: RuntimeValidator, *, answer_type: TypeExpr = ANSWER, weight_type: TypeExpr | None = None, reduction: str = 'logsumexp', key: str = 'enumerate') -> RuntimeHandler
Interpret Random.sample by aggregating over a finite support.
The handled computation must answer with its value paired with the
log weight it accumulated, as the collecting Weight handler
answers. The clause resumes once per support value, adds each shot's
weight to the prior log probability of its value, and aggregates the
shots by the reduction: logsumexp answers the log of the summed
probabilities, the marginal; sum the sum of the weighted shots;
mean their average. The aggregate is totalled over the plate's
positions when the latent is plated, or kept one per position when
a weight type is given, which is what a marginalization nested in a
grouped one adds to its group's weights.
| PARAMETER | DESCRIPTION |
|---|---|
result_validator
|
Checks the value a resumption carries inhabits the operation's result type.
TYPE:
|
answer_type
|
What the handled computation answers with.
TYPE:
|
weight_type
|
The type of the per-position weights the clause answers with,
the collected weights' own tensor type, whose shape the answer
takes from the shots' weights;
TYPE:
|
reduction
|
How the shots aggregate:
TYPE:
|
key
|
Distinguishes this handler from others of the same name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the reduction is not one of the three. |
Source code in src/quivers/qiec/builtins.py
1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 | |
intervene_handler
¶
intervene_handler(values: Mapping[object, object], *, result_validator: RuntimeValidator, on_intervene: Callable[[RuntimeRequest, object], None] | None = None, answer_type: TypeExpr = ANSWER, key: str = 'intervene') -> RuntimeHandler
Fix selected sites to given values without scoring them.
An intervened site's distribution is replaced by a point mass, so it contributes nothing to the joint; sites without a value forward.
| PARAMETER | DESCRIPTION |
|---|---|
values
|
The value for each intervened site, keyed by site.
TYPE:
|
result_validator
|
Checks an intervened value inhabits the request's result type.
TYPE:
|
on_intervene
|
Called with the request and the value fixed for it, so a caller can mark the site as deterministic.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
Source code in src/quivers/qiec/builtins.py
2932 2933 2934 2935 2936 2937 2938 2939 2940 2941 2942 2943 2944 2945 2946 2947 2948 2949 2950 2951 2952 2953 2954 2955 2956 2957 2958 2959 2960 2961 2962 2963 2964 2965 2966 2967 2968 2969 2970 2971 2972 2973 2974 2975 2976 2977 2978 2979 2980 2981 2982 2983 2984 2985 2986 2987 2988 2989 2990 2991 2992 2993 2994 2995 2996 2997 2998 2999 3000 3001 3002 3003 3004 3005 3006 3007 3008 3009 3010 3011 3012 3013 3014 3015 3016 3017 3018 | |
param_handler
¶
param_handler(lookup: Callable[[str, RuntimeRequest], object], *, result_validator: RuntimeValidator, total: bool = True, answer_type: TypeExpr = ANSWER, key: str = 'param') -> RuntimeHandler
Serve Param.get from a host parameter store.
| PARAMETER | DESCRIPTION |
|---|---|
lookup
|
Returns the value of the named parameter, given the name and the request.
TYPE:
|
result_validator
|
Checks a value inhabits the request's result type.
TYPE:
|
total
|
Whether the handler discharges the instance; a handler layered over a store leaves the instance in the row so the store stays required outside it.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
Source code in src/quivers/qiec/builtins.py
3297 3298 3299 3300 3301 3302 3303 3304 3305 3306 3307 3308 3309 3310 3311 3312 3313 3314 3315 3316 3317 3318 3319 3320 3321 3322 3323 3324 3325 3326 3327 3328 3329 3330 3331 3332 3333 3334 3335 3336 3337 3338 3339 3340 3341 3342 3343 3344 3345 3346 3347 3348 3349 3350 3351 3352 3353 3354 3355 3356 3357 3358 3359 3360 3361 3362 3363 3364 3365 3366 3367 3368 3369 3370 3371 3372 3373 3374 3375 3376 3377 | |
replay_handler
¶
replay_handler(values: Mapping[object, object], *, result_validator: RuntimeValidator, policy: ReplayPolicy = CLAMP_NO_SCORE, score_instance: EffectInstanceId | None = None, weight_validator: RuntimeValidator = lambda _value: True, extra: ExtraValuePolicy = ERROR, answer_type: TypeExpr = ANSWER, key: str = 'replay') -> RuntimeHandler
Replay selected sites under an explicit scoring/intervention policy.
A sample request at a site in values resumes with the recorded
value; a request at any other site is forwarded to an outer handler.
A site reached more than once, as a recurrence reaches the sites of
its step at every position, replays the value keyed "<site>@<n>"
at its n-th occurrence, counted from zero, when one is recorded,
and the value keyed by the site alone otherwise.
| PARAMETER | DESCRIPTION |
|---|---|
values
|
The recorded value for each replayed site, keyed by site, or by
site and occurrence as
TYPE:
|
result_validator
|
Checks a replayed value inhabits the request's result type.
TYPE:
|
policy
|
Whether a replayed value is also scored:
TYPE:
|
score_instance
|
The lexical
TYPE:
|
weight_validator
|
Checks each log-density contribution.
TYPE:
|
extra
|
What to do, when the handled computation returns, with a recorded site the computation never sampled.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If |
Source code in src/quivers/qiec/builtins.py
1644 1645 1646 1647 1648 1649 1650 1651 1652 1653 1654 1655 1656 1657 1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679 1680 1681 1682 1683 1684 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 1699 1700 1701 1702 1703 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717 1718 1719 1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742 1743 1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755 1756 1757 1758 1759 1760 1761 1762 1763 1764 1765 1766 1767 1768 1769 1770 1771 1772 1773 1774 1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822 1823 1824 1825 1826 1827 1828 1829 | |
reweight_handler
¶
reweight_handler(transform: Callable[[object], object], *, score_instance: EffectInstanceId, weight_validator: RuntimeValidator = lambda _value: True, answer_type: TypeExpr = ANSWER, key: str = 'reweight') -> RuntimeHandler
Transform every Score.add contribution before passing it outward.
Scaling and masking are transformers: each contribution arriving at the handler is replaced by its image and sent to the same instance's outer handler, with the provenance of the site it came from kept.
| PARAMETER | DESCRIPTION |
|---|---|
transform
|
The map applied to each contribution.
TYPE:
|
score_instance
|
The lexical
TYPE:
|
weight_validator
|
Checks each transformed contribution.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
Source code in src/quivers/qiec/builtins.py
3021 3022 3023 3024 3025 3026 3027 3028 3029 3030 3031 3032 3033 3034 3035 3036 3037 3038 3039 3040 3041 3042 3043 3044 3045 3046 3047 3048 3049 3050 3051 3052 3053 3054 3055 3056 3057 3058 3059 3060 3061 3062 3063 3064 3065 3066 3067 3068 3069 3070 3071 3072 3073 3074 3075 3076 3077 3078 3079 3080 3081 3082 3083 3084 3085 3086 3087 3088 3089 3090 3091 3092 3093 3094 3095 3096 3097 3098 3099 3100 3101 3102 3103 3104 3105 3106 3107 3108 3109 | |
score_handler
¶
score_handler(*, identity: object = 0.0, combine: Callable[[object, object], object] = _RUNTIME_ADD, weight_validator: RuntimeValidator = lambda _value: True, answer_validator: RuntimeValidator = lambda _value: True, total_validator: RuntimeValidator | None = None, expose_total: bool = False, answer_type: TypeExpr = ANSWER, key: str = 'score', observer: Callable[[RuntimeRequest, object], None] | None = None) -> tuple[RuntimeHandler, ScoreAccumulator]
Accumulate Score.add contributions in their evaluation order.
| PARAMETER | DESCRIPTION |
|---|---|
identity
|
The accumulator's value before any contribution.
TYPE:
|
combine
|
Folds a contribution into the running total.
TYPE:
|
weight_validator
|
Checks an individual weight contribution.
TYPE:
|
answer_validator
|
Checks the handled computation's answer.
TYPE:
|
total_validator
|
Checks the accumulated total;
TYPE:
|
expose_total
|
Whether the accumulated total is returned alongside the answer, rather than kept internal.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
observer
|
Called with each request and its contribution as it is accumulated, so a caller can attribute contributions to the sites their provenance names.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[RuntimeHandler, ScoreAccumulator]
|
The attachment, ready to bind into a runtime environment, and the accumulator each installation publishes into when its computation completes. |
Source code in src/quivers/qiec/builtins.py
1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 | |
search_handler
¶
search_handler(definition: HandlerDef, operation: OperationId, *, reduction: str, alternative_validator: RuntimeValidator) -> RuntimeHandler
Enumerate a tensor of alternatives, summing the shots' weights.
The handled computation answers with a unit paired with the weight a collecting handler inside it accumulated, which the return clause reduces to the weight. The clause resumes once per entry of the tensor it is asked to choose from and answers the semiring sum of what the resumptions answer, so an empty choice contributes the semiring's zero; a resumption's answer is itself a semiring sum when the continuation chooses again, and the sum is associative, so the nesting does not matter.
| PARAMETER | DESCRIPTION |
|---|---|
definition
|
The module's declaration of the handler, whose one clause handles the choosing operation with an unrestricted resumption.
TYPE:
|
operation
|
The choosing operation.
TYPE:
|
reduction
|
The semiring addition, one of
TYPE:
|
alternative_validator
|
Checks the value each resumption carries.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the reduction is unknown. |
Source code in src/quivers/qiec/builtins.py
2517 2518 2519 2520 2521 2522 2523 2524 2525 2526 2527 2528 2529 2530 2531 2532 2533 2534 2535 2536 2537 2538 2539 2540 2541 2542 2543 2544 2545 2546 2547 2548 2549 2550 2551 2552 2553 2554 2555 2556 2557 2558 2559 2560 2561 2562 2563 2564 2565 2566 2567 2568 2569 2570 2571 2572 2573 2574 2575 2576 2577 2578 2579 2580 2581 2582 2583 2584 2585 2586 2587 2588 2589 2590 2591 2592 2593 2594 2595 2596 2597 2598 2599 2600 2601 2602 2603 2604 2605 2606 2607 2608 2609 2610 2611 2612 2613 2614 2615 2616 2617 2618 2619 2620 2621 2622 2623 2624 2625 2626 2627 2628 | |
state_effect
¶
Construct the concrete State[state_type] interface.
| PARAMETER | DESCRIPTION |
|---|---|
state_type
|
The type to instantiate the interface's binder at.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRef
|
The saturated application. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the argument is not a type. |
ValueError
|
If it is ill-kinded. |
Source code in src/quivers/qiec/builtins.py
state_handler
¶
state_handler(initial: object, state_validator: RuntimeValidator, *, state_type: TypeExpr = STATE, expose_final: bool = False, answer_type: TypeExpr = ANSWER, answer_validator: RuntimeValidator = lambda _value: True, key: str = 'state') -> tuple[RuntimeHandler, StateCell]
Interpret lexical State.get/put with a nonduplicable mutable cell.
| PARAMETER | DESCRIPTION |
|---|---|
initial
|
The state before any operation.
TYPE:
|
state_validator
|
Checks the initial state, each value put, and each value got.
TYPE:
|
state_type
|
The type of the handler's state.
TYPE:
|
expose_final
|
Whether the final state is returned alongside the answer.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
answer_validator
|
Checks the handled computation's answer.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[RuntimeHandler, StateCell]
|
The attachment, ready to bind into a runtime environment, and the cell each installation publishes its final state into when its computation completes. |
| RAISES | DESCRIPTION |
|---|---|
RuntimeTypeMismatch
|
If |
Source code in src/quivers/qiec/builtins.py
2078 2079 2080 2081 2082 2083 2084 2085 2086 2087 2088 2089 2090 2091 2092 2093 2094 2095 2096 2097 2098 2099 2100 2101 2102 2103 2104 2105 2106 2107 2108 2109 2110 2111 2112 2113 2114 2115 2116 2117 2118 2119 2120 2121 2122 2123 2124 2125 2126 2127 2128 2129 2130 2131 2132 2133 2134 2135 2136 2137 2138 2139 2140 2141 2142 2143 2144 2145 2146 2147 2148 2149 2150 2151 2152 2153 2154 2155 2156 2157 2158 2159 2160 2161 2162 2163 2164 2165 2166 2167 2168 2169 2170 2171 2172 2173 2174 2175 2176 2177 2178 2179 2180 2181 2182 2183 2184 2185 2186 2187 2188 2189 2190 2191 2192 2193 2194 2195 2196 2197 2198 2199 2200 2201 2202 2203 2204 2205 2206 2207 2208 2209 2210 2211 2212 2213 2214 2215 2216 2217 2218 2219 2220 2221 2222 2223 2224 2225 2226 2227 2228 2229 2230 2231 2232 2233 2234 2235 2236 2237 2238 2239 2240 2241 2242 2243 2244 2245 2246 2247 2248 2249 2250 2251 2252 2253 2254 2255 2256 2257 | |
trace_handler
¶
trace_handler(effect: EffectRef, operations: Iterable[OperationId], recorder: TraceRecorder, *, validators: Mapping[OperationId, RuntimeValidator], answer_type: TypeExpr = ANSWER, key: str = 'trace') -> RuntimeHandler
Observe forwarded operation replies without interpreting the effect.
| PARAMETER | DESCRIPTION |
|---|---|
effect
|
The interface whose operations are recorded.
TYPE:
|
operations
|
Which operations to record.
TYPE:
|
recorder
|
Receives each recorded request.
TYPE:
|
validators
|
Per-operation result validators.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeHandler
|
The attachment, ready to bind into a runtime environment. |
Source code in src/quivers/qiec/builtins.py
1904 1905 1906 1907 1908 1909 1910 1911 1912 1913 1914 1915 1916 1917 1918 1919 1920 1921 1922 1923 1924 1925 1926 1927 1928 1929 1930 1931 1932 1933 1934 1935 1936 1937 1938 1939 1940 1941 1942 1943 1944 1945 1946 1947 1948 1949 1950 1951 1952 1953 1954 1955 1956 1957 1958 1959 1960 1961 1962 1963 1964 1965 1966 1967 1968 1969 1970 1971 1972 1973 1974 1975 1976 1977 1978 1979 1980 1981 1982 1983 1984 1985 1986 1987 1988 1989 1990 1991 1992 1993 1994 1995 1996 1997 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021 2022 2023 2024 2025 2026 2027 2028 2029 2030 2031 2032 2033 2034 2035 2036 2037 2038 2039 2040 2041 2042 2043 2044 2045 2046 2047 2048 2049 2050 2051 2052 2053 2054 2055 2056 2057 2058 2059 2060 2061 2062 | |
weight_effect
¶
Construct the concrete Weight[weight_type] interface.
| PARAMETER | DESCRIPTION |
|---|---|
weight_type
|
The type to instantiate the interface's binder at.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRef
|
The saturated application. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the argument is not a type. |
ValueError
|
If it is ill-kinded. |
Source code in src/quivers/qiec/builtins.py
weight_handler
¶
weight_handler(identity: object, combine: Callable[[object, object], object], weight_validator: RuntimeValidator, *, weight_type: TypeExpr = K, expose_total: bool = True, answer_type: TypeExpr = ANSWER, answer_validator: RuntimeValidator = lambda _value: True, total_validator: RuntimeValidator | None = None, forkable: bool = False, key: str = 'weight') -> tuple[RuntimeHandler, WeightAccumulator]
Accumulate values in a caller-supplied semiring multiplication.
| PARAMETER | DESCRIPTION |
|---|---|
identity
|
The accumulator's value before any contribution.
TYPE:
|
combine
|
Folds a contribution into the running total.
TYPE:
|
weight_validator
|
Checks an individual weight contribution.
TYPE:
|
weight_type
|
The type of an individual weight.
TYPE:
|
expose_total
|
Whether the accumulated total is returned alongside the answer, rather than kept internal.
TYPE:
|
answer_type
|
What the handler answers with.
TYPE:
|
answer_validator
|
Checks the handled computation's answer.
TYPE:
|
total_validator
|
Checks the accumulated total;
TYPE:
|
forkable
|
Whether an unrestricted resumption may capture an installation: each shot then continues from its own copy of the total so far, which is what a search inside the scope needs.
TYPE:
|
key
|
Distinguishes this handler from others of the same name, entering its derived identity.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[RuntimeHandler, WeightAccumulator]
|
The attachment, ready to bind into a runtime environment, and the accumulator each installation publishes into when its computation completes. |
Source code in src/quivers/qiec/builtins.py
2648 2649 2650 2651 2652 2653 2654 2655 2656 2657 2658 2659 2660 2661 2662 2663 2664 2665 2666 2667 2668 2669 2670 2671 2672 2673 2674 2675 2676 2677 2678 2679 2680 2681 2682 2683 2684 2685 2686 2687 2688 2689 2690 2691 2692 2693 2694 2695 2696 2697 2698 2699 2700 2701 2702 2703 2704 2705 2706 2707 2708 2709 2710 2711 2712 2713 2714 2715 2716 2717 2718 2719 2720 2721 2722 2723 2724 2725 2726 2727 2728 2729 2730 2731 2732 2733 2734 2735 2736 2737 2738 2739 2740 2741 2742 2743 2744 2745 2746 2747 2748 2749 2750 2751 2752 2753 2754 2755 2756 2757 2758 2759 2760 2761 2762 2763 2764 2765 2766 2767 2768 2769 2770 2771 2772 2773 2774 2775 2776 2777 2778 2779 2780 2781 2782 2783 2784 2785 2786 2787 2788 2789 2790 2791 2792 2793 2794 2795 2796 2797 2798 2799 2800 2801 2802 2803 2804 2805 2806 2807 2808 2809 2810 2811 2812 2813 2814 2815 2816 2817 2818 2819 2820 2821 2822 2823 2824 2825 2826 2827 2828 2829 2830 2831 | |
builtin_constructor
¶
builtin_constructor(name: str, *binders: TypeBinder | IndexBinder) -> TypeConstructorRef
A type constructor in the builtin namespace.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The constructor's name.
TYPE:
|
*binders
|
Its kinding telescope.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeConstructorRef
|
The constructor. Its identity derives from the namespace and the name alone, so it is the same constructor in every module. |
Source code in src/quivers/qiec/canonical.py
sampleable_type
¶
sampleable_type(element: TypeExpr) -> TypeApplication
The type of a distribution over element.
| PARAMETER | DESCRIPTION |
|---|---|
element
|
The sampled value's type.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeApplication
|
|
Source code in src/quivers/qiec/canonical.py
sampled_element
¶
The value type a Sampleable produces.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
A type that may be a sampleable application.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeExpr | None
|
The element type, or |
Source code in src/quivers/qiec/canonical.py
site_type
¶
site_type(element: TypeExpr) -> TypeApplication
The type of a sample site producing element.
| PARAMETER | DESCRIPTION |
|---|---|
element
|
The sampled value's type.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeApplication
|
|
Source code in src/quivers/qiec/canonical.py
tensor_shape
¶
Split a tensor type into its element type and dimensions.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
A type that may be a tensor application.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[TypeExpr, tuple[IndexTerm, ...]] | None
|
The element type and dimensions, or |
Source code in src/quivers/qiec/canonical.py
tensor_type
¶
tensor_type(element: TypeExpr, dimensions: tuple[IndexTerm, ...]) -> TypeApplication
The type of an array of element with the given static shape.
| PARAMETER | DESCRIPTION |
|---|---|
element
|
The element type.
TYPE:
|
dimensions
|
One index term per dimension, outermost first.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeApplication
|
|
Source code in src/quivers/qiec/canonical.py
check_evidence
¶
check_evidence(evidence: EqualityEvidence, context: CheckContext) -> EqualityType
Check an appeal to equality evidence and return what it proves.
| PARAMETER | DESCRIPTION |
|---|---|
evidence
|
The appeal being made, either reflexivity or an appeal to a branch given.
TYPE:
|
context
|
Scope the appeal is made in, which decides whether a branch given is still available.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EqualityType
|
The equality the evidence establishes. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the stated equality is ill-kinded, if reflexivity is claimed between unequal endpoints, if a branch given is appealed to outside its branch or with an equality other than the one it carries, or if the evidence is of an unknown class. |
Source code in src/quivers/qiec/checking.py
check_request
¶
check_request(request: EffectRequest, registry: KernelRegistry, context: CheckContext) -> tuple[EffectRef, TypeExpr]
Check one effect request and report what performing it yields.
| PARAMETER | DESCRIPTION |
|---|---|
request
|
The request to check, naming an instance, an interface application, an operation, and the arguments it carries.
TYPE:
|
registry
|
Declarations the request is resolved against.
TYPE:
|
context
|
Scope the request is made in.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[EffectRef, TypeExpr]
|
The interface application the request performs, and the type resuming it supplies. The interface comes back because the caller needs it to build the row this request adds to. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the operation is unknown, if the named interface does not own it, if the static or value arguments do not match the operation's signature, if the declared result type disagrees with the instantiated one, or if any part mentions a rigid variable out of scope. |
Source code in src/quivers/qiec/checking.py
2659 2660 2661 2662 2663 2664 2665 2666 2667 2668 2669 2670 2671 2672 2673 2674 2675 2676 2677 2678 2679 2680 2681 2682 2683 2684 2685 2686 2687 2688 2689 2690 2691 2692 2693 2694 2695 2696 2697 2698 2699 2700 2701 2702 2703 2704 2705 2706 2707 2708 2709 2710 2711 2712 2713 2714 2715 2716 2717 2718 2719 2720 2721 2722 2723 2724 2725 2726 2727 2728 2729 2730 2731 2732 2733 | |
check_static
¶
check_static(term: StaticArgument, scope: StaticScope | None = None, *, registry: KernelRegistry | None = None) -> None
Check the intrinsic kind/sort structure of one static term.
| PARAMETER | DESCRIPTION |
|---|---|
term
|
The static term to check.
TYPE:
|
scope
|
Binders in scope. None checks the term's intrinsic structure alone and permits no variable reference, which is the right mode for a closed declaration.
TYPE:
|
registry
|
Registry to resolve interface applications against. None skips that check, leaving only the structural one.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the term is ill-kinded, references an unbound or wrongly kinded static variable, carries a scoped variable where a declaration is expected, or applies a known interface wrongly. |
Source code in src/quivers/qiec/checking.py
1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 | |
check_type
¶
check_type(type_: TypeExpr, scope: StaticScope | None = None, *, registry: KernelRegistry | None = None) -> None
Check that a type expression is intrinsically well-kinded.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
The type expression to check.
TYPE:
|
scope
|
Binders in scope, or None for a closed type.
TYPE:
|
registry
|
Registry to resolve interface applications against, or None.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the expression is ill-kinded, or is a well-formed static term that is not a type, such as an index where a type is required. |
Source code in src/quivers/qiec/checking.py
infer_computation
¶
infer_computation(computation: Computation, registry: KernelRegistry, context: CheckContext = CheckContext()) -> ComputationType
Infer the result type and effect row of a computation.
This is the kernel's entry point for checking effectful code. The
row it returns is what remains unhandled: a Handle discharges its
instance, so a fully handled computation comes back with the empty
row.
| PARAMETER | DESCRIPTION |
|---|---|
computation
|
The term to check.
TYPE:
|
registry
|
Declarations the term is resolved against.
TYPE:
|
context
|
Bindings and evidence in scope. The default empty context suits a closed computation.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ComputationType
|
The result type paired with the effects still outstanding. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If two case branches share a static scope, if a request, value, or branch fails to check, if a handler's interface does not match the instance it discharges, if branch types or rows fail to unify, or if a rigid variable escapes the branch that introduced it. |
Source code in src/quivers/qiec/checking.py
infer_value
¶
infer_value(value: Value, registry: KernelRegistry, context: CheckContext = CheckContext()) -> TypeExpr
Infer the type of a pure value term.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The value to check.
TYPE:
|
registry
|
Declarations the value's types are resolved against.
TYPE:
|
context
|
Bindings and evidence in scope. The default empty context suits a closed value.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeExpr
|
The inferred type. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If a local is unbound or carries a type other than the one the term claims, if a literal's value does not inhabit its type, if a constructor is applied wrongly, if equality evidence is forged or out of scope, or if an inferred type mentions a rigid variable that escapes its branch. |
Source code in src/quivers/qiec/checking.py
2299 2300 2301 2302 2303 2304 2305 2306 2307 2308 2309 2310 2311 2312 2313 2314 2315 2316 2317 2318 2319 2320 2321 2322 2323 2324 2325 2326 2327 2328 2329 2330 2331 2332 2333 2334 2335 2336 2337 2338 2339 2340 2341 2342 2343 2344 2345 2346 2347 2348 2349 2350 2351 2352 2353 2354 2355 2356 2357 2358 2359 2360 2361 2362 2363 2364 2365 2366 2367 2368 2369 2370 2371 2372 2373 2374 2375 2376 2377 2378 2379 2380 2381 2382 2383 2384 2385 2386 2387 2388 2389 2390 2391 2392 2393 2394 2395 2396 2397 2398 2399 2400 2401 2402 2403 2404 2405 2406 2407 2408 2409 2410 2411 2412 2413 2414 2415 2416 2417 2418 2419 2420 2421 2422 2423 2424 2425 2426 2427 2428 2429 2430 2431 2432 2433 2434 2435 2436 2437 2438 2439 2440 2441 2442 2443 2444 2445 2446 2447 2448 2449 2450 2451 2452 2453 2454 2455 2456 2457 2458 2459 2460 2461 2462 2463 2464 2465 2466 2467 2468 2469 2470 2471 2472 2473 2474 2475 2476 2477 2478 2479 2480 2481 2482 2483 2484 2485 2486 2487 2488 2489 2490 2491 2492 2493 2494 2495 2496 2497 2498 2499 2500 2501 2502 2503 2504 2505 2506 2507 2508 2509 2510 2511 2512 2513 2514 2515 2516 2517 2518 2519 2520 2521 2522 2523 2524 2525 2526 2527 2528 2529 2530 2531 2532 2533 2534 2535 2536 2537 2538 2539 2540 2541 2542 2543 2544 2545 2546 2547 2548 2549 2550 2551 2552 2553 2554 2555 2556 2557 2558 2559 2560 2561 2562 2563 2564 2565 2566 2567 2568 2569 2570 2571 2572 2573 2574 2575 2576 2577 2578 2579 2580 2581 2582 2583 2584 2585 2586 2587 2588 2589 2590 2591 2592 2593 2594 2595 2596 2597 2598 2599 2600 2601 2602 2603 2604 2605 2606 2607 2608 2609 2610 2611 2612 2613 2614 2615 2616 2617 2618 2619 2620 2621 2622 2623 2624 2625 2626 2627 2628 2629 2630 2631 2632 2633 2634 2635 2636 2637 2638 2639 2640 2641 2642 2643 2644 2645 2646 2647 2648 2649 2650 2651 2652 2653 2654 2655 2656 | |
check_coverage
¶
check_coverage(family: FamilyDecl, patterns: tuple[BranchPattern, ...], *, certified_impossible: frozenset[ConstructorId] = frozenset()) -> CoverageResult
Check constructor coverage without pretending opaque cases are total.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family being matched on.
TYPE:
|
patterns
|
The branch patterns written, in source order.
TYPE:
|
certified_impossible
|
Constructors an equality solver has proven cannot occur, which may therefore be omitted without making the match incomplete.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
CoverageResult
|
The status, the constructors still missing, and any matched
twice. The status is |
Source code in src/quivers/qiec/coverage.py
check_indexed_coverage
¶
check_indexed_coverage(family: FamilyDecl, constructors: tuple[ConstructorDecl, ...], scrutinee: TypeApplication, patterns: tuple[BranchPattern, ...]) -> CoverageResult
Coverage with omissions justified by closed-index contradiction.
Only constructors that the small equality solver certifies as impossible may be omitted. An unknown result remains a required case.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family being matched on.
TYPE:
|
constructors
|
Declarations of the family's constructors, needed to refine each one against the scrutinee.
TYPE:
|
scrutinee
|
The applied family type being matched.
TYPE:
|
patterns
|
The branch patterns written.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
CoverageResult
|
Coverage judged against the constructors that remain possible. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If a constructor belongs to another family, or the scrutinee does not inhabit the matched family. |
Source code in src/quivers/qiec/coverage.py
constructor_skolems
¶
constructor_skolems(constructor: ConstructorDecl, scope: StaticScopeId) -> tuple[StaticArgument, ...]
Create rigid static variables for a constructor's local telescope.
| PARAMETER | DESCRIPTION |
|---|---|
constructor
|
The constructor whose telescope to instantiate.
TYPE:
|
scope
|
Identity of the branch scope. It enters each variable's identity, so skolems from two branches are never confused and cannot be mistaken for one another when a type escapes.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[StaticArgument, ...]
|
One rigid variable per binder, in telescope order. |
Source code in src/quivers/qiec/coverage.py
join_branch_rows
¶
join_branch_rows(branches: tuple[tuple[Reachability, EffectRow], ...]) -> EffectRow
Union effects of every possibly reachable branch.
UNKNOWN is intentionally treated as reachable. Dropping it would make
an incomplete equality solver unsound for effect inference.
| PARAMETER | DESCRIPTION |
|---|---|
branches
|
Each branch's reachability and the row its body performs.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRow
|
The union over every branch not certified impossible. Only a proven contradiction removes a branch's effects from the result. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If two reachable branches bind one instance to different interfaces, or their open tails cannot merge. |
Source code in src/quivers/qiec/coverage.py
refine_branch
¶
refine_branch(family: FamilyDecl, constructor: ConstructorDecl, scrutinee: TypeApplication, constructor_arguments: tuple[StaticArgument, ...]) -> BranchRefinement
Introduce constructor skolems and index equalities for a branch.
The equality solver is intentionally conservative. Syntactically equal
indices are reachable; contradictory closed literals are impossible; all
other equations remain UNKNOWN and must still contribute branch
effects and coverage.
| PARAMETER | DESCRIPTION |
|---|---|
family
|
The family being matched on.
TYPE:
|
constructor
|
The constructor this branch matches.
TYPE:
|
scrutinee
|
The applied family type being scrutinised, supplying the parameters and the indices to be refined.
TYPE:
|
constructor_arguments
|
Arguments instantiating the constructor's local telescope,
normally the rigid skolems from
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
BranchRefinement
|
The skolems in scope, the equalities the match makes available, and whether the branch is reachable. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the constructor belongs to another family, if the scrutinee does not inhabit the matched family, or if the scrutinee supplies the wrong number of arguments. |
Source code in src/quivers/qiec/coverage.py
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 | |
distribution_backend
¶
distribution_backend() -> DistributionBackend
The backend distribution values currently sample and score through.
| RETURNS | DESCRIPTION |
|---|---|
DistributionBackend
|
The installed backend; the reference backend until replaced. |
Source code in src/quivers/qiec/distributions.py
install_distribution_backend
¶
install_distribution_backend(backend: DistributionBackend) -> DistributionBackend
Replace the backend distribution values sample and score through.
| PARAMETER | DESCRIPTION |
|---|---|
backend
|
The backend to install, such as one over a host library that covers every family.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
DistributionBackend
|
The backend that was installed before, so a caller can restore it. |
Source code in src/quivers/qiec/distributions.py
seed_reference_rng
¶
Reseed the generator reference draws use by default.
| PARAMETER | DESCRIPTION |
|---|---|
seed
|
The seed; two runs seeded alike draw alike.
TYPE:
|
instantiate_effect
¶
instantiate_effect(effect: EffectRef, *, module: str, lexical_path: tuple[str | int, ...]) -> RowEntry
Allocate a deterministic lexical instance of an effect interface.
The instance identity is derived rather than generated, so the same interface allocated at the same place in the same module is the same instance on every run. That is what lets a serialized row refer to an instance across processes.
| PARAMETER | DESCRIPTION |
|---|---|
effect
|
The saturated interface application to allocate.
TYPE:
|
module
|
Module the allocation occurs in. Part of the identity, so two modules allocating at the same lexical path stay distinct.
TYPE:
|
lexical_path
|
Position of the allocation within the module. Two allocations of one interface at different paths are different instances, which is what makes two instances of the same effect distinguishable.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RowEntry
|
The fresh instance paired with the interface it implements, ready to add to a row. |
Source code in src/quivers/qiec/effects.py
render_instance
¶
render_instance(identity: EffectInstanceId, names: Mapping[EffectInstanceId, str] | None = None) -> str
Render one effect instance in the surface spelling.
| PARAMETER | DESCRIPTION |
|---|---|
identity
|
The instance.
TYPE:
|
names
|
The source name of each lexical instance.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
str
|
Its source name, or |
Source code in src/quivers/qiec/effects.py
render_row
¶
render_row(row: EffectRow, names: Mapping[EffectInstanceId, str] | None = None) -> str
Render an effect row in the surface spelling.
| PARAMETER | DESCRIPTION |
|---|---|
row
|
The row.
TYPE:
|
names
|
The source name of each lexical instance; an instance with no name renders as the first eight characters of its digest.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
str
|
|
Source code in src/quivers/qiec/effects.py
unify_effect_rows
¶
unify_effect_rows(left: EffectRow, right: EffectRow) -> RowUnification
Unify two rows, returning their common row and tail substitution.
Unification is symmetric and driven by the tails. Two closed rows unify only when already equal. One open row unifies with a closed one by binding its tail to the entries it lacks. Two open rows with distinct tails unify by binding both to a fresh tail carrying every instance either side names.
| PARAMETER | DESCRIPTION |
|---|---|
left
|
One row to unify.
TYPE:
|
right
|
The other row. The result does not depend on the order of the two arguments.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RowUnification
|
The common row and the substitution taking both inputs to it. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the rows bind one instance to different interfaces, if two closed rows differ, if an open row carries an entry the closed row lacks, if one side needs an instance the other's tail is proven to lack, or if the computed substitution fails to carry both inputs to the unified row. |
Source code in src/quivers/qiec/effects.py
493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 | |
entry_point
¶
entry_point(module: QiecModule, name: str) -> EntryPoint
One entry point of a module, by name.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The checked module.
TYPE:
|
name
|
The entry's source name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EntryPoint
|
The entry. |
| RAISES | DESCRIPTION |
|---|---|
ExecutionFailure
|
With code |
Source code in src/quivers/qiec/entries.py
entry_points
¶
entry_points(module: QiecModule) -> tuple[EntryPoint, ...]
Every executable entry point of a module.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The checked module.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[EntryPoint, ...]
|
The programs and the computations, in declaration order; a computation a program elaborated to appears once, as the program, and a marginalization helper not at all. |
Source code in src/quivers/qiec/entries.py
invoke_entry
¶
invoke_entry(module: QiecModule, name: str, arguments: Sequence[HostValue] = (), *, data: Mapping[str, HostValue] | None = None, sites: Mapping[str, HostValue] | None = None, static_arguments: Sequence[str] = (), runtime: RuntimeConfiguration | None = None, fuel: int | None = None, seed: int | None = None, observer: TraceObserver | None = None) -> EntryRun
Invoke an entry point.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The checked module.
TYPE:
|
name
|
The entry's source name.
TYPE:
|
arguments
|
Host values for the entry's value parameters, in order. A
program's parameters may instead, or additionally, be given by
name through
TYPE:
|
data
|
A program's parameters by name: its data, observations, fibrations, and scalars. A name given both positionally and here is an error.
TYPE:
|
sites
|
The values a program run conditions its sample sites on, by label; every other site is drawn. Not accepted for a computation.
TYPE:
|
static_arguments
|
Closed terms instantiating a computation's telescope, as
TYPE:
|
runtime
|
The providers a computation runs under; the core provider alone by default. A program's handlers are fixed by the run, so only the default configuration is accepted for a program.
TYPE:
|
fuel
|
A step budget for the run.
TYPE:
|
seed
|
A seed for the reference generator every draw of the run uses;
two runs seeded alike draw alike.
TYPE:
|
observer
|
A callback receiving every trace event as it is emitted.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EntryRun
|
The value, the log joint for a program, and the execution result. |
| RAISES | DESCRIPTION |
|---|---|
ExecutionFailure
|
With code |
Source code in src/quivers/qiec/entries.py
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 | |
json_value
¶
Read a parsed JSON value as a host value.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The parsed JSON.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
HostValue
|
The value with every list read as a tuple, which is how the runtime carries a tensor. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the value is |
Source code in src/quivers/qiec/entries.py
parse_bindings
¶
parse_bindings(items: Sequence[str]) -> dict[str, HostValue]
Read NAME=JSON bindings, as the command line and REPL take them.
| PARAMETER | DESCRIPTION |
|---|---|
items
|
The bindings as typed.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
dict[str, HostValue]
|
Name to the parsed value, lists read as tuples. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If an item has no |
Source code in src/quivers/qiec/entries.py
render_entry
¶
render_entry(entry: EntryPoint) -> str
Render an entry point as one signature line.
| PARAMETER | DESCRIPTION |
|---|---|
entry
|
The entry.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
str
|
|
Source code in src/quivers/qiec/entries.py
available_runtime_providers
¶
Return built-in and installed quivers.qiec_runtime entry points.
| RETURNS | DESCRIPTION |
|---|---|
tuple[str, ...]
|
Every selectable provider name, sorted. |
Source code in src/quivers/qiec/execution.py
load_runtime_configuration
¶
load_runtime_configuration(path: str | Path) -> RuntimeConfiguration
Load an explicit runtime selection without importing executable code.
| PARAMETER | DESCRIPTION |
|---|---|
path
|
A JSON file in the format :func:
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeConfiguration
|
The decoded selection. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If the file cannot be read, is not valid JSON, or does not decode as a runtime configuration. |
Source code in src/quivers/qiec/execution.py
parse_static_arguments
¶
parse_static_arguments(module: QiecModule, computation: str, assignments: tuple[str, ...]) -> tuple[StaticArgument, ...]
Resolve CLI NAME=TERM specializations in telescope order.
This intentionally accepts only closed, nominal terms available in the module: primitive or declared types, closed index constructors/literals, and declared effect applications. Static variables and inferred holes are not runtime configuration values.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module declaring
TYPE:
|
computation
|
The named computation whose telescope is being instantiated.
TYPE:
|
assignments
|
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[StaticArgument, ...]
|
The parsed arguments in the telescope's order. |
| RAISES | DESCRIPTION |
|---|---|
ExecutionFailure
|
With code |
Source code in src/quivers/qiec/execution.py
1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599 1600 1601 1602 1603 1604 1605 1606 1607 1608 1609 1610 1611 1612 | |
register_runtime_provider
¶
register_runtime_provider(name: str, factory: RuntimeProviderFactory) -> None
Register a provider factory for explicit configuration by name.
Registration makes a provider selectable; it never activates that provider for an invocation. Replacing an existing name is rejected so plugin load order cannot silently change execution semantics.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The name a configuration uses to select the provider.
TYPE:
|
factory
|
The callable building a provider from JSON-compatible options.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If |
Source code in src/quivers/qiec/execution.py
run_named
¶
run_named(module: QiecModule, computation: str, arguments: tuple[object, ...] = (), *, static_arguments: tuple[StaticArgument, ...] = (), runtime: RuntimeConfiguration | None = None, observer: TraceObserver | None = None, fuel: int | None = None) -> ExecutionResult
Validate and execute one named computation from module.
The attachment table and every configured provider instance are allocated inside this call. Mutable handler state can thus never leak from one named invocation to the next.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module declaring the computation; it is validated before the body is evaluated.
TYPE:
|
computation
|
The name of the computation to run.
TYPE:
|
arguments
|
Host values for the computation's value parameters, in order.
TYPE:
|
static_arguments
|
Closed terms instantiating the computation's telescope, in order; required whenever the telescope is non-empty.
TYPE:
|
runtime
|
The providers to attach; defaults to the core provider alone.
TYPE:
|
observer
|
A callback receiving every trace event as it is emitted.
TYPE:
|
fuel
|
The number of machine steps the run may take, or
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ExecutionResult
|
The validated result value, its specialized type, the runtime label, and the full trace. |
| RAISES | DESCRIPTION |
|---|---|
ExecutionFailure
|
With code |
Source code in src/quivers/qiec/execution.py
1658 1659 1660 1661 1662 1663 1664 1665 1666 1667 1668 1669 1670 1671 1672 1673 1674 1675 1676 1677 1678 1679 1680 1681 1682 1683 1684 1685 1686 1687 1688 1689 1690 1691 1692 1693 1694 1695 1696 1697 1698 1699 1700 1701 1702 1703 1704 1705 1706 1707 1708 1709 1710 1711 1712 1713 1714 1715 1716 1717 1718 1719 1720 1721 1722 1723 1724 1725 1726 1727 1728 1729 1730 1731 1732 1733 1734 1735 1736 1737 1738 1739 1740 1741 1742 1743 1744 1745 1746 1747 1748 1749 1750 1751 1752 1753 1754 1755 1756 1757 1758 1759 1760 1761 1762 1763 1764 1765 1766 1767 1768 1769 1770 1771 1772 1773 1774 1775 1776 1777 1778 1779 1780 1781 1782 1783 1784 1785 1786 1787 1788 1789 1790 1791 1792 1793 1794 1795 1796 1797 1798 1799 1800 1801 1802 1803 1804 1805 1806 1807 1808 1809 1810 1811 1812 1813 1814 1815 1816 1817 1818 1819 1820 1821 1822 1823 1824 1825 1826 1827 1828 1829 1830 1831 1832 1833 1834 1835 1836 1837 1838 1839 1840 1841 1842 1843 1844 1845 1846 1847 1848 1849 1850 1851 1852 1853 1854 1855 1856 1857 1858 1859 1860 1861 1862 1863 1864 1865 1866 1867 1868 1869 1870 1871 1872 1873 1874 1875 1876 1877 1878 1879 1880 1881 1882 1883 1884 1885 1886 1887 1888 1889 1890 1891 1892 1893 1894 1895 1896 1897 1898 1899 1900 1901 1902 1903 1904 1905 1906 1907 1908 1909 1910 | |
runtime_configuration_from_data
¶
runtime_configuration_from_data(data: object) -> RuntimeConfiguration
Decode the non-executable JSON runtime configuration format.
| PARAMETER | DESCRIPTION |
|---|---|
data
|
The decoded JSON document;
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeConfiguration
|
The selections in document order, with no programmatic providers. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If |
Source code in src/quivers/qiec/execution.py
family
¶
family(name: str) -> DistributionFamily
Look up a distribution family by source name.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The family's source name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
DistributionFamily
|
The family's semantic record. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If no family has the name. |
Source code in src/quivers/qiec/families.py
validate_telescope
¶
validate_telescope(telescope: Telescope) -> None
Reject duplicate names in one dependent telescope.
| PARAMETER | DESCRIPTION |
|---|---|
telescope
|
The binders to check, in order.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If a binder name is empty or repeats. Later binders may depend on earlier ones, so a repeated name would make a reference ambiguous. |
Source code in src/quivers/qiec/kinds.py
called_computations
¶
called_computations(body: Computation) -> frozenset[ComputationId]
The computations a body calls, directly.
| PARAMETER | DESCRIPTION |
|---|---|
body
|
The body to walk.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
frozenset[ComputationId]
|
The callee of every |
Source code in src/quivers/qiec/module.py
computation_type_conforms
¶
computation_type_conforms(actual: ComputationType, declared: ComputationType) -> bool
Check exact rows or sound weakening into an explicitly open row.
An inferred open tail can inhabit a declared open row only when it proves every absence guaranteed by the declaration. Row-variable names and IDs are lexical identities, so conformance compares their constraints rather than treating unrelated tails as identical.
| PARAMETER | DESCRIPTION |
|---|---|
actual
|
The type inferred from the body.
TYPE:
|
declared
|
The type the declaration states.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
bool
|
True when the body's type inhabits the declaration. The result types must be equal; the rows may differ only by the inferred row being weakened into a declared open one that it proves every absence of. |
Source code in src/quivers/qiec/module.py
inferred_computation_type
¶
inferred_computation_type(module: QiecModule, registry: KernelRegistry, name: str) -> ComputationType
The type a named computation's body has, as the checker infers it.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module, already validated.
TYPE:
|
registry
|
The registry
TYPE:
|
name
|
The computation's name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ComputationType
|
The inferred result type and the row the body performs, which the declared row may widen. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If the module has no computation of that name. |
Source code in src/quivers/qiec/module.py
program_computations
¶
program_computations(module: QiecModule) -> frozenset[ComputationId]
The computations that hold programs and their own helpers.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
frozenset[ComputationId]
|
The identity of every entry point's computation and of every computation the elaboration made for a program, such as a marginalization helper or a scan's recurrence: what a target renders from the program's plan rather than as a computation of its own. |
Source code in src/quivers/qiec/module.py
reachable_computations
¶
reachable_computations(module: QiecModule) -> frozenset[ComputationId]
The computations a program reaches.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
frozenset[ComputationId]
|
The identity of every entry point's computation and of every computation it calls, transitively. |
Source code in src/quivers/qiec/module.py
render_computation_type
¶
render_computation_type(type_: ComputationType, names: Mapping[EffectInstanceId, str] | None = None) -> str
Render a computation type as its result and row.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
The type.
TYPE:
|
names
|
The source name of each lexical instance, for the row.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
str
|
|
Source code in src/quivers/qiec/module.py
validate_module
¶
validate_module(module: QiecModule) -> KernelRegistry
Recheck a whole lowered module and return its resolved registry.
This is deliberately independent of the lowerer. It rebuilds the registry from the module's own declarations and rechecks every body against it, so a module that arrived from elsewhere, or from a lowerer with a bug, is held to the same standard as one just built.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The lowered module to recheck.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
KernelRegistry
|
The registry resolved from the module's declarations, for a caller that wants to check further terms against it. |
| RAISES | DESCRIPTION |
|---|---|
KernelError
|
If the ABI does not match, a declaration is ill-formed, an instance or index sort is undeclared, a body fails to check, or an inferred type does not conform to the declared one. |
Source code in src/quivers/qiec/module.py
416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 | |
primitive
¶
primitive(name: str) -> PrimitiveSignature
Look up a primitive by name.
| PARAMETER | DESCRIPTION |
|---|---|
name
|
The nominal name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
PrimitiveSignature
|
The primitive's signature. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If no primitive has the name. Callers turn this into a source-located diagnostic; the registry itself has no location to blame. |
Source code in src/quivers/qiec/primitives.py
deduction_item
¶
deduction_item(module: QiecModule, name: str, symbol: str, *fields: object) -> RuntimeConstructor
Build an item of a deduction's family as a host value.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module holding the deduction.
TYPE:
|
name
|
The deduction's name.
TYPE:
|
symbol
|
The atom or constructor symbol, as the deduction spells it.
TYPE:
|
*fields
|
The constructor's fields: integers for position slots, items for the rest.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeConstructor
|
The item, which |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If the deduction declares no such symbol. |
ValueError
|
If the field count differs from the constructor's arity. |
Source code in src/quivers/qiec/program_runtime.py
foreign_handler_configuration
¶
foreign_handler_configuration(module: QiecModule) -> dict[str, object]
The runtime configuration of a module's elaborated foreign handlers.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
dict[str, object]
|
By handler name: the enumeration handlers of marginalization blocks, the collecting handlers of those blocks and of deductions, and the search handlers of deductions, each with the options its name records. |
Source code in src/quivers/qiec/program_runtime.py
joint_module
¶
joint_module(module: QiecModule, name: str) -> tuple[QiecModule, str]
Extend a module with a computation scoring one program's log joint.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module holding the program.
TYPE:
|
name
|
The program's name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[QiecModule, str]
|
The extended module and the wrapper computation's name. The
wrapper takes the program's parameters, handles its |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If the module has no such program. |
Source code in src/quivers/qiec/program_runtime.py
program_entry
¶
program_entry(module: QiecModule, name: str) -> ProgramEntry
Find a program's entry point in a module.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module.
TYPE:
|
name
|
The program's name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ProgramEntry
|
The entry. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If the module has no program of that name. |
Source code in src/quivers/qiec/program_runtime.py
run_deduction
¶
run_deduction(module: QiecModule, name: str, *, tokens: Sequence[str] | None = None, axioms: Sequence[object] | None = None, axiom_weights: Sequence[object] | None = None, parameters: Mapping[str, object] | None = None, fuel: int | None = None) -> DeductionRun
Run a deduction's entry on the reference machine.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module holding the deduction.
TYPE:
|
name
|
The deduction's name.
TYPE:
|
tokens
|
The sentence, for a deduction with a lexicon.
TYPE:
|
axioms
|
The axiom items, for a deduction without one; runtime constructor values of its item family.
TYPE:
|
axiom_weights
|
One weight per axiom in the semiring's carrier.
TYPE:
|
parameters
|
The learned weights by name; an absent weight reads as zero.
TYPE:
|
fuel
|
A step budget for the run.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
DeductionRun
|
The goal's inside weight. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If the module has no such deduction. |
ValueError
|
If the input does not fit the deduction: tokens for one that takes axioms, or the reverse. |
ExecutionFailure
|
If the run fails. |
Source code in src/quivers/qiec/program_runtime.py
919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 | |
run_program
¶
run_program(module: QiecModule, name: str, *, data: Mapping[str, object], sites: Mapping[str, object], parameters: Mapping[str, object] | None = None, static_arguments: Sequence[StaticArgument] = (), fuel: int | None = None, observer: TraceObserver | None = None, providers: tuple[RuntimeProvider, ...] = ()) -> ProgramRun
Run a program with every site replayed and score its log joint.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module holding the program.
TYPE:
|
name
|
The program's name.
TYPE:
|
data
|
A host value for each of the program's parameters, by name: its data, observations, fibrations, and map numbers.
TYPE:
|
sites
|
A host value for each sampled site, by label, or by label and
occurrence as
TYPE:
|
parameters
|
The learned weights a deduction the program calls reads, by name; an absent weight reads as zero.
TYPE:
|
static_arguments
|
The program's static extents, one per telescope binder, for an extent no data fixes (a template's object parameter); empty when the data fix every extent.
TYPE:
|
fuel
|
A step budget for the run.
TYPE:
|
observer
|
A callback receiving every trace event as it is emitted.
TYPE:
|
providers
|
Additional typed providers used by computations the program calls.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ProgramRun
|
The returned value and the log joint. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If the module has no such program, a parameter is not given, or an open extent cannot be read off the data. |
ExecutionFailure
|
If the run fails, a site is missing, or a value does not inhabit its type. |
Source code in src/quivers/qiec/program_runtime.py
565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 | |
sample_module
¶
sample_module(module: QiecModule, name: str) -> tuple[QiecModule, str]
Extend a module with a computation running one program forward.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module holding the program.
TYPE:
|
name
|
The program's name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[QiecModule, str]
|
The extended module and the wrapper computation's name. The
wrapper takes the program's parameters, handles its |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If the module has no such program. |
Source code in src/quivers/qiec/program_runtime.py
sample_program
¶
sample_program(module: QiecModule, name: str, *, data: Mapping[str, object], sites: Mapping[str, object] | None = None, parameters: Mapping[str, object] | None = None, static_arguments: Sequence[StaticArgument] = (), fuel: int | None = None, observer: TraceObserver | None = None, providers: tuple[RuntimeProvider, ...] = ()) -> ProgramRun
Run a program forward, drawing every site it is not given.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The module holding the program.
TYPE:
|
name
|
The program's name.
TYPE:
|
data
|
A host value for each of the program's parameters, by name: its data, observations, fibrations, and map numbers.
TYPE:
|
sites
|
A host value for each conditioned site, by label, or by label
and occurrence as
TYPE:
|
parameters
|
The learned weights a deduction the program calls reads, by name; an absent weight reads as zero.
TYPE:
|
static_arguments
|
The program's static extents, one per telescope binder, for an extent no data fixes; empty when the data fix every extent.
TYPE:
|
fuel
|
A step budget for the run.
TYPE:
|
observer
|
A callback receiving every trace event as it is emitted.
TYPE:
|
providers
|
Additional typed providers used by computations the program calls.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ProgramRun
|
The returned value and the log joint of the drawn and given sites together with the program's observations and scores. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If the module has no such program, a parameter is not given, or an open extent cannot be read off the data. |
ExecutionFailure
|
If the run fails or a value does not inhabit its type. |
Source code in src/quivers/qiec/program_runtime.py
646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 | |
static_arguments_for
¶
static_arguments_for(entry: ProgramEntry, data: Mapping[str, object], given: Sequence[StaticArgument] = ()) -> tuple[StaticArgument, ...]
Read a program's static extents off the data it is applied to.
| PARAMETER | DESCRIPTION |
|---|---|
entry
|
The program's entry point, whose telescope names the extents.
TYPE:
|
data
|
The host value of each parameter, by name.
TYPE:
|
given
|
Static arguments supplied explicitly, one per telescope binder in telescope order, or none. A template's object parameter is an extent no data fixes, so a run of the template supplies it; a binder the data does fix must agree with what is supplied.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[StaticArgument, ...]
|
One index literal per telescope binder, in telescope order: the length of the axis of the first parameter whose tensor type is shaped by the binder, else the supplied argument. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If a binder shapes no parameter and none is supplied, or the parameter is not given or has too few axes, or a supplied argument disagrees with the data, or the supplied arguments do not number the telescope. |
Source code in src/quivers/qiec/program_runtime.py
480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 | |
dumps
¶
Serialize a QIEC graph as deterministic UTF-8-compatible JSON text.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The graph to serialize.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
str
|
Compact, key-sorted JSON. Determinism matters because identities downstream are content addressed: the same graph must produce the same bytes on every run and every platform. |
| RAISES | DESCRIPTION |
|---|---|
SerializationError
|
If the graph contains a value that may not cross the boundary. |
Source code in src/quivers/qiec/serialization.py
from_data
¶
Decode a QIEC graph, rejecting other ABIs and unknown node tags.
| PARAMETER | DESCRIPTION |
|---|---|
data
|
The decoded envelope.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
The reconstructed graph. |
| RAISES | DESCRIPTION |
|---|---|
SerializationError
|
If the envelope is malformed, declares another wire format or ABI, or holds a graph that fails to decode. An ABI mismatch is refused rather than attempted, since a payload from another version may use the same tags for different shapes. |
Source code in src/quivers/qiec/serialization.py
loads
¶
Deserialize one canonical QIEC JSON document.
| PARAMETER | DESCRIPTION |
|---|---|
text
|
The document to read.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
object
|
The reconstructed graph. |
| RAISES | DESCRIPTION |
|---|---|
SerializationError
|
If the text is not valid JSON, repeats an object key at any depth, or fails any of the decoding checks. |
Source code in src/quivers/qiec/serialization.py
to_data
¶
to_data(value: object) -> dict[str, JsonValue]
Encode a stable QIEC graph in its versioned wire envelope.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The graph to encode.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
dict[str, JsonValue]
|
The envelope, carrying the wire format and the ABI alongside the graph. Both are recorded because neither can be guessed from the payload, and a reader that guessed wrong would misread it. |
| RAISES | DESCRIPTION |
|---|---|
SerializationError
|
If the graph contains a value that may not cross the boundary. |
Source code in src/quivers/qiec/serialization.py
instantiate_operation
¶
instantiate_operation(operation: OperationDef, arguments: tuple[StaticArgument, ...], outer: StaticSubstitution = StaticSubstitution()) -> tuple[tuple[TypeExpr, ...], TypeExpr]
Instantiate an operation's signature at a request site.
| PARAMETER | DESCRIPTION |
|---|---|
operation
|
The declared operation.
TYPE:
|
arguments
|
Static arguments for the operation's own telescope.
TYPE:
|
outer
|
Bindings already in force from the interface's telescope. These come first, so an operation binder of the same name shadows the interface's, which is the scoping a reader expects.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[tuple[TypeExpr, ...], TypeExpr]
|
The instantiated parameter types and result type. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If an argument is of the wrong static class for its binder. |
ValueError
|
If the argument count is wrong, or an argument is ill-kinded. |
Source code in src/quivers/qiec/substitution.py
instantiate_telescope
¶
instantiate_telescope(telescope: Telescope, arguments: tuple[StaticArgument, ...]) -> StaticSubstitution
Kind-check static arguments and construct their substitution.
| PARAMETER | DESCRIPTION |
|---|---|
telescope
|
The binders to instantiate, in order. Later binders may depend on earlier ones, so the arguments are checked left to right with the substitution built so far already applied.
TYPE:
|
arguments
|
One argument per binder.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
StaticSubstitution
|
The substitution carrying each binder to its argument. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If an argument is of the wrong static class for its binder. |
ValueError
|
If the counts differ, or an argument is of the wrong kind or index sort. |
Source code in src/quivers/qiec/substitution.py
substitute_computation
¶
substitute_computation(computation: Computation, substitution: StaticSubstitution) -> Computation
Substitute static arguments throughout a computation.
Capture cannot occur, and the reason is structural rather than a
freshening pass. A substitution binds declaration binders, which
carry no identity and are matched by name. Every binder a computation
introduces is rigid: a case branch's skolems are built with derived
StaticVariableIds, and substitute_type and substitute_static
return a variable carrying an identity unchanged. So a branch's own
binders are invisible to substitution while references to an
enclosing declaration binder inside that branch are rewritten, which
is exactly the capture-avoiding behavior.
| PARAMETER | DESCRIPTION |
|---|---|
computation
|
The computation to rewrite.
TYPE:
|
substitution
|
The static bindings to apply.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Computation
|
The computation with every static position substituted. Identities are preserved throughout: a call still names the same callee, a handle the same handler, and an allocation the same instance. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the computation, or a term nested in it, is of an unknown class. |
Source code in src/quivers/qiec/substitution.py
659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 | |
substitute_effect
¶
substitute_effect(effect: EffectRef, substitution: StaticSubstitution) -> EffectRef
Substitute into an interface application's static arguments.
| PARAMETER | DESCRIPTION |
|---|---|
effect
|
The application to rewrite.
TYPE:
|
substitution
|
The bindings to apply.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRef
|
The application with its arguments rewritten. The declaration's identity and name are unchanged, since substitution instantiates an interface rather than selecting a different one. |
Source code in src/quivers/qiec/substitution.py
substitute_evidence
¶
substitute_evidence(evidence: EqualityEvidence, substitution: StaticSubstitution) -> EqualityEvidence
Substitute into the equality an evidence term states.
| PARAMETER | DESCRIPTION |
|---|---|
evidence
|
The evidence to rewrite.
TYPE:
|
substitution
|
The static bindings to apply.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EqualityEvidence
|
Evidence of the same class stating the substituted equality. A branch given keeps its identity, since substituting into what it proves does not make it a different piece of evidence. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the evidence is of an unknown class. |
Source code in src/quivers/qiec/substitution.py
substitute_index
¶
substitute_index(term: IndexTerm, substitution: StaticSubstitution) -> IndexTerm
Substitute into an index term.
| PARAMETER | DESCRIPTION |
|---|---|
term
|
The index to rewrite.
TYPE:
|
substitution
|
The bindings to apply.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
IndexTerm
|
The rewritten index. A variable carrying an identity is rigid and is returned unchanged, which is what keeps a branch's skolem from being captured by a like-named declaration binder. |
Source code in src/quivers/qiec/substitution.py
substitute_plate
¶
substitute_plate(plate: PlateShape, substitution: StaticSubstitution) -> PlateShape
Substitute static variables in a plate's axis sizes.
| PARAMETER | DESCRIPTION |
|---|---|
plate
|
The plate.
TYPE:
|
substitution
|
The static substitution.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
PlateShape
|
The plate with every axis size substituted. |
Source code in src/quivers/qiec/substitution.py
substitute_request
¶
substitute_request(request: EffectRequest, substitution: StaticSubstitution) -> EffectRequest
Substitute static arguments throughout an effect request.
| PARAMETER | DESCRIPTION |
|---|---|
request
|
The request to rewrite.
TYPE:
|
substitution
|
The static bindings to apply.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRequest
|
The request against the substituted interface application, with its own static and value arguments and result type rewritten. The instance, the operation, and the site are identities and do not move. |
Source code in src/quivers/qiec/substitution.py
substitute_row
¶
substitute_row(row: EffectRow, substitution: StaticSubstitution) -> EffectRow
Substitute into every interface application in an effect row.
| PARAMETER | DESCRIPTION |
|---|---|
row
|
The row to rewrite.
TYPE:
|
substitution
|
The bindings to apply.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
EffectRow
|
The row with each entry's interface rewritten. Instance identities and the open tail are untouched: this substitutes static arguments, and a row variable is solved by unification rather than by this substitution. |
Source code in src/quivers/qiec/substitution.py
substitute_static
¶
substitute_static(term: StaticArgument, substitution: StaticSubstitution) -> StaticArgument
Substitute into a static argument of any namespace.
| PARAMETER | DESCRIPTION |
|---|---|
term
|
A type, index, or effect argument.
TYPE:
|
substitution
|
The bindings to apply.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
StaticArgument
|
The rewritten argument, dispatched to the namespace it belongs to. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the term is of an unknown class. |
Source code in src/quivers/qiec/substitution.py
substitute_type
¶
substitute_type(type_: TypeExpr, substitution: StaticSubstitution) -> TypeExpr
Substitute into a type expression.
| PARAMETER | DESCRIPTION |
|---|---|
type_
|
The type to rewrite.
TYPE:
|
substitution
|
The bindings to apply.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeExpr
|
The rewritten type. As with indices, a variable carrying an identity is rigid and survives unchanged. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the expression is of an unknown class. |
Source code in src/quivers/qiec/substitution.py
substitute_value
¶
substitute_value(value: Value, substitution: StaticSubstitution) -> Value
Substitute static arguments throughout a value term.
| PARAMETER | DESCRIPTION |
|---|---|
value
|
The value to rewrite.
TYPE:
|
substitution
|
The static bindings to apply.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Value
|
The value with every type, index, and effect position substituted. Value-level structure is untouched: this rewrites the static layer, not the data. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the value is of an unknown class. |
Source code in src/quivers/qiec/substitution.py
460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 | |
check_static_arguments
¶
check_static_arguments(telescope: Telescope, arguments: tuple[StaticArgument, ...]) -> tuple[tuple[tuple[str, TypeExpr], ...], tuple[tuple[str, IndexTerm], ...], tuple[tuple[str, EffectRef | EffectVariable], ...]]
Kind-check static arguments against a telescope and classify them.
| PARAMETER | DESCRIPTION |
|---|---|
telescope
|
The binders the arguments instantiate, in order.
TYPE:
|
arguments
|
One argument per binder.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
tuple[tuple[tuple[str, TypeExpr], ...], tuple[tuple[str, IndexTerm], ...], tuple[tuple[str, EffectRef | EffectVariable], ...]]
|
The type, index, and effect bindings the arguments make, each paired with its binder's name, in telescope order. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the counts differ, an argument is of the wrong static class for its binder, or an argument is of the wrong kind or index sort. |
ValueError
|
If a nested application is ill-kinded, or an index constructor is applied at the wrong arity. |
Source code in src/quivers/qiec/types.py
index_sort
¶
Return an index term's sort, checking shape dimensions.
| PARAMETER | DESCRIPTION |
|---|---|
term
|
The index whose sort is wanted.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
IndexSort
|
The term's sort. A shape reports its concrete rank, which is what lets a rank-polymorphic binder accept it while a binder of a fixed rank does not. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If a shape dimension is not of |
Source code in src/quivers/qiec/types.py
product_type
¶
product_type(*components: TypeExpr) -> TypeApplication
Construct the canonical finite-product type of the given arity.
| PARAMETER | DESCRIPTION |
|---|---|
components
|
The component types, in order.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
TypeApplication
|
The product. Its constructor identity derives from the arity, so every two-component product in every module is the same type constructor and two products of different arity are different ones. |
Source code in src/quivers/qiec/types.py
render_static
¶
render_static(term: StaticArgument) -> str
Render a static term in the surface spelling.
| PARAMETER | DESCRIPTION |
|---|---|
term
|
The type, index, or effect term to render.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
str
|
A readable rendering: a constructor applied to its arguments in
brackets, with shape arguments in parentheses after them; an
arrow for a function type; an equality with |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the term is not a static term. |
Source code in src/quivers/qiec/types.py
static_kind
¶
static_kind(term: StaticArgument) -> Kind
Return the outer kind of a static term.
Index sorts are deliberately not collapsed into Type: callers that
validate an index binder compare the term's concrete sort separately.
| PARAMETER | DESCRIPTION |
|---|---|
term
|
The static term to classify.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Kind
|
The term's kind. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If the term is an index, which carries a sort rather than a kind. Raising rather than returning a placeholder is what keeps a caller from comparing an index against a kind and finding them equal. |
Source code in src/quivers/qiec/types.py
validate_static_argument
¶
validate_static_argument(term: StaticArgument) -> None
Recursively validate one intrinsically kinded static argument.
| PARAMETER | DESCRIPTION |
|---|---|
term
|
The static term to validate, together with everything nested in it.
TYPE:
|
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If a term is of a class that cannot appear in a static position. |
ValueError
|
If an application is ill-kinded, or an index constructor is applied at the wrong arity. |
Source code in src/quivers/qiec/types.py
run_structural
¶
run_structural(module: QiecModule, program: Program, name: str, arguments: Sequence[object], *, fuel: int | None = None) -> ExecutionResult
Run a structural computation through the compiled PyTorch attachments.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The checked QIEC module.
TYPE:
|
program
|
The classic compiled container supplying encoders, decoders, losses, and their learned tensors.
TYPE:
|
name
|
The structural computation name.
TYPE:
|
arguments
|
Its host arguments.
TYPE:
|
fuel
|
Optional reference-machine step budget.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ExecutionResult
|
The typed result and trace. Torch tensor results retain their autograd graph back to the attached component parameters. |
| RAISES | DESCRIPTION |
|---|---|
KeyError
|
If |
Source code in src/quivers/qiec/structural_runtime.py
structural_handler_definition
¶
structural_handler_definition(effect: EffectRef, result: TypeExpr, *, instance_name: str, computation_name: str) -> HandlerDef
Build the stable checked handler signature for one neural attachment.
| PARAMETER | DESCRIPTION |
|---|---|
effect
|
The applied
TYPE:
|
result
|
The closed result type returned by the host component.
TYPE:
|
instance_name
|
The source-derived effect-instance name.
TYPE:
|
computation_name
|
The source-derived structural computation name.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
HandlerDef
|
A stable foreign handler declaration for the component. |
Source code in src/quivers/qiec/structural_runtime.py
structural_runtime_configuration
¶
structural_runtime_configuration(module: QiecModule, program: Program) -> RuntimeConfiguration
Return the standard runtime configuration for structural entries.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The checked QIEC module whose structural entries may be invoked.
TYPE:
|
program
|
The compiled container supplying their PyTorch attachments.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
RuntimeConfiguration
|
A configuration selecting the structural provider when the module has structural runtimes, or no providers otherwise. |
Source code in src/quivers/qiec/structural_runtime.py
structural_runtime_provider
¶
structural_runtime_provider(module: QiecModule, program: Program) -> StructuralRuntimeProvider
Build the typed neural-attachment provider for a compiled module.
| PARAMETER | DESCRIPTION |
|---|---|
module
|
The checked QIEC module whose structural instances need handlers.
TYPE:
|
program
|
The compiled container supplying the corresponding PyTorch objects.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
StructuralRuntimeProvider
|
A provider containing one validated runtime handler per structural instance. |
| RAISES | DESCRIPTION |
|---|---|
TypeError
|
If a structural component returns a type with no host validator. |