Declarations

Indexed-family and constructor declarations.

declarations

Indexed-family and constructor declarations for the QIEC kernel.

FieldDef dataclass

FieldDef(name: str, type: TypeExpr)

One named, typed field of a constructor.

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

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: FamilyId
name	Source name, used for display and for the derived type constructor. TYPE: str
parameters	Binders uniform across every constructor. TYPE: Telescope
indices	Binders a constructor result may refine. Each must be marked refinable, which is what separates them from parameters. TYPE: Telescope
constructors	The constructors this family declares, without repetition. TYPE: tuple[ConstructorId, ...]
closed	Whether the constructor list is exhaustive. A closed family admits coverage checking; an opaque one does not. TYPE: bool DEFAULT: True

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__

__post_init__() -> None

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

def __post_init__(self) -> None:
    """Reject a family whose binders or constructors are malformed.

    Raises
    ------
    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.
    """
    validate_telescope(self.parameters)
    validate_telescope(self.indices)
    names = [binder.name for binder in (*self.parameters, *self.indices)]
    if len(set(names)) != len(names):
        raise ValueError(f"duplicate binder in family {self.name!r}")
    if any(not binder.refinable for binder in self.indices):
        raise ValueError("family indices must be marked refinable")
    if len(set(self.constructors)) != len(self.constructors):
        raise ValueError(f"duplicate constructor in family {self.name!r}")

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: ConstructorId
family	The family this constructor belongs to, which must list it. TYPE: FamilyId
name	Source name. TYPE: str
telescope	Binders local to the constructor. These become rigid skolems while a branch matching it is checked. TYPE: Telescope
fields	The values the constructor carries, uniquely named. TYPE: tuple[FieldDef, ...]
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: tuple[StaticArgument, ...]

__post_init__

__post_init__() -> None

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

def __post_init__(self) -> None:
    """Reject a constructor whose telescope or fields are malformed.

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