Kinds

Kinds, closed index sorts, and declaration telescopes.

kinds

Kinds, closed index sorts, and declaration telescopes for QIEC.

TYPE module-attribute

TYPE = TypeKind()

The kind of types.

EFFECT module-attribute

EFFECT = EffectKind()

The kind of effect interface applications.

ROW module-attribute

ROW = RowKind()

The kind of effect rows.

NAT module-attribute

NAT = NatSort()

The sort of natural-number indices.

SHAPE module-attribute

SHAPE = ShapeSort()

The sort of static tensor shapes.

Kind

Kind = TypeKind | EffectKind | RowKind | ArrowKind

The kind of a static binder: a type, an effect, a row, or an arrow between kinds.

IndexSort

IndexSort = NatSort | ShapeSort | ContextSort | UserIndexSort

The sort of an index binder: naturals, shapes, contexts, or a declared sort.

TelescopeBinder

TelescopeBinder = TypeBinder | IndexBinder | EffectBinder

One binder of a declaration telescope: a type, an index, or an effect binder.

Telescope

Telescope = tuple[TelescopeBinder, ...]

The static binders a declaration takes, in order; later binders may mention earlier ones.

TypeKind dataclass

TypeKind(tag: Literal['type'] = 'type')

The kind of types.

PARAMETER	DESCRIPTION
tag	The serialization discriminator; always "type". TYPE: Literal['type'] DEFAULT: 'type'

EffectKind dataclass

EffectKind(tag: Literal['effect'] = 'effect')

The kind of effect interfaces.

PARAMETER	DESCRIPTION
tag	The serialization discriminator; always "effect". TYPE: Literal['effect'] DEFAULT: 'effect'

RowKind dataclass

RowKind(tag: Literal['row'] = 'row')

The kind of effect rows.

PARAMETER	DESCRIPTION
tag	The serialization discriminator; always "row". TYPE: Literal['row'] DEFAULT: 'row'

ArrowKind dataclass

ArrowKind(domain: Kind, codomain: Kind, tag: Literal['arrow'] = 'arrow')

The kind of a constructor from one kind to another.

PARAMETER	DESCRIPTION
domain	The kind of the argument. TYPE: Kind
codomain	The kind of the result. TYPE: Kind
tag	The serialization discriminator; always "arrow". TYPE: Literal['arrow'] DEFAULT: 'arrow'

NatSort dataclass

NatSort(tag: Literal['nat'] = 'nat')

The sort of natural-number indices.

PARAMETER	DESCRIPTION
tag	The serialization discriminator; always "nat". TYPE: Literal['nat'] DEFAULT: 'nat'

ShapeSort dataclass

ShapeSort(rank: int | None = None, tag: Literal['shape'] = 'shape')

The sort of shapes, optionally restricted to a fixed rank.

PARAMETER	DESCRIPTION
rank	The number of dimensions, or None for any rank. A binder of unspecified rank accepts a shape of any rank, which is what makes a rank-polymorphic signature expressible. TYPE: int or None DEFAULT: None
tag	Discriminator for the index-sort union. TYPE: Literal['shape'] DEFAULT: 'shape'

__post_init__

__post_init__() -> None

Reject a negative rank.

RAISES	DESCRIPTION
ValueError	If rank is negative.

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

def __post_init__(self) -> None:
    """Reject a negative rank.

    Raises
    ------
    ValueError
        If `rank` is negative.
    """
    if self.rank is not None and self.rank < 0:
        raise ValueError("shape rank cannot be negative")

ContextSort dataclass

ContextSort(signature: str, tag: Literal['context'] = 'context')

A logic-program context indexed by a stable signature name.

PARAMETER	DESCRIPTION
signature	The name of the signature whose contexts inhabit this sort. TYPE: str
tag	The serialization discriminator; always "context". TYPE: Literal['context'] DEFAULT: 'context'

UserIndexSort dataclass

UserIndexSort(name: str, constructors: tuple[str, ...], arities: tuple[int, ...] = (), tag: Literal['user'] = 'user')

A closed user-defined index datatype.

Constructor names are part of the sort identity. Open index sorts are deliberately absent from the first kernel because they make coverage unstable under separate compilation.

PARAMETER	DESCRIPTION
name	The sort's name, part of its identity. TYPE: str
constructors	Constructor names, unique and part of the identity. Two sorts with the same name and different constructors are different sorts, which is what keeps coverage decidable. TYPE: tuple[str, ...]
arities	Argument count per constructor, positionally aligned with constructors. Empty defaults to all-nullary. TYPE: tuple[int, ...] DEFAULT: ()
tag	Discriminator for the index-sort union. TYPE: Literal['user'] DEFAULT: 'user'

