Types

Static terms: types, indices, shapes, effect references, and their rendering.

types

Static terms for the Quivers Indexed Effect Core (QIEC).

The module intentionally models only the kernel's small static language. Didactic and Panproto check a first-order projection of its indexed-family declarations, while these frozen records retain the QIEC-specific distinction between uniform parameters and refinable indices.

UNIT module-attribute

UNIT = TypeApplication(TypeConstructorRef.builtin('Unit'))

The unit type, inhabited by None alone.

BOOL module-attribute

BOOL = TypeApplication(TypeConstructorRef.builtin('Bool'))

The Boolean type.

INT module-attribute

INT = TypeApplication(TypeConstructorRef.builtin('Int'))

The integer type.

REAL module-attribute

REAL = TypeApplication(TypeConstructorRef.builtin('Real'))

The real-number type.

STRING module-attribute

STRING = TypeApplication(TypeConstructorRef.builtin('String'))

The string type.

IndexTerm

IndexTerm = IndexVariable | IndexLiteral | IndexConstructor | ShapeIndex

A static index: a variable, a literal, a constructor application, or a shape.

TypeExpr

TypeExpr = TypeVariable | TypeApplication | FunctionType | EqualityType

A type: a variable, a constructor application, a function type, or an equality.

StaticArgument

StaticArgument = TypeExpr | IndexTerm | EffectRef | EffectVariable

Anything a telescope binder may be instantiated at: a type, an index, or an effect.

IndexVariable dataclass

IndexVariable(name: str, sort: IndexSort, identity: StaticVariableId | None = None, tag: Literal['index_variable'] = 'index_variable')

A variable standing for an index term.

PARAMETER	DESCRIPTION
name	The variable's display name. TYPE: str
sort	The closed index sort of the terms it stands for. TYPE: IndexSort
identity	The rigid identity of a case branch's skolem, or None for a declaration binder matched by name. TYPE: StaticVariableId | None DEFAULT: None
tag	The serialization discriminator; always "index_variable". TYPE: Literal['index_variable'] DEFAULT: 'index_variable'

__eq__

__eq__(other: object) -> bool

Compare by identity when either side is rigid, else by name.

A variable carrying a StaticVariableId is rigid: a case branch's skolem, distinct from every other even where the names agree. One without is a declaration binder, which two occurrences share by name. Comparing a rigid variable to a free one is therefore false, which is what stops a branch's skolem from unifying with an enclosing binder.

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

RETURNS	DESCRIPTION
bool	True when both denote the same variable at the same sort.

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

def __eq__(self, other: object) -> bool:
    """Compare by identity when either side is rigid, else by name.

    A variable carrying a `StaticVariableId` is rigid: a case branch's
    skolem, distinct from every other even where the names agree. One
    without is a declaration binder, which two occurrences share by
    name. Comparing a rigid variable to a free one is therefore
    false, which is what stops a branch's skolem from unifying with
    an enclosing binder.

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

    Returns
    -------
    bool
        True when both denote the same variable at the same sort.
    """
    if not isinstance(other, IndexVariable) or self.sort != other.sort:
        return False
    if self.identity is not None or other.identity is not None:
        return self.identity is not None and self.identity == other.identity
    return self.name == other.name

__hash__

__hash__() -> int

Hash the fields __eq__ compares.

