Effects

Typed effect interfaces, lexical rows, and handler signatures.

effects

Typed effect interfaces, lexical rows, and handler signatures for QIEC.

EMPTY_ROW module-attribute

EMPTY_ROW = EffectRow()

The row of a computation that performs no effects.

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: str
identity	Stable identity. Equality and hashing are taken from this rather than from name, so renaming for readability cannot silently split one variable into two. TYPE: RowVariableId
lacks	Instances the tail is proven not to contain. Sorted at construction, so equality is insensitive to the order given. TYPE: tuple[EffectInstanceId, ...] DEFAULT: ()

__post_init__

__post_init__() -> None

Sort the lacks constraints and reject a malformed variable.

RAISES	DESCRIPTION
ValueError	If name is empty, or lacks names one instance twice.

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

def __post_init__(self) -> None:
    """Sort the lacks constraints and reject a malformed variable.

    Raises
    ------
    ValueError
        If `name` is empty, or `lacks` names one instance twice.
    """
    if not self.name:
        raise ValueError("row variable name cannot be empty")
    ordered = tuple(sorted(self.lacks, key=str))
    if len(set(ordered)) != len(ordered):
        raise ValueError("a row lacks constraint cannot repeat an instance")
    object.__setattr__(self, "lacks", ordered)

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

RETURNS	DESCRIPTION
bool	True when the constraint is carried, which is what permits an explicit entry for instance to sit beside this tail.

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

def proves_lacks(self, instance: EffectInstanceId) -> bool:
    """Whether this tail is known not to contain `instance`.

    Parameters
    ----------
    instance : EffectInstanceId
        The lexical instance to test.

    Returns
    -------
    bool
        True when the constraint is carried, which is what permits an
        explicit entry for `instance` to sit beside this tail.
    """
    return instance in self.lacks

__eq__

__eq__(other: object) -> bool

Compare by identity and constraints, ignoring the display name.

PARAMETER	DESCRIPTION
other	The value to compare against. TYPE: object

RETURNS	DESCRIPTION
bool	True when other is a row variable with the same identity and the same lacks constraints.

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

def __eq__(self, other: object) -> bool:
    """Compare by identity and constraints, ignoring the display name.

    Parameters
    ----------
    other : object
        The value to compare against.

    Returns
    -------
    bool
        True when `other` is a row variable with the same identity and
        the same lacks constraints.
    """
    return (
        isinstance(other, RowVariable)
        and self.identity == other.identity
        and self.lacks == other.lacks
    )

__hash__

__hash__() -> int

Hash the fields that __eq__ compares.

RETURNS	DESCRIPTION
int	A hash of the identity and the lacks constraints.

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

def __hash__(self) -> int:
    """Hash the fields that `__eq__` compares.

    Returns
    -------
    int
        A hash of the identity and the lacks constraints.
    """
    return hash((self.identity, self.lacks))

merge

merge(other: RowVariable) -> RowVariable

Unify two occurrences, accumulating their lacks constraints.

PARAMETER	DESCRIPTION
other	Another occurrence of the same variable. TYPE: RowVariable

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

def merge(self, other: RowVariable) -> RowVariable:
    """Unify two occurrences, accumulating their lacks constraints.

    Parameters
    ----------
    other : RowVariable
        Another occurrence of the same variable.

    Returns
    -------
    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
    ------
    ValueError
        If the two variables have different identities, and so are not
        occurrences of one variable at all.
    """
    if self.identity != other.identity:
        raise ValueError("cannot unify distinct row variables")
    merged = tuple(sorted(set((*self.lacks, *other.lacks)), key=str))
    return RowVariable(self.name, self.identity, merged)

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: tuple[EffectInstanceId, ...]

RETURNS	DESCRIPTION
RowVariable	A variable of the same identity carrying the wider constraint.

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

def with_lacks(self, instances: tuple[EffectInstanceId, ...]) -> RowVariable:
    """Return this variable with further instances excluded.

    Parameters
    ----------
    instances : tuple[EffectInstanceId, ...]
        Instances to add to the constraint set. Instances already
        excluded are absorbed rather than repeated.

    Returns
    -------
    RowVariable
        A variable of the same identity carrying the wider constraint.
    """
    merged = tuple(sorted(set((*self.lacks, *instances)), key=str))
    return RowVariable(self.name, self.identity, merged)

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 effect is the row's key. TYPE: EffectInstanceId
effect	The saturated interface application the instance implements. TYPE: EffectRef

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: tuple[RowEntry, ...] DEFAULT: ()
tail	A row variable standing for further entries, or None for a closed row. An open row's tail must prove it lacks every explicit entry. TYPE: RowVariable | None DEFAULT: None