__post_init__

__post_init__() -> None

Default the arities and reject a malformed sort.

RAISES	DESCRIPTION
ValueError	If the name is empty, there are no constructors, a constructor name repeats, the arities do not align with the constructors, or an arity is negative.

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

def __post_init__(self) -> None:
    """Default the arities and reject a malformed sort.

    Raises
    ------
    ValueError
        If the name is empty, there are no constructors, a
        constructor name repeats, the arities do not align with the
        constructors, or an arity is negative.
    """
    if not self.name:
        raise ValueError("user index sort name cannot be empty")
    if not self.constructors:
        raise ValueError("a closed user index sort needs a constructor")
    if len(set(self.constructors)) != len(self.constructors):
        raise ValueError(f"duplicate constructors in index sort {self.name!r}")
    if not self.arities:
        object.__setattr__(self, "arities", (0,) * len(self.constructors))
    if len(self.arities) != len(self.constructors):
        raise ValueError("index constructor arities must align with constructors")
    if any(arity < 0 for arity in self.arities):
        raise ValueError("index constructor arities cannot be negative")

constructor_arity

constructor_arity(name: str) -> int

The number of arguments one constructor takes.

PARAMETER	DESCRIPTION
name	The constructor name. TYPE: str

RETURNS	DESCRIPTION
int	Its arity, zero for a nullary constructor.

RAISES	DESCRIPTION
ValueError	If the sort has no such constructor. The sort is closed, so an unknown name is an error rather than an open extension.

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

def constructor_arity(self, name: str) -> int:
    """The number of arguments one constructor takes.

    Parameters
    ----------
    name : str
        The constructor name.

    Returns
    -------
    int
        Its arity, zero for a nullary constructor.

    Raises
    ------
    ValueError
        If the sort has no such constructor. The sort is closed, so
        an unknown name is an error rather than an open extension.
    """
    try:
        position = self.constructors.index(name)
    except ValueError as error:
        raise ValueError(
            f"{name!r} is not a constructor of index sort {self.name!r}"
        ) from error
    return self.arities[position]

TypeBinder dataclass

TypeBinder(name: str, kind: Kind = TYPE, refinable: bool = False, tag: Literal['type'] = 'type')

A telescope binder for a type or effect-kinded static argument.

PARAMETER	DESCRIPTION
name	The binder's display name. TYPE: str
kind	The kind of the bound argument. TYPE: Kind DEFAULT: TYPE
refinable	Whether case analysis may refine the bound argument; true for a family's indices and false for its uniform parameters. TYPE: bool DEFAULT: False
tag	The serialization discriminator; always "type". TYPE: Literal['type'] DEFAULT: 'type'

IndexBinder dataclass

IndexBinder(name: str, sort: IndexSort, refinable: bool = False, tag: Literal['index'] = 'index')

A telescope binder for an index argument.

PARAMETER	DESCRIPTION
name	The binder's display name. TYPE: str
sort	The closed index sort of the bound argument. TYPE: IndexSort
refinable	Whether case analysis may refine the bound argument; true for a family's indices and false for its uniform parameters. TYPE: bool DEFAULT: False
tag	The serialization discriminator; always "index". TYPE: Literal['index'] DEFAULT: 'index'

EffectBinder dataclass

EffectBinder(name: str, refinable: bool = False, tag: Literal['effect'] = 'effect')

A telescope binder for an effect argument.

PARAMETER	DESCRIPTION
name	The binder's display name. TYPE: str
refinable	Whether case analysis may refine the bound argument. TYPE: bool DEFAULT: False
tag	The serialization discriminator; always "effect". TYPE: Literal['effect'] DEFAULT: 'effect'

validate_telescope

validate_telescope(telescope: Telescope) -> None

Reject duplicate names in one dependent telescope.

PARAMETER	DESCRIPTION
telescope	The binders to check, in order. TYPE: Telescope

RAISES	DESCRIPTION
ValueError	If a binder name is empty or repeats. Later binders may depend on earlier ones, so a repeated name would make a reference ambiguous.

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

def validate_telescope(telescope: Telescope) -> None:
    """Reject duplicate names in one dependent telescope.

    Parameters
    ----------
    telescope : Telescope
        The binders to check, in order.

    Raises
    ------
    ValueError
        If a binder name is empty or repeats. Later binders may depend on
        earlier ones, so a repeated name would make a reference ambiguous.
    """
    seen: set[str] = set()
    for binder in telescope:
        if not binder.name:
            raise ValueError("telescope binder name cannot be empty")
        if binder.name in seen:
            raise ValueError(f"duplicate telescope binder {binder.name!r}")
        seen.add(binder.name)