RETURNS	DESCRIPTION
int	A hash of the sort with the identity when rigid, and with the name otherwise, so equal variables hash alike.

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

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

    Returns
    -------
    int
        A hash of the sort with the identity when rigid, and with
        the name otherwise, so equal variables hash alike.
    """
    return hash(
        (self.sort, self.identity if self.identity is not None else self.name)
    )

IndexLiteral dataclass

IndexLiteral(value: int | str, sort: IndexSort, tag: Literal['index_literal'] = 'index_literal')

A closed index literal.

PARAMETER	DESCRIPTION
value	A natural number for the nat sort, or a nullary constructor name for a user-defined index sort. TYPE: int | str
sort	The sort the literal inhabits. TYPE: IndexSort
tag	The serialization discriminator; always "index_literal". TYPE: Literal['index_literal'] DEFAULT: 'index_literal'

__post_init__

__post_init__() -> None

Check the literal inhabits the sort it claims.

RAISES	DESCRIPTION
ValueError	If a Nat literal is not a nonnegative integer, if a user sort's literal names a constructor that sort does not declare, or if it names one that takes arguments. The last is the subtle case: a nullary constructor is a literal, while one with arguments has to be applied.

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

def __post_init__(self) -> None:
    """Check the literal inhabits the sort it claims.

    Raises
    ------
    ValueError
        If a `Nat` literal is not a nonnegative integer, if a user
        sort's literal names a constructor that sort does not
        declare, or if it names one that takes arguments. The last is
        the subtle case: a nullary constructor is a literal, while
        one with arguments has to be applied.
    """

    if isinstance(self.sort, NatSort):
        if not isinstance(self.value, int) or self.value < 0:
            raise ValueError("Nat literals must be nonnegative integers")
    if (
        isinstance(self.sort, UserIndexSort)
        and self.value not in self.sort.constructors
    ):
        raise ValueError(
            f"{self.value!r} is not a constructor of index sort {self.sort.name!r}"
        )
    if (
        isinstance(self.sort, UserIndexSort)
        and isinstance(self.value, str)
        and self.sort.constructor_arity(self.value) != 0
    ):
        raise ValueError(f"index constructor {self.value!r} is not nullary")

IndexConstructor dataclass

IndexConstructor(name: str, arguments: tuple[IndexTerm, ...], sort: IndexSort, tag: Literal['index_constructor'] = 'index_constructor')

A fully applied constructor of a user-defined index sort.

PARAMETER	DESCRIPTION
name	The constructor's name, which must belong to sort. TYPE: str
arguments	The constructor's index arguments, in order. TYPE: tuple[IndexTerm, ...]
sort	The sort the constructor builds. TYPE: IndexSort
tag	The serialization discriminator; always "index_constructor". TYPE: Literal['index_constructor'] DEFAULT: 'index_constructor'

__post_init__

__post_init__() -> None

Check the constructor belongs to its sort and is fully applied.

RAISES	DESCRIPTION
ValueError	If the sort is not a user-defined one, if it declares no such constructor, or if the argument count differs from the declared arity. A partially applied index constructor is rejected rather than curried, since an index is a value of its sort and a partial application is not one.

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

def __post_init__(self) -> None:
    """Check the constructor belongs to its sort and is fully applied.

    Raises
    ------
    ValueError
        If the sort is not a user-defined one, if it declares no such
        constructor, or if the argument count differs from the
        declared arity. A partially applied index constructor is
        rejected rather than curried, since an index is a value of
        its sort and a partial application is not one.
    """

    if not isinstance(self.sort, UserIndexSort):
        raise ValueError("named index constructors require a user index sort")
    expected = self.sort.constructor_arity(self.name)
    if len(self.arguments) != expected:
        raise ValueError(
            f"index constructor {self.name!r} expects {expected} arguments, "
            f"got {len(self.arguments)}"
        )
    for argument in self.arguments:
        if index_sort(argument) != self.sort:
            raise ValueError(
                f"argument of index constructor {self.name!r} has the wrong sort"
            )

ShapeIndex dataclass

ShapeIndex(dimensions: tuple[IndexTerm, ...], tag: Literal['shape_index'] = 'shape_index')

A shape given by its dimensions.

PARAMETER	DESCRIPTION
dimensions	One index term per dimension, outermost first. TYPE: tuple[IndexTerm, ...]
tag	The serialization discriminator; always "shape_index". TYPE: Literal['shape_index'] DEFAULT: 'shape_index'

TypeVariable dataclass

TypeVariable(name: str, kind: Kind = TYPE, identity: StaticVariableId | None = None, tag: Literal['type_variable'] = 'type_variable')

A variable standing for a type or effect-kinded static argument.

PARAMETER	DESCRIPTION
name	The variable's display name. TYPE: str
kind	The kind of the arguments it stands for. TYPE: Kind DEFAULT: TYPE
identity	The rigid identity of a case branch's skolem, or None for a declaration binder matched by name. TYPE: StaticVariableId | None DEFAULT: None
tag	The serialization discriminator; always "type_variable". TYPE: Literal['type_variable'] DEFAULT: 'type_variable'

__eq__

__eq__(other: object) -> bool

Compare by identity when either side is rigid, else by name.

A variable carrying a StaticVariableId is rigid: a case branch's skolem, distinct from every other even where the names agree. One without is a declaration binder, which two occurrences share by name. Comparing a rigid variable to a free one is therefore false, which is what stops a branch's skolem from unifying with an enclosing binder.

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

RETURNS	DESCRIPTION
bool	True when both denote the same variable at the same kind.

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

def __eq__(self, other: object) -> bool:
    """Compare by identity when either side is rigid, else by name.

    A variable carrying a `StaticVariableId` is rigid: a case branch's
    skolem, distinct from every other even where the names agree. One
    without is a declaration binder, which two occurrences share by
    name. Comparing a rigid variable to a free one is therefore
    false, which is what stops a branch's skolem from unifying with
    an enclosing binder.

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

    Returns
    -------
    bool
        True when both denote the same variable at the same kind.
    """
    if not isinstance(other, TypeVariable) or self.kind != other.kind:
        return False
    if self.identity is not None or other.identity is not None:
        return self.identity is not None and self.identity == other.identity
    return self.name == other.name

__hash__

__hash__() -> int

Hash the fields __eq__ compares.

RETURNS	DESCRIPTION
int	A hash of the kind with the identity when rigid, and with the name otherwise, so equal variables hash alike.

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

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

    Returns
    -------
    int
        A hash of the kind with the identity when rigid, and with
        the name otherwise, so equal variables hash alike.
    """
    return hash(
        (self.kind, self.identity if self.identity is not None else self.name)
    )

TypeConstructorRef dataclass

TypeConstructorRef(id: TypeId, name: str, telescope: Telescope = ())

A fully qualified type constructor and its kinding telescope.

PARAMETER	DESCRIPTION
id	The constructor's stable identity, which alone determines equality. TYPE: TypeId
name	The constructor's display name. TYPE: str
telescope	The binders the constructor's arguments instantiate, in order. TYPE: Telescope DEFAULT: ()

builtin classmethod

builtin(name: str) -> TypeConstructorRef

A constructor for one of the language's own types.

PARAMETER	DESCRIPTION
name	The builtin's name. TYPE: str

RETURNS	DESCRIPTION
TypeConstructorRef	A nullary constructor whose identity derives from the builtin namespace, so Int means the same type in every module without being declared in any of them.

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

@classmethod
def builtin(cls, name: str) -> TypeConstructorRef:
    """A constructor for one of the language's own types.

    Parameters
    ----------
    name : str
        The builtin's name.

    Returns
    -------
    TypeConstructorRef
        A nullary constructor whose identity derives from the
        ``builtin`` namespace, so `Int` means the same type in every
        module without being declared in any of them.
    """
    return cls(TypeId.derive("builtin", name), name)

__eq__

__eq__(other: object) -> bool

Compare semantic identity, excluding diagnostic presentation data.

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

RETURNS	DESCRIPTION
bool	True when both name the same declaration. The display name and the telescope are presentation, so a constructor read back under a different spelling is still the same type.

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

def __eq__(self, other: object) -> bool:
    """Compare semantic identity, excluding diagnostic presentation data.

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

    Returns
    -------
    bool
        True when both name the same declaration. The display name
        and the telescope are presentation, so a constructor read
        back under a different spelling is still the same type.
    """
    return isinstance(other, TypeConstructorRef) and self.id == other.id

__hash__

__hash__() -> int

Hash the identity __eq__ compares.

RETURNS	DESCRIPTION
int	A hash of the declaration identity alone.

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

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

    Returns
    -------
    int
        A hash of the declaration identity alone.
    """
    return hash(self.id)

TypeApplication dataclass

TypeApplication(constructor: TypeConstructorRef, arguments: tuple[StaticArgument, ...] = (), tag: Literal['type_application'] = 'type_application')

A type constructor applied to static arguments.

PARAMETER	DESCRIPTION
constructor	The constructor applied. TYPE: TypeConstructorRef
arguments	The arguments instantiating the constructor's telescope, in order; empty for a nullary constructor. TYPE: tuple[StaticArgument, ...] DEFAULT: ()
tag	The serialization discriminator; always "type_application". TYPE: Literal['type_application'] DEFAULT: 'type_application'

FunctionType dataclass

FunctionType(parameter: TypeExpr, result: TypeExpr, tag: Literal['function_type'] = 'function_type')

A pure function type.

Effectful codomains are represented explicitly by :class:quivers.qiec.effects.ComputationType, keeping the value and computation strata separate.

PARAMETER	DESCRIPTION
parameter	The argument type. TYPE: TypeExpr
result	The result type. TYPE: TypeExpr
tag	The serialization discriminator; always "function_type". TYPE: Literal['function_type'] DEFAULT: 'function_type'

EqualityType dataclass

EqualityType(kind: Kind | IndexSort, left: StaticArgument, right: StaticArgument, tag: Literal['equality_type'] = 'equality_type')

The proposition that two static arguments are equal.

PARAMETER	DESCRIPTION
kind	The kind or index sort both sides inhabit. TYPE: Kind | IndexSort
left	The left side of the equation. TYPE: StaticArgument
right	The right side of the equation. TYPE: StaticArgument
tag	The serialization discriminator; always "equality_type". TYPE: Literal['equality_type'] DEFAULT: 'equality_type'

EffectVariable dataclass

EffectVariable(name: str, identity: StaticVariableId | None = None, tag: Literal['effect_variable'] = 'effect_variable')

A variable standing for an effect interface application.

PARAMETER	DESCRIPTION
name	The variable's display name. TYPE: str
identity	The rigid identity of a case branch's skolem, or None for a declaration binder matched by name. TYPE: StaticVariableId | None DEFAULT: None
tag	The serialization discriminator; always "effect_variable". TYPE: Literal['effect_variable'] DEFAULT: 'effect_variable'

__eq__

__eq__(other: object) -> bool

Compare by identity when either side is rigid, else by name.

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

RETURNS	DESCRIPTION
bool	True when both denote the same effect variable. A rigid variable never equals a free one, which is what keeps a branch's skolem from unifying with an enclosing binder.

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

def __eq__(self, other: object) -> bool:
    """Compare by identity when either side is rigid, else by name.

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

    Returns
    -------
    bool
        True when both denote the same effect variable. A rigid
        variable never equals a free one, which is what keeps a
        branch's skolem from unifying with an enclosing binder.
    """
    if not isinstance(other, EffectVariable):
        return False
    if self.identity is not None or other.identity is not None:
        return self.identity is not None and self.identity == other.identity
    return self.name == other.name

__hash__

__hash__() -> int

Hash the fields __eq__ compares.

RETURNS	DESCRIPTION
int	A hash of the identity when the variable is rigid, and of the name otherwise.

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

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

    Returns
    -------
    int
        A hash of the identity when the variable is rigid, and of the
        name otherwise.
    """
    return hash(self.identity if self.identity is not None else self.name)

EffectRef dataclass

EffectRef(id: EffectId, name: str, arguments: tuple[StaticArgument, ...] = (), tag: Literal['effect_ref'] = 'effect_ref')

One closed effect interface application.

PARAMETER	DESCRIPTION
id	The stable identity of the interface declaration. TYPE: EffectId
name	The interface's display name. TYPE: str
arguments	The arguments instantiating the interface's telescope, in order. TYPE: tuple[StaticArgument, ...] DEFAULT: ()
tag	The serialization discriminator; always "effect_ref". TYPE: Literal['effect_ref'] DEFAULT: 'effect_ref'

__eq__

__eq__(other: object) -> bool

Compare a concrete interface application by stable identity.

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

RETURNS	DESCRIPTION
bool	True when both name the same declaration and supply equal static arguments. The display name is ignored, and identity is nominal, so two applications of one interface differ only by their arguments.

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

def __eq__(self, other: object) -> bool:
    """Compare a concrete interface application by stable identity.

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

    Returns
    -------
    bool
        True when both name the same declaration and supply equal
        static arguments. The display name is ignored, and identity
        is nominal, so two applications of one interface differ only
        by their arguments.
    """
    return (
        isinstance(other, EffectRef)
        and self.id == other.id
        and self.arguments == other.arguments
    )

__hash__

__hash__() -> int

Hash the fields __eq__ compares.

