Signatures

Multi-sorted algebra signatures with constructors, typed binders, and (optionally) vertex / edge kinds for graph-shaped signatures. The runtime carrier for signature { … } DSL declarations.

The de-Bruijn discipline is enforced structurally: a BoundVar(i) term carries an integer index; binders push a fresh ContextEntry(var_sort, embedding, type_term) onto an implicit context Γ tracked by the encoder / decoder runtime. Binder variables may carry an annotation sort : the variable's type is stored alongside its embedding in Γ.

signature

Signatures: typed multi-sorted algebras with binders.

A Signature is the runtime form of a signature { … } DSL declaration. It carries the sort table, constructor table, binder table, and (for graph-shaped signatures) vertex / edge kind tables.

Terms over a signature are first-class Python values (Term instances): each carries the constructor / binder name and its positional arguments. The framework's encoder and decoder runtimes walk these records uniformly.

The de-Bruijn discipline is enforced structurally: a BoundVar term carries an integer index; binders push a fresh entry onto an implicit context Γ tracked by the encoder / decoder runtime.

All structured value types in this module are didactic didactic.api.Model records, matching the quivers convention for schema-bearing data; the only fields held opaque are runtime-only artefacts that don't round-trip (torch tensors, arbitrary Python data leaves).

SortVocabEntry

Bases: Model

One closed-vocabulary entry on a data sort.

Each entry is a tagged Python value: kind is the leaf type ("string" | "integer" | "float"), value is the decoded Python value (str, int, or float).

Sort

Bases: Model

A sort declaration: name, kind, optional dim, optional closed vocabulary.

A data sort may carry a vocab tuple of SortVocabEntry records. Object / index sorts must have an empty vocab (the framework checks at runtime).

vocab_values property

vocab_values: tuple[DataLeaf, ...]

The decoded Python values in declaration order.

Constructor

Bases: Model

A typed constructor symbol.

BinderVarSpec

Bases: Model

A scoped variable introduced by a binder.

sort is the variable's own sort. annot_sort is the sort of an optional type annotation — a sibling argument in the enclosing Term that travels alongside the variable's embedding in Γ. Used to track per-variable type information.

BinderArgSpec

Bases: Model

A scoped argument of a binder.

Binder

Bases: Model

A binder constructor: introduces variables of given sorts into the scope of given arguments.

domain

domain() -> tuple[str, ...]

Positional sort sequence of the binder's arguments in the enclosing Term: type-annotations for each annotated bound variable (in declaration order, outer-context-evaluated), followed by the scoped arguments (extended-context-evaluated).

Source code in src/quivers/structural/signature.py

def domain(self) -> tuple[str, ...]:
    """Positional sort sequence of the binder's arguments in the
    enclosing `Term`: type-annotations for each annotated
    bound variable (in declaration order, outer-context-evaluated),
    followed by the scoped arguments (extended-context-evaluated).
    """
    return tuple(
        b.annot_sort for b in self.binds if b.annot_sort is not None
    ) + tuple(a.sort for a in self.scoped)

VertexKind

Bases: Model

A vertex kind in a graph-shaped signature.

EdgeKind

Bases: Model

An edge kind in a graph-shaped signature.

Signature

Bases: Model

A multi-sorted algebra signature with optional binders / graph structure.

Sort, constructor, binder, vertex_kind and edge_kind tables are represented as tuples of records (rather than dicts) so the enclosing dx.Model keeps a schema-bearing layout. The runtime exposes O(1) name-keyed lookup methods (sort(name), constructor(name), etc.) on top of those tuples.

Term

Bases: Model

A closed term over a signature.

op is the constructor name, the binder name, or the framework-reserved "BoundVar" for a de-Bruijn variable reference.

args are positional children. Object positions carry a Term; data positions carry a DataLeaf raw value; index positions carry a non-negative int. args is held opaque (its element type is the open union TermArg); the encoder / decoder enforce sort agreement structurally at use time.

No wrapping such as Term("Data", …) is used at any position; raw values appear directly at data positions.

to_tuple

to_tuple() -> tuple

A serialisable form matching the agenda's item-tuple convention: (op, *args_serialised). Children that are Terms are recursively serialised; data leaves and indices pass through.

Source code in src/quivers/structural/signature.py

def to_tuple(self) -> tuple:
    """A serialisable form matching the agenda's item-tuple
    convention: ``(op, *args_serialised)``. Children that are
    `Term`s are recursively serialised; data leaves and
    indices pass through."""
    out: list = [self.op]
    for a in self.args:
        if isinstance(a, Term):
            out.append(a.to_tuple())
        else:
            out.append(a)
    return tuple(out)

ContextEntry dataclass

ContextEntry(var_sort: str, embedding: Tensor, type_term: Term | None = None)

One scope entry on the binder stack.

embedding is a runtime tensor; type_term is the binder's annotation term captured at scope-extension time.

Context dataclass

Context(entries: tuple[ContextEntry, ...] = ())

The de-Bruijn scope context threaded through encoder and decoder runtimes.

Position 0 is the most recently bound variable; lookup var(i) returns the i-th entry from the top.

by_sort

by_sort(sort: str) -> list[tuple[int, ContextEntry]]

All entries whose var_sort matches; returned as (depth-index, entry) pairs for the decoder's categorical-over-in-scope-variables.

Source code in src/quivers/structural/signature.py

def by_sort(self, sort: str) -> list[tuple[int, ContextEntry]]:
    """All entries whose ``var_sort`` matches; returned as
    ``(depth-index, entry)`` pairs for the decoder's
    categorical-over-in-scope-variables."""
    return [(i, e) for i, e in enumerate(self.entries) if e.var_sort == sort]

bound_var

bound_var(index: int) -> Term

A de-Bruijn variable reference.

Source code in src/quivers/structural/signature.py

def bound_var(index: int) -> Term:
    """A de-Bruijn variable reference."""
    if not isinstance(index, int) or index < 0:
        raise TypeError(f"bound_var requires a non-negative int, got {index!r}")
    return Term(op="BoundVar", args=(index,))

make_term

make_term(op: str, *args) -> Term

Construct a term over a signature.

Each arg must be a Term, a DataLeaf raw value, or a non-negative int (for index-sorted positions). The encoder / decoder runtime validate sort agreement at use time.

Source code in src/quivers/structural/signature.py

def make_term(op: str, *args) -> Term:
    """Construct a term over a signature.

    Each ``arg`` must be a `Term`, a `DataLeaf` raw
    value, or a non-negative int (for index-sorted positions). The
    encoder / decoder runtime validate sort agreement at use
    time.
    """
    if not isinstance(op, str):
        raise TypeError(f"make_term requires a string op, got {type(op).__name__}")
    return Term(op=op, args=tuple(args))