Module

Serializable whole-module containers.

module

Serializable, whole-module containers for the QIEC kernel.

The small records in this module are the boundary returned by source-language extension lowerers. They contain declarations and checked computation graphs, but never parser nodes, compiler objects, callbacks, or backend-specific data.

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: str
entry	The allocated instance and its interface application. TYPE: RowEntry
origin	Where the instance was declared. TYPE: SourceOrigin

__post_init__

__post_init__() -> None

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

def __post_init__(self) -> None:
    """Reject an unnamed instance.

    Raises
    ------
    ValueError
        If the source name is empty. The name is how a request
        resolves to this instance, so an empty one names nothing.
    """
    if not self.name:
        raise ValueError("an effect instance name cannot be empty")

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: ComputationId
name	The display name; must be non-empty and unique within the module. TYPE: str
telescope	The static parameters the computation abstracts over, in order. TYPE: Telescope
parameters	The value parameters, in order; their names must be distinct and must not reuse a telescope binder's name. TYPE: tuple[Local, ...]
body	The computation's body, with the parameters in scope. TYPE: Computation
type	The checked effect row and result type of body. TYPE: ComputationType
origin	Where the computation was declared. TYPE: SourceOrigin

__post_init__

__post_init__() -> None

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

def __post_init__(self) -> None:
    """Reject a computation whose names collide or are absent.

    Raises
    ------
    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.
    """
    if not self.name:
        raise ValueError("a computation name cannot be empty")
    validate_telescope(self.telescope)
    static_names = {binder.name for binder in self.telescope}
    local_names = [parameter.name for parameter in self.parameters]
    if len(set(local_names)) != len(local_names):
        raise ValueError(f"duplicate parameter in computation {self.name!r}")
    overlap = static_names & set(local_names)
    if overlap:
        raise ValueError(
            f"computation {self.name!r} reuses static names as parameters: "
            f"{sorted(overlap)!r}"
        )

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: str
source_protocol	The source route that produced the module. TYPE: str
index_sorts	The user-defined closed index sorts. TYPE: tuple[UserIndexSort, ...] DEFAULT: ()
families	The indexed data families. TYPE: tuple[FamilyDecl, ...] DEFAULT: ()
constructors	The family constructors. TYPE: tuple[ConstructorDecl, ...] DEFAULT: ()
effects	The effect interfaces. TYPE: tuple[EffectDef, ...] DEFAULT: ()
instances	The module-scoped named effect instances. TYPE: tuple[NamedEffectInstance, ...] DEFAULT: ()
handlers	The handler declarations. TYPE: tuple[HandlerDef, ...] DEFAULT: ()
computations	The named computations. TYPE: tuple[NamedComputation, ...] DEFAULT: ()
entries	The program entry points, each naming one of the computations. TYPE: tuple[ProgramEntry, ...] DEFAULT: ()
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: str DEFAULT: ''
abi	The kernel ABI the module is expressed against; must equal :data:QIEC_ABI. TYPE: str DEFAULT: QIEC_ABI

__post_init__

__post_init__() -> None

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

def __post_init__(self) -> None:
    """Reject a module whose identity or ABI is missing or wrong.

    Raises
    ------
    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.
    """
    if not isinstance(self.module, str) or not self.module:
        raise ValueError("a QIEC module name cannot be empty")
    if not isinstance(self.source_protocol, str) or not self.source_protocol:
        raise ValueError("a QIEC source protocol cannot be empty")
    if self.abi != QIEC_ABI:
        raise ValueError(f"QIEC module ABI must be {QIEC_ABI!r}")
    _require_unique(
        (sort.name for sort in self.index_sorts),
        subject="index sort name",
    )
    _require_unique((family.id for family in self.families), subject="family ID")
    _require_unique(
        (family.name for family in self.families), subject="family name"
    )
    _require_unique(
        (constructor.id for constructor in self.constructors),
        subject="constructor ID",
    )
    _require_unique((effect.ref.id for effect in self.effects), subject="effect ID")
    _require_unique(
        (effect.ref.name for effect in self.effects), subject="effect name"
    )
    _require_unique(
        (instance.entry.instance for instance in self.instances),
        subject="effect-instance ID",
    )
    _require_unique(
        (instance.name for instance in self.instances),
        subject="effect-instance name",
    )
    _require_unique((handler.id for handler in self.handlers), subject="handler ID")
    _require_unique(
        (handler.name for handler in self.handlers), subject="handler name"
    )
    _require_unique(
        (computation.name for computation in self.computations),
        subject="computation name",
    )

    declared_constructors = {
        constructor.id: constructor for constructor in self.constructors
    }
    family_ids = {family.id for family in self.families}
    expected_constructor_ids = {
        constructor
        for family in self.families
        for constructor in family.constructors
    }
    if set(declared_constructors) != expected_constructor_ids:
        raise ValueError(
            "module constructors must exactly match the constructors named by families"
        )
    if any(
        constructor.family not in family_ids
        for constructor in declared_constructors.values()
    ):
        raise ValueError("a module constructor names an unknown family")

    effect_ids = {effect.ref.id for effect in self.effects}
    if any(
        instance.entry.effect.id not in effect_ids for instance in self.instances
    ):
        raise ValueError("an effect instance names an unknown interface")
    if any(handler.effect.id not in effect_ids for handler in self.handlers):
        raise ValueError("a handler names an unknown effect interface")
    for item in (*self.instances, *self.computations):
        if item.origin.module != self.module:
            raise ValueError("source origin belongs to another QIEC module")
        if item.origin.source_protocol != self.source_protocol:
            raise ValueError("source origin uses another source protocol")

called_computations

called_computations(body: Computation) -> frozenset[ComputationId]

The computations a body calls, directly.

PARAMETER	DESCRIPTION
body	The body to walk. TYPE: Computation

RETURNS	DESCRIPTION
frozenset[ComputationId]	The callee of every Call in the body, at any depth.

Source code in src/quivers/qiec/module.py

def called_computations(body: Computation) -> frozenset[ComputationId]:
    """The computations a body calls, directly.

    Parameters
    ----------
    body : Computation
        The body to walk.

    Returns
    -------
    frozenset[ComputationId]
        The callee of every ``Call`` in the body, at any depth.
    """
    found: set[ComputationId] = set()
    pending: list[Computation] = [body]
    while pending:
        term = pending.pop()
        if isinstance(term, Call):
            found.add(term.callee)
        elif isinstance(term, Bind):
            pending.append(term.then)
            pending.append(term.first)
        elif isinstance(term, Handle):
            pending.append(term.computation)
        elif isinstance(term, Case):
            pending.extend(branch.body for branch in term.branches)
        elif isinstance(term, If):
            pending.append(term.otherwise)
            pending.append(term.then)
        elif isinstance(term, NewInstance):
            pending.append(term.body)
    return frozenset(found)

program_computations

program_computations(module: QiecModule) -> frozenset[ComputationId]

The computations that hold programs and their own helpers.

PARAMETER	DESCRIPTION
module	The module. TYPE: QiecModule

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

def program_computations(module: QiecModule) -> frozenset[ComputationId]:
    """The computations that hold programs and their own helpers.

    Parameters
    ----------
    module : QiecModule
        The module.

    Returns
    -------
    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.
    """
    entries = {entry.computation for entry in module.entries}
    return frozenset(
        computation.id
        for computation in module.computations
        if computation.id in entries
        or computation.origin.structural_path[:1] == ("programs",)
    )

reachable_computations

reachable_computations(module: QiecModule) -> frozenset[ComputationId]

The computations a program reaches.

PARAMETER	DESCRIPTION
module	The module. TYPE: QiecModule

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

def reachable_computations(module: QiecModule) -> frozenset[ComputationId]:
    """The computations a program reaches.

    Parameters
    ----------
    module : QiecModule
        The module.

    Returns
    -------
    frozenset[ComputationId]
        The identity of every entry point's computation and of every
        computation it calls, transitively.
    """
    by_id = {computation.id: computation for computation in module.computations}
    found: set[ComputationId] = set()
    pending = [entry.computation for entry in module.entries]
    while pending:
        identity = pending.pop()
        if identity in found or identity not in by_id:
            continue
        found.add(identity)
        pending.extend(called_computations(by_id[identity].body))
    return frozenset(found)

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: QiecModule

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

def 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.

    Parameters
    ----------
    module : QiecModule
        The lowered module to recheck.

    Returns
    -------
    KernelRegistry
        The registry resolved from the module's declarations, for a
        caller that wants to check further terms against it.

    Raises
    ------
    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.
    """

    if module.abi != QIEC_ABI:
        raise KernelError(f"unsupported QIEC ABI {module.abi!r}")
    _validate_index_sorts(module)
    registry = KernelRegistry()
    for family in module.families:
        registry.register_family(family)
    for constructor in module.constructors:
        registry.register_constructor(constructor)
    for effect in module.effects:
        registry.register_effect(effect)
    for instance in module.instances:
        _validate_closed_effect_instance(instance)
        registry.validate_static(instance.entry.effect)
        declared = registry.effects.get(instance.entry.effect.id)
        if declared is None or not declared.matches(instance.entry.effect):
            raise KernelError(
                f"unknown effect interface for instance {instance.name!r}"
            )
        registry.instance_names[instance.entry.instance] = instance.name
    # Every computation signature is registered before any body is
    # rechecked, for the same reason the lowerer collects them first: a
    # body may call a computation declared after it, and two may call
    # each other.
    for computation in module.computations:
        registry.register_computation(
            ComputationSignature(
                computation.id,
                computation.name,
                computation.telescope,
                tuple(parameter.type for parameter in computation.parameters),
                computation.type.result,
                computation.type.effects,
            )
        )
    for handler in module.handlers:
        registry.register_handler(handler)
    instance_interfaces = {
        instance.entry.instance: instance.entry.effect for instance in module.instances
    }
    for handler in module.handlers:
        _validate_effect_instances(
            handler.introduced,
            instance_interfaces,
            subject=f"handler {handler.name!r}",
            module=module.module,
            source_protocol=module.source_protocol,
        )
    for computation in module.computations:
        _validate_named_static_scope(computation, computation.telescope)
        registry.validate_computation_type(computation.type)
        _validate_effect_instances(
            computation.type.effects,
            instance_interfaces,
            subject=f"declared row of computation {computation.name!r}",
            module=module.module,
            source_protocol=module.source_protocol,
        )
        _validate_effect_instances(
            computation.body,
            instance_interfaces,
            subject=f"body of computation {computation.name!r}",
            module=module.module,
            source_protocol=module.source_protocol,
        )
        context = CheckContext()
        for parameter in computation.parameters:
            registry.validate_type(parameter.type)
            context = context.extend(parameter)
        actual = infer_computation(computation.body, registry, context)
        if not computation_type_conforms(actual, computation.type):
            raise KernelError(
                f"computation {computation.name!r} has type "
                f"{render_computation_type(actual, registry.instance_names)}, "
                f"not declared type "
                f"{render_computation_type(computation.type, registry.instance_names)}"
            )
    return registry

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: ComputationType
names	The source name of each lexical instance, for the row. TYPE: Mapping[EffectInstanceId, str] | None DEFAULT: None

RETURNS	DESCRIPTION
str	Result !{row}.

Source code in src/quivers/qiec/module.py

def render_computation_type(
    type_: ComputationType, names: Mapping[EffectInstanceId, str] | None = None
) -> str:
    """Render a computation type as its result and row.

    Parameters
    ----------
    type_ : ComputationType
        The type.
    names : Mapping[EffectInstanceId, str] | None
        The source name of each lexical instance, for the row.

    Returns
    -------
    str
        ``Result !{row}``.
    """
    return f"{render_static(type_.result)} {render_row(type_.effects, names)}"

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: QiecModule
registry	The registry validate_module resolved for it. TYPE: KernelRegistry
name	The computation's name. TYPE: str

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

def inferred_computation_type(
    module: QiecModule, registry: KernelRegistry, name: str
) -> ComputationType:
    """The type a named computation's body has, as the checker infers it.

    Parameters
    ----------
    module : QiecModule
        The module, already validated.
    registry : KernelRegistry
        The registry `validate_module` resolved for it.
    name : str
        The computation's name.

    Returns
    -------
    ComputationType
        The inferred result type and the row the body performs, which the
        declared row may widen.

    Raises
    ------
    KeyError
        If the module has no computation of that name.
    """
    computation = next(
        (item for item in module.computations if item.name == name), None
    )
    if computation is None:
        raise KeyError(f"module {module.module!r} has no computation {name!r}")
    context = CheckContext()
    for parameter in computation.parameters:
        context = context.extend(parameter)
    return infer_computation(computation.body, registry, context)

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: ComputationType
declared	The type the declaration states. TYPE: ComputationType

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

def 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.

    Parameters
    ----------
    actual : ComputationType
        The type inferred from the body.
    declared : ComputationType
        The type the declaration states.

    Returns
    -------
    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.
    """

    if actual.result != declared.result:
        return False
    if declared.effects.tail is None:
        return actual.effects == declared.effects
    actual_entries = {entry.instance: entry.effect for entry in actual.effects.entries}
    declared_entries = {
        entry.instance: entry.effect for entry in declared.effects.entries
    }
    for instance, effect in actual_entries.items():
        expected = declared_entries.get(instance)
        if expected is not None:
            if expected != effect:
                return False
            continue
        if declared.effects.tail.proves_lacks(instance):
            return False
    if actual.effects.tail is None:
        return True
    forbidden = set(declared.effects.tail.lacks) - set(declared_entries)
    if any(instance in actual_entries for instance in forbidden):
        return False
    if any(not actual.effects.tail.proves_lacks(instance) for instance in forbidden):
        return False
    return True