RETURNS	DESCRIPTION
int	A hash of the declaration identity and the arguments.

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

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

    Returns
    -------
    int
        A hash of the declaration identity and the arguments.
    """
    return hash((self.id, self.arguments))

product_type

product_type(*components: TypeExpr) -> TypeApplication

Construct the canonical finite-product type of the given arity.

PARAMETER	DESCRIPTION
components	The component types, in order. TYPE: TypeExpr DEFAULT: ()

RETURNS	DESCRIPTION
TypeApplication	The product. Its constructor identity derives from the arity, so every two-component product in every module is the same type constructor and two products of different arity are different ones.

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

def product_type(*components: TypeExpr) -> TypeApplication:
    """Construct the canonical finite-product type of the given arity.

    Parameters
    ----------
    components : TypeExpr
        The component types, in order.

    Returns
    -------
    TypeApplication
        The product. Its constructor identity derives from the arity, so
        every two-component product in every module is the same type
        constructor and two products of different arity are different
        ones.
    """

    arity = len(components)
    constructor = TypeConstructorRef(
        TypeId.derive("builtin", "Product", arity),
        f"Product{arity}",
        tuple(TypeBinder(f"item{position}") for position in range(arity)),
    )
    return TypeApplication(constructor, components)

static_kind

static_kind(term: StaticArgument) -> Kind

Return the outer kind of a static term.

Index sorts are deliberately not collapsed into Type: callers that validate an index binder compare the term's concrete sort separately.

PARAMETER	DESCRIPTION
term	The static term to classify. TYPE: StaticArgument

RETURNS	DESCRIPTION
Kind	The term's kind.

RAISES	DESCRIPTION
TypeError	If the term is an index, which carries a sort rather than a kind. Raising rather than returning a placeholder is what keeps a caller from comparing an index against a kind and finding them equal.

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

def static_kind(term: StaticArgument) -> Kind:
    """Return the outer kind of a static term.

    Index sorts are deliberately not collapsed into ``Type``: callers that
    validate an index binder compare the term's concrete ``sort`` separately.

    Parameters
    ----------
    term : StaticArgument
        The static term to classify.

    Returns
    -------
    Kind
        The term's kind.

    Raises
    ------
    TypeError
        If the term is an index, which carries a sort rather than a kind.
        Raising rather than returning a placeholder is what keeps a
        caller from comparing an index against a kind and finding them
        equal.
    """

    if isinstance(term, (EffectRef, EffectVariable)):
        return EFFECT
    if isinstance(term, TypeVariable):
        return term.kind
    if isinstance(term, (TypeApplication, FunctionType, EqualityType)):
        return TYPE
    raise TypeError("index terms have a sort, not a QIEC kind")

index_sort

index_sort(term: IndexTerm) -> IndexSort

Return an index term's sort, checking shape dimensions.

PARAMETER	DESCRIPTION
term	The index whose sort is wanted. TYPE: IndexTerm

RETURNS	DESCRIPTION
IndexSort	The term's sort. A shape reports its concrete rank, which is what lets a rank-polymorphic binder accept it while a binder of a fixed rank does not.

RAISES	DESCRIPTION
TypeError	If a shape dimension is not of Nat sort. A dimension is a count, so admitting anything else would let a shape be indexed by a value that cannot be one.

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

def index_sort(term: IndexTerm) -> IndexSort:
    """Return an index term's sort, checking shape dimensions.

    Parameters
    ----------
    term : IndexTerm
        The index whose sort is wanted.

    Returns
    -------
    IndexSort
        The term's sort. A shape reports its concrete rank, which is what
        lets a rank-polymorphic binder accept it while a binder of a
        fixed rank does not.

    Raises
    ------
    TypeError
        If a shape dimension is not of `Nat` sort. A dimension is a
        count, so admitting anything else would let a shape be indexed by
        a value that cannot be one.
    """

    if isinstance(term, ShapeIndex):
        for dimension in term.dimensions:
            if index_sort(dimension) != NAT:
                raise TypeError("shape dimensions must have Nat sort")
        return ShapeSort(rank=len(term.dimensions))
    return term.sort

validate_static_argument

validate_static_argument(term: StaticArgument) -> None

Recursively validate one intrinsically kinded static argument.

PARAMETER	DESCRIPTION
term	The static term to validate, together with everything nested in it. TYPE: StaticArgument

RAISES	DESCRIPTION
TypeError	If a term is of a class that cannot appear in a static position.
ValueError	If an application is ill-kinded, or an index constructor is applied at the wrong arity.

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

def validate_static_argument(term: StaticArgument) -> None:
    """Recursively validate one intrinsically kinded static argument.

    Parameters
    ----------
    term : StaticArgument
        The static term to validate, together with everything nested in
        it.

    Raises
    ------
    TypeError
        If a term is of a class that cannot appear in a static position.
    ValueError
        If an application is ill-kinded, or an index constructor is
        applied at the wrong arity.
    """
    if isinstance(term, TypeVariable | EffectVariable | IndexVariable | IndexLiteral):
        return
    if isinstance(term, TypeApplication):
        check_static_arguments(term.constructor.telescope, term.arguments)
        return
    if isinstance(term, FunctionType):
        validate_static_argument(term.parameter)
        validate_static_argument(term.result)
        if static_kind(term.parameter) != TYPE:
            raise TypeError("function parameter must have Type kind")
        if static_kind(term.result) != TYPE:
            raise TypeError("function result must have Type kind")
        return
    if isinstance(term, EqualityType):
        validate_static_argument(term.left)
        validate_static_argument(term.right)
        index_kinds = (NatSort, ShapeSort, ContextSort, UserIndexSort)
        index_nodes = (IndexVariable, IndexLiteral, IndexConstructor, ShapeIndex)
        if isinstance(term.kind, index_kinds):
            if not isinstance(term.left, index_nodes) or not isinstance(
                term.right, index_nodes
            ):
                raise TypeError("index equality endpoints must be index terms")
            if not _sort_matches(term.kind, index_sort(term.left)) or not _sort_matches(
                term.kind, index_sort(term.right)
            ):
                raise TypeError("index equality endpoint has the wrong sort")
        elif (
            static_kind(term.left) != term.kind or static_kind(term.right) != term.kind
        ):
            raise TypeError("equality endpoint has the wrong kind")
        return
    if isinstance(term, EffectRef):
        for argument in term.arguments:
            validate_static_argument(argument)
        return
    if isinstance(term, IndexConstructor):
        for argument in term.arguments:
            validate_static_argument(argument)
        index_sort(term)
        return
    if isinstance(term, ShapeIndex):
        index_sort(term)
        for dimension in term.dimensions:
            validate_static_argument(dimension)
        return
    raise TypeError(f"unknown static argument {term!r}")

check_static_arguments

check_static_arguments(telescope: Telescope, arguments: tuple[StaticArgument, ...]) -> tuple[tuple[tuple[str, TypeExpr], ...], tuple[tuple[str, IndexTerm], ...], tuple[tuple[str, EffectRef | EffectVariable], ...]]

Kind-check static arguments against a telescope and classify them.

PARAMETER	DESCRIPTION
telescope	The binders the arguments instantiate, in order. TYPE: Telescope
arguments	One argument per binder. TYPE: tuple[StaticArgument, ...]

RETURNS	DESCRIPTION
tuple[tuple[tuple[str, TypeExpr], ...], tuple[tuple[str, IndexTerm], ...], tuple[tuple[str, EffectRef | EffectVariable], ...]]	The type, index, and effect bindings the arguments make, each paired with its binder's name, in telescope order.

RAISES	DESCRIPTION
TypeError	If the counts differ, an argument is of the wrong static class for its binder, or an argument is of the wrong kind or index sort.
ValueError	If a nested application is ill-kinded, or an index constructor is applied at the wrong arity.

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

def check_static_arguments(
    telescope: Telescope,
    arguments: tuple[StaticArgument, ...],
) -> tuple[
    tuple[tuple[str, TypeExpr], ...],
    tuple[tuple[str, IndexTerm], ...],
    tuple[tuple[str, EffectRef | EffectVariable], ...],
]:
    """Kind-check static arguments against a telescope and classify them.

    Parameters
    ----------
    telescope : Telescope
        The binders the arguments instantiate, in order.
    arguments : tuple[StaticArgument, ...]
        One argument per binder.

    Returns
    -------
    tuple[tuple[tuple[str, TypeExpr], ...], tuple[tuple[str, IndexTerm], ...], tuple[tuple[str, EffectRef | EffectVariable], ...]]
        The type, index, and effect bindings the arguments make, each
        paired with its binder's name, in telescope order.

    Raises
    ------
    TypeError
        If the counts differ, an argument is of the wrong static class
        for its binder, or an argument is of the wrong kind or index
        sort.
    ValueError
        If a nested application is ill-kinded, or an index constructor is
        applied at the wrong arity.
    """
    if len(telescope) != len(arguments):
        raise TypeError(
            f"expected {len(telescope)} static arguments, got {len(arguments)}"
        )

    types: list[tuple[str, TypeExpr]] = []
    indices: list[tuple[str, IndexTerm]] = []
    effects: list[tuple[str, EffectRef | EffectVariable]] = []
    for binder, argument in zip(telescope, arguments, strict=True):
        validate_static_argument(argument)
        if isinstance(binder, TypeBinder):
            if not isinstance(
                argument,
                (TypeVariable, TypeApplication, FunctionType, EqualityType),
            ):
                raise TypeError(f"{binder.name!r} expects a type argument")
            if static_kind(argument) != binder.kind:
                raise TypeError(f"type argument for {binder.name!r} has wrong kind")
            types.append((binder.name, argument))
        elif isinstance(binder, IndexBinder):
            if not isinstance(
                argument,
                (IndexVariable, IndexConstructor, ShapeIndex),
            ) and not hasattr(argument, "sort"):
                raise TypeError(f"{binder.name!r} expects an index argument")
            actual_sort = index_sort(argument)  # type: ignore[arg-type]
            if not _sort_matches(binder.sort, actual_sort):
                raise TypeError(
                    f"index argument for {binder.name!r} has sort {actual_sort!r}, "
                    f"expected {binder.sort!r}"
                )
            indices.append((binder.name, argument))  # type: ignore[arg-type]
        elif isinstance(binder, EffectBinder):
            if not isinstance(argument, (EffectRef, EffectVariable)):
                raise TypeError(f"{binder.name!r} expects an effect argument")
            effects.append((binder.name, argument))
        else:  # pragma: no cover - closed binder union
            raise TypeError(f"unknown telescope binder {binder!r}")
    return tuple(types), tuple(indices), tuple(effects)

render_static

render_static(term: StaticArgument) -> str

Render a static term in the surface spelling.

PARAMETER	DESCRIPTION
term	The type, index, or effect term to render. TYPE: StaticArgument

RETURNS	DESCRIPTION
str	A readable rendering: a constructor applied to its arguments in brackets, with shape arguments in parentheses after them; an arrow for a function type; an equality with ~; a shape as a bracketed dimension list; an index constructor as a call.

RAISES	DESCRIPTION
TypeError	If the term is not a static term.

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

def render_static(term: StaticArgument) -> str:
    """Render a static term in the surface spelling.

    Parameters
    ----------
    term : StaticArgument
        The type, index, or effect term to render.

    Returns
    -------
    str
        A readable rendering: a constructor applied to its arguments in
        brackets, with shape arguments in parentheses after them; an
        arrow for a function type; an equality with ``~``; a shape as a
        bracketed dimension list; an index constructor as a call.

    Raises
    ------
    TypeError
        If the term is not a static term.
    """
    if isinstance(term, TypeVariable | EffectVariable | IndexVariable):
        return term.name
    if isinstance(term, IndexLiteral):
        return str(term.value)
    if isinstance(term, IndexConstructor):
        if not term.arguments:
            return term.name
        inner = ", ".join(render_static(argument) for argument in term.arguments)
        return f"{term.name}({inner})"
    if isinstance(term, ShapeIndex):
        inner = ", ".join(render_static(dimension) for dimension in term.dimensions)
        return f"[{inner}]"
    if isinstance(term, TypeApplication | EffectRef):
        name = term.constructor.name if isinstance(term, TypeApplication) else term.name
        statics = [
            render_static(argument)
            for argument in term.arguments
            if not isinstance(argument, ShapeIndex)
        ]
        shapes = [
            render_static(argument)
            for argument in term.arguments
            if isinstance(argument, ShapeIndex)
        ]
        rendered = name
        if statics:
            rendered += f"[{', '.join(statics)}]"
        if shapes:
            rendered += f"({', '.join(shapes)})"
        return rendered
    if isinstance(term, FunctionType):
        return f"{render_static(term.parameter)} -> {render_static(term.result)}"
    if isinstance(term, EqualityType):
        return f"{render_static(term.left)} ~ {render_static(term.right)}"
    raise TypeError(f"not a static term: {term!r}")