__post_init__

__post_init__() -> None

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

def __post_init__(self) -> None:
    """Sort the entries and reject a row that cannot be well formed.

    Raises
    ------
    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.
    """
    ordered = tuple(sorted(self.entries, key=lambda entry: str(entry.instance)))
    instances = [entry.instance for entry in ordered]
    if len(set(instances)) != len(instances):
        raise ValueError("an effect row cannot contain a lexical instance twice")
    if self.tail is not None:
        unconstrained = [
            instance
            for instance in instances
            if not self.tail.proves_lacks(instance)
        ]
        if unconstrained:
            raise ValueError(
                "an open row must prove its tail lacks every explicit instance"
            )
    object.__setattr__(self, "entries", ordered)

lookup

lookup(instance: EffectInstanceId) -> EffectRef | None

The interface an instance implements in this row.

PARAMETER	DESCRIPTION
instance	The lexical instance to resolve. TYPE: EffectInstanceId

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

def lookup(self, instance: EffectInstanceId) -> EffectRef | None:
    """The interface an instance implements in this row.

    Parameters
    ----------
    instance : EffectInstanceId
        The lexical instance to resolve.

    Returns
    -------
    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.
    """
    return next(
        (entry.effect for entry in self.entries if entry.instance == instance),
        None,
    )

contains

contains(instance: EffectInstanceId) -> bool

Whether the row carries an explicit entry for an instance.

PARAMETER	DESCRIPTION
instance	The lexical instance to test. TYPE: EffectInstanceId

RETURNS	DESCRIPTION
bool	True when an explicit entry names the instance.

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

def contains(self, instance: EffectInstanceId) -> bool:
    """Whether the row carries an explicit entry for an instance.

    Parameters
    ----------
    instance : EffectInstanceId
        The lexical instance to test.

    Returns
    -------
    bool
        True when an explicit entry names the instance.
    """
    return self.lookup(instance) is not None

add

add(entry: RowEntry) -> EffectRow

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

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 __post_init__ enforces.

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

def add(self, entry: RowEntry) -> EffectRow:
    """Return this row extended with one entry.

    Parameters
    ----------
    entry : RowEntry
        The instance and interface to add. Re-adding an entry the row
        already carries returns the row unchanged, so the operation is
        idempotent.

    Returns
    -------
    EffectRow
        The extended row. When the row is open, its tail gains a lacks
        constraint for the new instance, which keeps the invariant
        `__post_init__` enforces.

    Raises
    ------
    ValueError
        If the row already binds this instance to a different
        interface, since one lexical instance implements one
        interface.
    """
    existing = self.lookup(entry.instance)
    if existing is not None and existing != entry.effect:
        raise ValueError("one lexical instance cannot implement two interfaces")
    if existing is not None:
        return self
    tail = self.tail
    if tail is not None and not tail.proves_lacks(entry.instance):
        tail = tail.with_lacks((entry.instance,))
    return EffectRow((*self.entries, entry), tail)

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

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

def without(self, instance: EffectInstanceId) -> EffectRow:
    """Return this row with one instance discharged.

    Parameters
    ----------
    instance : EffectInstanceId
        The lexical instance to remove, as a handler does when it
        handles every operation of that instance.

    Returns
    -------
    EffectRow
        The row without that entry, keeping the tail as it was.

    Raises
    ------
    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.
    """
    if not self.contains(instance):
        raise KeyError(str(instance))
    return EffectRow(
        tuple(entry for entry in self.entries if entry.instance != instance),
        self.tail,
    )

union

union(other: EffectRow) -> EffectRow

Union two rows, preserving a compatible open tail.

PARAMETER	DESCRIPTION
other	The row to merge in. TYPE: EffectRow

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

def union(self, other: EffectRow) -> EffectRow:
    """Union two rows, preserving a compatible open tail.

    Parameters
    ----------
    other : EffectRow
        The row to merge in.

    Returns
    -------
    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
    ------
    ValueError
        If the two rows bind one instance to different interfaces, or
        if their tails are distinct variables and so cannot merge.
    """
    if self.tail is not None and other.tail is not None:
        tail = self.tail.merge(other.tail)
    else:
        tail = self.tail or other.tail
    if tail is not None:
        tail = tail.with_lacks(
            tuple(entry.instance for entry in (*self.entries, *other.entries))
        )
    result = EffectRow(self.entries, tail)
    for entry in other.entries:
        result = result.add(entry)
    return result

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: tuple[tuple[RowVariableId, EffectRow], ...] DEFAULT: ()

__post_init__

__post_init__() -> None

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

def __post_init__(self) -> None:
    """Reject a substitution that is ambiguous or immediately cyclic.

    Raises
    ------
    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.
    """
    identities = [identity for identity, _ in self.bindings]
    if len(set(identities)) != len(identities):
        raise ValueError("duplicate row substitution binding")
    for identity, row in self.bindings:
        if row.tail is not None and row.tail.identity == identity:
            raise ValueError("recursive row substitution")

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

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

def lookup(self, variable: RowVariable) -> EffectRow | None:
    """The row a variable stands for under this substitution.

    Parameters
    ----------
    variable : RowVariable
        The variable to resolve, matched on its identity rather than
        its display name.

    Returns
    -------
    EffectRow or None
        The bound row, or None when the variable is unbound and so
        remains an open tail.
    """
    return next(
        (row for identity, row in self.bindings if identity == variable.identity),
        None,
    )

apply

apply(row: EffectRow) -> EffectRow

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

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

def apply(self, row: EffectRow) -> EffectRow:
    """Replace this row's tail, and any tail it resolves to.

    Parameters
    ----------
    row : EffectRow
        The row to substitute into. A closed row is returned as is.

    Returns
    -------
    EffectRow
        The row with its tail resolved as far as the bindings reach.

    Raises
    ------
    ValueError
        If the bindings are cyclic, or if resolving a tail would
        introduce an instance that tail was proven to lack.
    """
    return self._apply(row, frozenset())

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: EffectRow
substitution	The bindings that carry each input row to row. Empty when the rows already agreed. TYPE: RowSubstitution DEFAULT: RowSubstitution()

ComputationType dataclass

ComputationType(effects: EffectRow, result: TypeExpr)

The type of a computation: its effect row and result type.

PARAMETER	DESCRIPTION
effects	The row of effect instances the computation may perform. TYPE: EffectRow
result	The type of the value it returns. TYPE: TypeExpr

ArgumentDef dataclass

ArgumentDef(name: str, type: TypeExpr)

One named, typed value argument of an operation.

PARAMETER	DESCRIPTION
name	The argument's display name. TYPE: str
type	The argument's type, which may mention the operation's telescope. TYPE: TypeExpr

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: OperationId
name	Source name, as written in the effect declaration. TYPE: str
telescope	Static binders this operation introduces on top of the interface's own. They may not shadow the interface binders. TYPE: Telescope
arguments	Value arguments the request carries, named uniquely. TYPE: tuple[ArgumentDef, ...]
result_type	What resuming the request supplies, possibly mentioning the binders above. TYPE: TypeExpr

__post_init__

__post_init__() -> None

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

def __post_init__(self) -> None:
    """Validate the telescope and the argument names.

    Raises
    ------
    ValueError
        If the telescope is malformed, or two arguments share a name.
    """
    validate_telescope(self.telescope)
    names = [argument.name for argument in self.arguments]
    if len(set(names)) != len(names):
        raise ValueError(f"duplicate argument in operation {self.name!r}")

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: EffectRef
telescope	Static binders the interface takes. TYPE: Telescope
operations	The declared operations, unique by both identity and name. TYPE: tuple[OperationDef, ...]

__post_init__

__post_init__() -> None

Validate the declaration against its operations.

RAISES	DESCRIPTION
ValueError	If the telescope is malformed, if ref is saturated, if two operations share an identity or a name, or if an operation's telescope shadows an interface binder. Shadowing is rejected rather than resolved so that a binder in an operation signature always denotes the one thing.

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

def __post_init__(self) -> None:
    """Validate the declaration against its operations.

    Raises
    ------
    ValueError
        If the telescope is malformed, if `ref` is saturated, if two
        operations share an identity or a name, or if an operation's
        telescope shadows an interface binder. Shadowing is rejected
        rather than resolved so that a binder in an operation
        signature always denotes the one thing.
    """
    validate_telescope(self.telescope)
    if self.ref.arguments:
        raise ValueError("an effect declaration ref must be unsaturated")
    ids = [operation.id for operation in self.operations]
    names = [operation.name for operation in self.operations]
    if len(set(ids)) != len(ids):
        raise ValueError(f"duplicate operation ID in effect {self.ref.name!r}")
    if len(set(names)) != len(names):
        raise ValueError(f"duplicate operation name in effect {self.ref.name!r}")
    interface_names = {binder.name for binder in self.telescope}
    for operation in self.operations:
        overlap = interface_names & {binder.name for binder in operation.telescope}
        if overlap:
            raise ValueError(
                f"operation {operation.name!r} shadows interface binders: {overlap!r}"
            )

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: tuple[StaticArgument, ...]

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

def apply(self, arguments: tuple[StaticArgument, ...]) -> EffectRef:
    """Instantiate the interface telescope as a concrete effect.

    Parameters
    ----------
    arguments : tuple[StaticArgument, ...]
        Static arguments to saturate the telescope with.

    Returns
    -------
    EffectRef
        The saturated application, carrying this declaration's
        identity together with the arguments given.

    Raises
    ------
    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.
    """
    check_static_arguments(self.telescope, arguments)
    return EffectRef(
        self.ref.id,
        self.ref.name,
        arguments,
    )

matches

matches(effect: EffectRef) -> bool

Whether a concrete effect is a well-kinded application here.

PARAMETER	DESCRIPTION
effect	The saturated application to test. TYPE: EffectRef

RETURNS	DESCRIPTION
bool	True when effect names this declaration and its arguments saturate the telescope. False rather than raising, so callers can test candidates; use apply when the reason matters.

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

def matches(self, effect: EffectRef) -> bool:
    """Whether a concrete effect is a well-kinded application here.

    Parameters
    ----------
    effect : EffectRef
        The saturated application to test.

    Returns
    -------
    bool
        True when `effect` names this declaration and its arguments
        saturate the telescope. False rather than raising, so callers
        can test candidates; use `apply` when the reason matters.
    """
    if effect.id != self.ref.id:
        return False
    try:
        self.apply(effect.arguments)
    except TypeError, ValueError:
        return False
    return True

operation

operation(operation: OperationId) -> OperationDef

The declared operation with a given identity.

PARAMETER	DESCRIPTION
operation	The identity to resolve. TYPE: OperationId

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

def operation(self, operation: OperationId) -> OperationDef:
    """The declared operation with a given identity.

    Parameters
    ----------
    operation : OperationId
        The identity to resolve.

    Returns
    -------
    OperationDef
        The matching declaration.

    Raises
    ------
    KeyError
        If this interface declares no such operation, which is how a
        request naming an operation another effect owns is caught.
    """
    for candidate in self.operations:
        if candidate.id == operation:
            return candidate
    raise KeyError(str(operation))

ResumptionGrade

Bases: str, Enum

Quantitative use allowed for a handler-clause resumption.

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: OperationId
grade	How often the clause may invoke its continuation. The grade is part of the clause contract and is checked against the body. TYPE: ResumptionGrade
parameters	Binders for the operation's value arguments, in declaration order. The body refers to the request's arguments through these. TYPE: tuple[Local, ...] DEFAULT: ()
body	What the clause does. None is a signature rather than an implementation, and is legal only for a handler whose implementation is supplied at runtime. An absent body never means "look up a callback": the declaration has to say so. TYPE: Computation or None DEFAULT: None

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: Local
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: Computation

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: HandlerId
name	The handler's display name. TYPE: str
effect	The interface application the handler handles. TYPE: EffectRef
clauses	One clause per operation the handler covers. TYPE: tuple[HandlerClauseDef, ...]
input_type	The result type of the computation the handler accepts. TYPE: TypeExpr
output_type	The type of the handler's answer. TYPE: TypeExpr
introduced	The effects the handler's own clauses perform, which the residual row of a handled computation gains. TYPE: EffectRow DEFAULT: EMPTY_ROW
total	Whether the clauses cover every operation of effect. TYPE: bool DEFAULT: True
forwards_unknown	Whether an operation no clause covers is forwarded outward rather than rejected; incompatible with total. TYPE: bool DEFAULT: False
telescope	The static parameters the handler abstracts over, in order. TYPE: Telescope DEFAULT: ()
return_clause	How the handler answers the computation's return, or None to return the value unchanged. TYPE: HandlerReturnClauseDef | None DEFAULT: None
implementation	"authored" when every clause carries a body, "foreign" when none does and a runtime provider supplies the behavior. TYPE: Literal['authored', 'foreign'] DEFAULT: 'foreign'

