Skip to content

refactor(language): an operator, a declaration kind and a notation name the values they can be, rather than being a string - #345

Merged
FBumann merged 1 commit into
mainfrom
refactor/literal-vocabularies
Sep 1, 2026
Merged

refactor(language): an operator, a declaration kind and a notation name the values they can be, rather than being a string#345
FBumann merged 1 commit into
mainfrom
refactor/literal-vocabularies

Conversation

@FBumann

@FBumann FBumann commented Sep 1, 2026

Copy link
Copy Markdown
Contributor

Prompt: I think we could improve type hints etc more! Narrowing them from str to literals for example.

Note

The following content was generated by AI.

Six vocabularies that were closed in prose but open in the annotation now name their members, so the checker enforces what a docstring used to ask for. No behaviour changes.

The one that earns its place: Namespace.kind() returned str | None with the four kinds written out in its docstring, and both match statements over it ended in case _. It now returns DeclarationKind, the wildcards are gone, and non-exhaustive-match — already an error since #325 — guards a fifth kind.

Was Is Where
kind() -> str | None -> DeclarationKind | None resolution.py
Namespace.dtypes: Mapping[str, str] Mapping[str, DeclaredDtype] resolution.py, threaded through exclusivity.py
UnaryOperatorNode.op: str UnaryOperator expression_parser.py
BinaryOperatorNode.op: str BinaryOperator expression_parser.py
Format.notation: ClassVar[str] ClassVar[Notation] format.py, latex.py, typst.py
SymbolTable.notation: str Notation symbols.py

_PRECEDENCE, _PREDICATES, _ORDERED_DTYPES and NUMERIC_DTYPES are typed by the vocabulary they are keyed or filled by, which is what makes the narrowing reach a lookup rather than stop at the field.

Verified: pixi run ci — lint, 1003 tests, mkdocs build --strict, 27 documents compiled. Each new guard was checked by deleting it and watching the checker fail; output below.

The guards, deleted

non-exhaustive-match on kind — remove the case 'lookup': arm from _resolve_where:

ERROR Match on `Literal['dimension', 'lookup', 'parameter', 'variable']` is not exhaustive [non-exhaustive-match]
 INFO 1 error (9 suppressed)

DeclaredDtype on _ORDERED_DTYPES — misspell 'datetime':

ERROR `tuple[Literal['float'], Literal['int'], Literal['datetimee']]` is not assignable to `tuple[DeclaredDtype, ...]` [bad-assignment]
 INFO 1 error (9 suppressed)

BinaryOperator on the node — construct one the grammar cannot produce:

ERROR Argument `Literal['^']` is not assignable to parameter `op` with type `Literal['*', '**', '+', '-', '/']` in function `math_spec.expression_parser.BinaryOperatorNode.__init__` [bad-argument-type]
Two shapes the checker forced, and one cast

The wildcards could not simply become case None:. pyrefly 1.2.0 does not treat a wildcard-free match over a Literal as terminating flow, so removing case _ made the outer assert_never(node) unreachable-by-its-own-lights and errored. case _: assert_never(kind) does not fix it either — only a bare raise does, and a wildcard defeats the exhaustiveness check that was the point.

The shape that gets both: hoist kind = ns.kind(...), handle None as a guard clause above the match, and let the arms that only record an error fall out to one shared return node. That reads as an invariant rather than a workaround — an arm that builds a node returns it, an error path returns the node unchanged, once.

One cast was added, in SymbolTable.load: notation not in NOTATIONS does not narrow a str, so the value crossing into the typed field is cast at the validation boundary, directly under the check that earns it. redundant-cast is an error since #325 and does not flag it.

Deliberately not done
  • OPERATOR_SPELLINGS / Format.operators / Walk.op — 30 rows, 46 call sites. Left for a follow-up, because tests/typesetting/test_golden.py::test_the_golden_model_asks_for_every_operator_the_vocabulary_spells already catches an unspelled name, so it is a smaller win than the six above and wants its own diff.
  • FORMATS and BUILTINS — keyed by strings arriving from argparse and from a parsed file. A Literal key buys a cast at the boundary and nothing downstream.
  • EdgeNode.policyLiteral['wrap'] — honest, but a one-member Literal is ceremony.
  • getattr(vdef.bounds, side) in model.py and dimensions.py returns Any. A real hole, but the fix is reaching the two fields directly, not a Literal.

…me the values they can be, rather than being a string

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Hdxai54hc4LwxFQBqMM8jF
@read-the-docs-community

Copy link
Copy Markdown

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant