GADTs and indexed families

Declarations

didactic.gadt.GADT 

GADT(name: str, *, extends: Iterable[str] = ())

A complete generalized algebraic theory declaration.

GADT is a builder with a deliberate freeze point. Sorts, constructors, operations, and equations may be added until :meth:compile is called. Compilation seals the declaration, builds a panproto.Theory value, and runs Panproto's full theory typechecker before returning it.

sealed property 

sealed: bool

Whether compilation has frozen the declaration.

families property 

families: tuple[Family, ...]

Return families in declaration order.

operations property 

operations: tuple[Operation, ...]

Return operations in declaration order.

equations property 

equations: tuple[Equation, ...]

Return ordinary equations in declaration order.

definition_count property 

definition_count: int

Return the number used to derive the next definition name.

theory property 

theory: Theory

Compile once and return the cached Panproto theory.

family_named 

family_named(name: str) -> Family | None

Return the family declared under name, if any.

operation_named 

operation_named(name: str) -> Operation | None

Return the operation declared under name, if any.

sort 

sort(
    name: str,
    *,
    closed: bool = False,
    kind: JsonValue = "Structural",
) -> Family

Declare a sort with no indices: Ty = language.sort("Ty", closed=True).

An indexed sort is declared with :meth:family, whose signature carries the telescope.

family 

family(
    name: str,
    *,
    closed: bool = False,
    kind: JsonValue = "Structural",
    **parameters: InputSpec,
) -> Family

Declare an indexed sort from keyword indices.

language.family("Expr", t=Ty, closed=True) declares Expr(t : Ty). Keyword order is the telescope. A later index's sort may depend on an earlier one, as a lambda over its name::

language.family("Term", context=Context, type=lambda context: Type[context])

constructor 

constructor(
    name: str, *, returns: SortSpec, **inputs: InputSpec
) -> Operation

Declare an introduction form.

returns names the family the constructor introduces, and that family's constructor list gains the name::

language.constructor(
    "IntLit", value=El[int_code()], returns=Expr[int_code()]
)

operation 

operation(
    name: str, *, returns: SortSpec, **inputs: InputSpec
) -> Operation

Declare an ordinary operation.

language.operation("int_value", returns=El[int_code()]) declares a nullary operation producing a carrier value.

eliminator 

eliminator(
    name: str,
    *,
    returns: SortSpec,
    body: Body | None = None,
    **inputs: InputSpec,
) -> Operation

Declare an eliminator, and define it when given a body.

returns is the motive and may depend on earlier inputs. The body is a lambda over every input, in order, returning the term that defines the eliminator, usually a :func:match over one input::

language.eliminator(
    "evaluate",
    t=Ty,
    expression=lambda t: Expr[t],
    returns=lambda t: El[t],
    body=lambda t, expression: match(expression, IntLit=lambda v: v, ...),
)

Without a body the eliminator is declared only, and :meth:Operation.define supplies one later.

equation 

equation(
    name: str,
    lhs: Term,
    rhs: Term,
    *,
    directed: bool = False,
    executable: bool = False,
) -> Equation

Declare an equality or directed rewrite.

rewrite 

rewrite(name: str, lhs: Term, rhs: Term) -> Equation

Declare a directed equation used by normalization.

to_spec 

to_spec() -> JsonObject

Return the complete Panproto theory specification.

compile 

compile() -> Theory

Build and rigorously typecheck a panproto.Theory.

infer_sort 

infer_sort(
    term: Term,
    *,
    context: Mapping[str, SortExpr] | None = None,
) -> SortExpr

Infer the sort of an application, variable, let, or case term.

normalize 

normalize(term: Term, *, max_steps: int = 1000) -> Term

Normalize a symbolic term with eliminator definitions and rewrites.

didactic.gadt.Family dataclass 

Family(
    owner: GADT,
    name: str,
    parameters: tuple[Parameter, ...],
    closed: bool,
    kind: JsonValue = "Structural",
    _constructors: list[str] = _empty_constructor_names(),
)

A possibly indexed sort declaration owned by one :class:GADT.

constructors property 

constructors: tuple[str, ...]

Return constructor names in declaration order.

to_spec 

to_spec() -> JsonObject

Render this family as a Panproto sort declaration.

add_constructor 

add_constructor(name: str) -> None

Record an owner-validated constructor in declaration order.

didactic.gadt.Operation dataclass 

Operation(
    owner: GADT,
    name: str,
    inputs: tuple[Parameter, ...],
    output: SortExpr,
    role: Literal[
        "constructor", "operation", "eliminator"
    ] = "operation",
    motive: Motive | None = None,
)

A constructor, ordinary operation, or eliminator declaration.

explicit_inputs property 

explicit_inputs: tuple[Parameter, ...]

Return the arguments callers must supply in term applications.

to_spec 

to_spec() -> JsonObject

Render this operation for Panproto.

define 

define(body: Body, *, name: str | None = None) -> Equation

Define an eliminator by an oriented, typechecked equation.

body is a lambda over every input, in order, returning the defining term. It runs once with a symbolic variable per input. The equation applies the eliminator to those variables on the left and is included among the equalities sent to Panproto and among the executable reduction rules.

didactic.gadt.Parameter dataclass 

Parameter(
    name: str, sort: SortExpr, implicit: bool = False
)

One named input in a sort or operation telescope.

to_sort_param_spec 

to_sort_param_spec() -> JsonObject

Render a sort parameter for Panproto.

to_input_spec 

to_input_spec() -> JsonValue

Render an operation input for Panproto.

didactic.gadt.Implicit dataclass 

Implicit(sort: SortSpec)

An input Panproto infers from the explicit ones: n=Implicit(Nat).

The wrapped sort may itself depend on earlier inputs.

didactic.gadt.Motive dataclass 

Motive(result: SortExpr)

The result-sort expression of an eliminator.

A motive may mention any earlier eliminator input. Panproto refines those variables separately in each case branch, which is what permits branch bodies at different indices to inhabit one dependent result.

at 

at(**substitution: Term) -> SortExpr

Instantiate motive variables with concrete index terms.

didactic.gadt.Equation dataclass 

Equation(
    name: str, lhs: Term, rhs: Term, directed: bool = False
)

A named equality between terms.

to_spec 

to_spec() -> JsonObject

Render the equality for Panproto.

Terms

didactic.gadt.Term

Bases: ABC

Base class for terms in a generalized algebraic theory.

to_spec abstractmethod 

to_spec() -> JsonObject

Return Panproto's JSON-serializable representation.

substitute abstractmethod 

substitute(_substitution: Mapping[str, Term]) -> Term

Apply a capture-avoiding variable substitution.

free_vars abstractmethod 

free_vars() -> frozenset[str]

Return the names free in this term.

didactic.gadt.Var dataclass 

Var(name: str)

Bases: Term

A variable reference.

to_spec 

to_spec() -> JsonObject

Return the tagged variable record Panproto accepts.

substitute 

substitute(substitution: Mapping[str, Term]) -> Term

Replace this variable when it occurs in substitution.

free_vars 

free_vars() -> frozenset[str]

Return this variable as the sole free name.

didactic.gadt.App dataclass 

App(op: str, args: tuple[Term, ...] = ())

Bases: Term

An operation applied to zero or more argument terms.

to_spec 

to_spec() -> JsonObject

Return the tagged application record Panproto accepts.

substitute 

substitute(substitution: Mapping[str, Term]) -> Term

Substitute recursively through the arguments.

free_vars 

free_vars() -> frozenset[str]

Return the union of the arguments' free variables.

didactic.gadt.Hole dataclass 

Hole(name: str | None = None)

Bases: Term

A typed hole reported by Panproto during theory checking.

to_spec 

to_spec() -> JsonObject

Return the tagged hole record Panproto accepts.

substitute 

substitute(_substitution: Mapping[str, Term]) -> Term

Return the hole unchanged; holes do not bind variables.

free_vars 

free_vars() -> frozenset[str]

Return the empty set.

didactic.gadt.Let dataclass 

Let(name: str, bound: Term, body: Term)

Bases: Term

A monomorphic local binding.

to_spec 

to_spec() -> JsonObject

Return the tagged let record Panproto accepts.

substitute 

substitute(substitution: Mapping[str, Term]) -> Term

Substitute outside the scope of the local binder.

free_vars 

free_vars() -> frozenset[str]

Return free names, excluding the locally bound name.

didactic.gadt.Case dataclass 

Case(scrutinee: Term, branches: tuple[Branch, ...])

Bases: Term

Exhaustive elimination of a closed-sort term.

to_spec 

to_spec() -> JsonObject

Return the tagged case record Panproto accepts.

substitute 

substitute(substitution: Mapping[str, Term]) -> Term

Substitute without replacing variables shadowed by branch binders.

free_vars 

free_vars() -> frozenset[str]

Return free names after removing each branch's binders.

didactic.gadt.Branch dataclass 

Branch(
    constructor: str, binders: tuple[str, ...], body: Term
)

One constructor branch of a case term.

to_spec 

to_spec() -> JsonObject

Return Panproto's case-branch representation.

didactic.gadt.SortExpr dataclass 

SortExpr(name: str, args: tuple[Term, ...] = ())

A sort head applied to zero or more term indices.

to_spec 

to_spec() -> JsonValue

Return a bare name or Panproto's applied-sort record.

substitute 