__post_init__

__post_init__() -> None

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

def __post_init__(self) -> None:
    """Validate the clause set against the coverage claim.

    Raises
    ------
    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.
    """
    validate_telescope(self.telescope)
    operations = [clause.operation for clause in self.clauses]
    if len(set(operations)) != len(operations):
        raise ValueError(f"duplicate clause in handler {self.name!r}")
    if self.total and self.forwards_unknown:
        raise ValueError("a handler cannot be both total and forwarding")
    authored = self.implementation == "authored"
    missing = [clause.operation for clause in self.clauses if clause.body is None]
    if authored and missing:
        raise ValueError(
            f"authored handler {self.name!r} has clauses without a body: "
            f"{missing!r}; write the bodies, or declare the handler "
            f"foreign if its behavior comes from a runtime provider"
        )
    supplied = [
        clause.operation for clause in self.clauses if clause.body is not None
    ]
    if not authored and supplied:
        raise ValueError(
            f"foreign handler {self.name!r} carries authored clause bodies: "
            f"{supplied!r}; a foreign handler's behavior comes from its "
            f"runtime provider, so a body here would be ignored"
        )
    if not authored and self.return_clause is not None:
        raise ValueError(
            f"foreign handler {self.name!r} carries a return clause; its "
            f"answer comes from its runtime provider"
        )

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

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

def clause(self, operation: OperationId) -> HandlerClauseDef | None:
    """The clause covering an operation, if this handler has one.

    Parameters
    ----------
    operation : OperationId
        The operation to look for.

    Returns
    -------
    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.
    """
    return next(
        (clause for clause in self.clauses if clause.operation == operation),
        None,
    )

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: EffectInstanceId
effect	The instance's interface application. TYPE: EffectRef
operation	The operation requested. TYPE: OperationId
static_arguments	The operation's telescope instantiation, in binder order. TYPE: tuple[StaticArgument, ...]
arguments	The value arguments, one per operation argument. TYPE: tuple[Value, ...]
result_type	The type of the value the operation returns under the instantiation. TYPE: TypeExpr
origin	Where the request was written and how it was reached. TYPE: SiteProvenance
tag	The serialization discriminator; always "effect_request". TYPE: Literal['effect_request'] DEFAULT: 'effect_request'

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: EffectRow
right	The other row. The result does not depend on the order of the two arguments. TYPE: EffectRow

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

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

    Parameters
    ----------
    left : EffectRow
        One row to unify.
    right : EffectRow
        The other row. The result does not depend on the order of the two
        arguments.

    Returns
    -------
    RowUnification
        The common row and the substitution taking both inputs to it.

    Raises
    ------
    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.
    """
    left_entries = {entry.instance: entry.effect for entry in left.entries}
    right_entries = {entry.instance: entry.effect for entry in right.entries}
    for instance in left_entries.keys() & right_entries.keys():
        if left_entries[instance] != right_entries[instance]:
            raise ValueError("row entries disagree on an effect interface")
    left_only = tuple(
        RowEntry(instance, effect)
        for instance, effect in left_entries.items()
        if instance not in right_entries
    )
    right_only = tuple(
        RowEntry(instance, effect)
        for instance, effect in right_entries.items()
        if instance not in left_entries
    )

    if left.tail is None and right.tail is None:
        if left_only or right_only:
            raise ValueError("closed effect rows do not unify")
        return RowUnification(left)

    if left.tail is not None and right.tail is None:
        if left_only:
            raise ValueError("an open row has entries absent from the closed row")
        replacement = EffectRow(right_only)
        substitution = RowSubstitution(((left.tail.identity, replacement),))
        if substitution.apply(left) != right:
            raise ValueError("row substitution violates a lacks constraint")
        return RowUnification(right, substitution)

    if left.tail is None and right.tail is not None:
        result = unify_effect_rows(right, left)
        return RowUnification(result.row, result.substitution)

    assert left.tail is not None and right.tail is not None
    if left.tail.identity == right.tail.identity:
        if left_only or right_only:
            raise ValueError(
                "two occurrences of one row variable have incompatible entries"
            )
        tail = left.tail.merge(right.tail)
        return RowUnification(EffectRow(left.entries, tail))

    if any(entry.instance in left.tail.lacks for entry in right_only):
        raise ValueError("left row lacks an entry required by the right row")
    if any(entry.instance in right.tail.lacks for entry in left_only):
        raise ValueError("right row lacks an entry required by the left row")
    all_instances = tuple((*left_entries.keys(), *right_entries.keys()))
    fresh_identity = RowVariableId.derive(
        "unify",
        *sorted((left.tail.identity, right.tail.identity), key=str),
        *sorted(all_instances, key=str),
    )
    fresh = RowVariable(
        "unified_tail",
        fresh_identity,
        tuple(
            sorted(
                set((*left.tail.lacks, *right.tail.lacks, *all_instances)),
                key=str,
            )
        ),
    )
    left_replacement = EffectRow(right_only, fresh)
    right_replacement = EffectRow(left_only, fresh)
    substitution = RowSubstitution(
        (
            (left.tail.identity, left_replacement),
            (right.tail.identity, right_replacement),
        )
    )
    unified_entries = tuple(
        RowEntry(instance, effect)
        for instance, effect in {**left_entries, **right_entries}.items()
    )
    unified = EffectRow(unified_entries, fresh)
    if substitution.apply(left) != unified or substitution.apply(right) != unified:
        raise ValueError("row unification produced an inconsistent substitution")
    return RowUnification(unified, substitution)

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: EffectRef
module	Module the allocation occurs in. Part of the identity, so two modules allocating at the same lexical path stay distinct. TYPE: str
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: tuple[str | int, ...]

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

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

    Parameters
    ----------
    effect : EffectRef
        The saturated interface application to allocate.
    module : str
        Module the allocation occurs in. Part of the identity, so two
        modules allocating at the same lexical path stay distinct.
    lexical_path : tuple[str | int, ...]
        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.

    Returns
    -------
    RowEntry
        The fresh instance paired with the interface it implements, ready
        to add to a row.
    """
    instance = EffectInstanceId.derive(
        str(effect.id),
        effect.arguments,
        module,
        lexical_path,
    )
    return RowEntry(instance, effect)

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

RETURNS	DESCRIPTION
str	Its source name, or instance: and the first eight characters of its digest when it has none.

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

def render_instance(
    identity: EffectInstanceId, names: Mapping[EffectInstanceId, str] | None = None
) -> str:
    """Render one effect instance in the surface spelling.

    Parameters
    ----------
    identity : EffectInstanceId
        The instance.
    names : Mapping[EffectInstanceId, str] | None
        The source name of each lexical instance.

    Returns
    -------
    str
        Its source name, or ``instance:`` and the first eight characters
        of its digest when it has none.
    """
    table = names or {}
    return table.get(identity, f"instance:{identity.digest[:8]}")

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: EffectRow
names	The source name of each lexical instance; an instance with no name renders as the first eight characters of its digest. TYPE: Mapping[EffectInstanceId, str] | None DEFAULT: None

RETURNS	DESCRIPTION
str	!{a : Effect, b : Other[Int] | rho}: each entry as its instance's name and interface, in name order, and an open row's tail after a bar, with the instances it lacks after a backslash.

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

def render_row(
    row: EffectRow, names: Mapping[EffectInstanceId, str] | None = None
) -> str:
    """Render an effect row in the surface spelling.

    Parameters
    ----------
    row : EffectRow
        The row.
    names : Mapping[EffectInstanceId, str] | None
        The source name of each lexical instance; an instance with no
        name renders as the first eight characters of its digest.

    Returns
    -------
    str
        ``!{a : Effect, b : Other[Int] | rho}``: each entry as its
        instance's name and interface, in name order, and an open row's
        tail after a bar, with the instances it lacks after a backslash.
    """
    entries = ", ".join(
        sorted(
            f"{render_instance(entry.instance, names)} : {render_static(entry.effect)}"
            for entry in row.entries
        )
    )
    if row.tail is None:
        return "!{" + entries + "}"
    tail = row.tail.name
    if row.tail.lacks:
        tail += " \\ " + ", ".join(
            render_instance(item, names) for item in row.tail.lacks
        )
    return "!{" + (entries + " | " if entries else "") + tail + "}"