substitute(substitution: Mapping[str, Term]) -> SortExpr

Substitute throughout the sort's term indices.

free_vars 

free_vars() -> frozenset[str]

Return free names in the index arguments.

didactic.gadt.term_from_spec 

term_from_spec(spec: JsonValue) -> Term

Decode a term previously produced by :meth:Term.to_spec.

PARAMETER DESCRIPTION
spec

A tagged Panproto term record.

TYPE: JsonValue

RETURNS DESCRIPTION
Term

The corresponding immutable term.

didactic.gadt.match 

match(scrutinee: Term, **branches: Body) -> Case

Case analysis, one keyword per constructor: IntLit=lambda v: v.

Each branch lambda runs once with a fresh variable per parameter, and its parameters are the branch's binders. Inside an eliminator body the constructor names are checked against the scrutinee's family at once, naming the valid set on a miss, and each branch's binder count against its constructor. Outside one, those are left to Panproto's checker.

didactic.gadt.let 

let(
    bound: Term, body: Callable[[Var], Term] | Operation
) -> Let

Bind a term locally: let(int_value(), lambda x: IntLit(x)).

The lambda's single parameter is the binder. A unary operation may stand in for the lambda: let(int_value(), IntLit).

didactic.gadt.hole 

hole(name: str | None = None) -> Hole

Construct a typed hole.

Declaration types

didactic.gadt.Sort 

Sort = SortExpr | Family

A sort given directly: an applied family such as Expr[t] or a bare family with no indices such as Ty.

didactic.gadt.SortSpec 

SortSpec = Sort | Dep[Sort]

A sort, or a lambda over earlier inputs producing one.

didactic.gadt.InputSpec 

InputSpec = SortSpec | Implicit

What one keyword argument of a declaration may be.

didactic.gadt.Body 

Body = (
    Operation
    | Callable[[], Term]
    | Callable[[Var], Term]
    | Callable[[Var, Var], Term]
    | Callable[[Var, Var, Var], Term]
    | Callable[[Var, Var, Var, Var], Term]
    | Callable[[Var, Var, Var, Var, Var], Term]
    | Callable[[Var, Var, Var, Var, Var, Var], Term]
    | Callable[[Var, Var, Var, Var, Var, Var, Var], Term]
    | Callable[
        [Var, Var, Var, Var, Var, Var, Var, Var], Term
    ]
)

A term over some binders: an eliminator body, a case branch, a let body.

Model integration

didactic.gadt.Universe 

Universe(name: str, **cases: TypeForm)

A finite Tarski universe for value-indexed schema fields.

The generated GADT contains a closed code sort and an open El(code) carrier. Each supplied case receives a nullary code constructor, a value sort, and an injection from that value sort into the corresponding carrier. The open carrier permits Model field projections while the closed code sort retains exhaustive case analysis.

theory property 

theory: Theory

Compile and return this universe's checked theory.

code 

code(name: str) -> App

Return the nullary term for one universe code.

at 

at(field_name: str) -> IndexedBy

Build a one-index marker selecting payload type by code field.

didactic.gadt.IndexedBy dataclass 

IndexedBy(
    family: Family,
    index_fields: tuple[str, ...],
    cases: tuple[
        tuple[tuple[Term, ...], TypeForm], ...
    ] = (),
    case_labels: tuple[tuple[str, ...], ...] = (),
)

Metadata linking a field's sort to one or more sibling fields.

Put an IndexedBy value inside typing.Annotated. The base Python annotation remains visible to static type checkers, while this marker supplies the dependent family and the model fields used as its indices. Optional cases associate concrete index terms with Python annotations, allowing runtime values to be validated at the refined type.

sort property 

sort: SortExpr

Return the symbolic field sort before model values are substituted.

instantiate 

instantiate(values: Mapping[str, FieldValue]) -> SortExpr

Substitute concrete sibling-field values into the dependent sort.

expected_python_type 

expected_python_type(
    values: Mapping[str, FieldValue],
) -> TypeForm | None

Return the Python payload type selected by concrete indices.

validate 

validate(
    values: Mapping[str, FieldValue], value: FieldValue
) -> None

Check a symbolic or Python payload against its instantiated index.

didactic.gadt.indexed_by 

indexed_by(
    family: Family,
    *index_fields: str,
    cases: Mapping[Term | tuple[Term, ...], TypeForm]
    | None = None,
) -> IndexedBy

Construct an :class:IndexedBy marker.

A one-index family accepts term keys directly. Multi-index families use a tuple of terms per case.

Errors

didactic.gadt.GADTDeclarationError

Bases: ValueError

A locally detectable error in a GADT declaration.

didactic.gadt.GADTReductionError

Bases: RuntimeError

A symbolic reduction could not make safe progress.