v0.15.0

What's Changed

• Homogenize the QVR grammar surface and parse through the vendored grammar by @aaronstevenwhite in #47

Full Changelog: v0.14.1...v0.15.0

v0.14.1

What's Changed

• fix(dsl): v0.11.0 -> v0.14.0 grammar migration (0.14.1) by @aaronstevenwhite in #46

Full Changelog: v0.14.0...v0.14.1

v0.14.0

What's Changed

• feat(inference,continuous,effects,transpile): 0.14.0 by @aaronstevenwhite in #45

Full Changelog: v0.13.0...v0.14.0

v0.13.0

Added

• GHCi-style :type and :kind commands in the REPL. :type accepts an expression (morphism, program, deduction, scoped sample / observe / let / marginalize / return site, contraction, rule, encoder / decoder / loss, bundle, transformation) and prints the GHCi-shaped one-line signature name :: A -> B (or name :: (Real, Real) => Word -> Word for parametric programs, with the Π-bound parameter universes in a Haskell-style constraint context). :kind accepts a type-level binding (object, space, signature, category) or a bare type expression (FinSet 3, A * B) and prints the kind. Each command rejects the wrong sort with a redirect: :type Doc → "Doc is a type, not an expression; use :kind Doc". The bare-expression fallback tries :type first, then :kind, so users can keep typing a name on its own. Aliases :t and :k work as before.
• User-given type aliases preserved across the REPL. The compiler internally resolves object Item : FinSet 200 to FinSet(name='_FinSet_200', cardinality=200). The REPL now builds an id(obj) → user_name map per session and renders morphism signatures through it, so :type X prints X :: Item -> H_in rather than X :: FinSet 200 -> FinSet 4. The map recurses into product / coproduct components, so a mixed Doc * Topic still surfaces both user names.
• render_signature(compiler, name) shared helper in quivers.cli.repl_session. Single entry point for the GHCi-style signature line, used by both the REPL's :type / :kind / bare-expression fallback and the LSP's hover panel — so a binding looks the same in the TUI and in an editor.
• LSP hover leads with a **Type** / **Kind** block. Hover now shows the GHCi signature first (same string :type / :kind would print), then the doc comment, then the verbatim QVR source slice, then the collapsed AST. Editor users get the one-glance signature that REPL users already had.
• New semantics chapter: docs/semantics/typing.md. Chapter 8 in the semantics development, presenting the QVR type system as a proof calculus: syntactic categories (kinds, type expressions, families, term expressions, statements, programs); contexts ($\Gamma$, $\Delta$, $\Phi$); judgments ($\Gamma \vdash \tau : \kappa$, $\Gamma; \Phi \vdash e : A \rightsquigarrow B$, $\Gamma; \Phi \vdash F(\bar a) : \mathsf{Kernel}[\Phi, B]$, $\Gamma; \Phi \vdash s \dashv \Phi'$, $\Gamma \vdash p : (\Delta) \Rightarrow A \rightsquigarrow B$); the full inference-rule set; the four structural lemmas (Weakening, Substitution, Type Uniqueness, Inversion); the Soundness theorem against the denotation with proof sketches for the representative Compose / Bind / Marginalize / Prog cases; the Subject-Reduction theorem for parametric instantiation; a Completeness theorem (every phrase with a defined raw denotation has a derivation) with a Decidable-Type-Membership corollary on the non-residuated fragment; the bidirectional algorithm underlying the compiler's typechecker; and a worked example deriving the LDA program's full judgment.

Changed

• Constraint context in parametric programs drops binder names. A program with typed parameters renders as lda :: (Real, Real) => Word -> Word, not lda :: (alpha : Real, beta : Real) => Word -> Word — Haskell convention. Parameter names are accessible through :info lda.
• :type of a parametric program no longer curries the parameters with the kernel arrow. Per docs/semantics/programs.md §3a, typed parameters denote a dependent family $\prod_{p:P} \mathbf{Kern}(\mathrm{dom}, \mathrm{cod})$ — they live in a $\Pi$, not in the kernel's domain. Rendering them as Real -> Real -> Word -> Word (the previous "GHCi-curried" form) conflates the $\Pi$-context with the kernel arrow.
• Compiler-driven expression typing in :type. The expression-fallback path now drives Compiler._compile_expr directly on the already-compiled session state instead of re-running the full module compile for every :type query.
• Auto-generated placeholder names stripped from output. The compiler assigns synthetic names like _FinSet_20 and _Real_8 to anonymous FinSets and Euclidean spaces. They no longer leak into :type / :kind output as Doc : _FinSet_20; the stripper renders them as Doc : FinSet 20.
• Help-text rewrite for :type and :kind. Both commands' inline :help entries and detailed :help :type / :help :kind text now match the GHCi-style semantics.

Documentation

• docs/semantics/typing.md added as chapter 8; index renumbered.
• Semantics corpus audit (substantive). After threading typing.md into the development:
  • Cross-link setting.md §6, morphisms.md, and programs.md into the new typing chapter at their natural touch-points.
  • morphisms.md §1.1 gets a "Categorical structure" proposition under the strict-quantale hypothesis, proving $\mathcal{V}\text{-}\mathbf{Rel}$ is a symmetric monoidal category using the join's universal colimit property, $\otimes$ associativity, $\bot$ absorption, and the distributivity law; flags the lax cases of $\mathcal{V}{\mathrm{pf}}$ / $\mathcal{V}{\mathrm{L}}$ explicitly.
  • programs.md §5 upgrades the monad-law table to a "Monad laws for QVR programs" theorem with proofs derived from the Giry monad's universal property (Giry 1982, Kock 1972, Fritz 2020). The commutativity equation is now stated with an explicit double-strength pair $\mathrm{dst}_1$ / $\mathrm{dst}_2$ rather than the previous ambiguous one-line formula, identifying Fubini–Tonelli as its substance.
  • adequacy.md §3.4 upgrades the one-liner "the proofs are straightforward" to a full "Adequacy of @" proposition with term-by-term unfolding; the remaining five tensor combinators get a table whose every row makes the proof template explicit.
  • effects.md §4a adds explicit inference rules for the four chart firings (Base, Lift_T, Handle_{T→S}, Eliminate_T, Swap_{T|U}), turning the previously prose-only joint type-and-effect dispatch into a proof system.
  • Stale class-name references across the corpus updated: TypeExpr → ObjectExpr, TypeProduct → ObjectProduct, TypeEffectApply → ObjectEffectApply (the AST class was renamed and the docs had not tracked it).
  • adequacy.md §3.7 references the real method names (_compile_program, not _compile_program_body; dispatch key compose, not compose_deductions).
  • adequacy.md §4: drop references to tests/test_resolution_lenses.py, which no longer exists.
• British → American spelling sweep across all 14 semantics chapters. marginalisation → marginalization, realise → realize, behaviour → behavior, catalogue → catalog, modelling → modeling, analyse → analyze, etc.

Fixed

• Compiler.signatures, Compiler.categories now exposed to the REPL's bare-name lookup. Previously, :type SomeSignature returned "unknown name" because signatures and categories were not in either the value-level or type-level buckets the REPL consulted. They are now classified as type-level (a signature denotes a generalised algebraic theory; a category denotes an atom universe) and respond to :kind.
• Contraction and rule signatures render correctly under :type. Contractions get an operadic c :: (A_1, …, A_k) -> B signature; rules get the r :: prem |- concl schema form.

v0.12.0

Added

• :: scope paths everywhere a binding name is taken. :info, :type, :doc, :browse, :plate, :graph, :where, :effects, :shape all accept a ::-separated scope path. The leftmost segment is a top-level binding; each subsequent segment looks up a named child in that binding's scope. Coverage across every container kind: program (typed parameters + sample / observe / let / marginalize / return steps; recursing into nested marginalize bodies), deduction (rules / atoms / lexicon entries), signature (sorts / constructors / binders / vertex_kinds / edge_kinds), encoder (op_rules / init_rules / message_rules / update_rules / var_inits), decoder (per-constructor heads), bundle (member rule names), contraction (input parameter names). Examples: lda::theta resolves to the sample site inside the lda program; lda::z::w to the observe site inside the lda program's marginalize block; LF::Term to the Term sort inside the LF signature; CCG::fwd_app to the forward-application rule inside the CCG deduction.
• quivers.analysis.scope module. New ScopedRef value type, resolve_scoped_path(compiler, path) resolver, scope_children(ref) view, find_all_references(compiler, name) reverse lookup. Foundation for every scope-aware REPL feature.
• Env-tree click navigation on every nested node. Each env-tree node now carries its full :: path on node.data. Clicking any node (top-level binding, program step, deduction rule, signature sort, bundle member) fires :info PATH against that exact binding. Previously only top-level bindings were clickable; nested children either did nothing or raised "undefined morphism" errors when the click handler tried to dispatch against the rich signature label.
• Scope-aware tab completion. lda:: completes against the lda program's children; lda::z:: completes against the marginalize block's inner scope; a bare-name prefix like thet surfaces every scoped descendant whose final segment matches (lda::theta).
• quivers.analysis.plate_graph module. Extractor that walks a compiled QVR program and builds a PlateGraph capturing nodes (latent / observed / marginalized / deterministic), plates (with nested parents), and dependency edges. The grouping plate of a marginalize block propagates correctly to nested observes via the [over=G] axis; the [via=idx] fibration index is correctly treated as a routing label rather than an additional plate. Handles nested marginalize blocks recursively.
• :plate PROGRAM meta-command with five output formats: default Rich table (kind / variable / family / plates / parents), --mermaid (Mermaid graph TD source with subgraph clusters per plate), --dot (Graphviz DOT with cluster_* subgraphs), --tikz (LaTeX TikZ + bayesnet snippet), --daft (Python script using the daft library), and --open (renders via daft or graphviz to a temp PNG and launches the system default viewer; falls back to Mermaid source if no renderer is installed).
• :graph PROGRAM meta-command. Vertical step-flow view of a program: one row per sample / observe / let / marginalize / return step with its dependency parents on the side. No 2D edge routing in the in-TUI view so the output is robust on any terminal width. Same --mermaid / --dot / --open flags as :plate.
• :where NAME meta-command. Lists every scope path in the loaded module whose final segment is NAME, sorted by depth. Useful for finding cross-references between programs, deductions, and other declarations.
• :effects PROGRAM meta-command. Prints the program's declared [effects=[...]] set alongside the effect set inferred from the body (Sample / Score / Marginal / Pure based on the step kinds present). Flags leak (body uses effects not declared) and unused (declared but not used) divergences.
• :shape PROGRAM meta-command. Pretty-prints the program's ChainShape: per-step depth, kind, intermediate axis size, source location. Useful for auditing chain depth before fitting.
• Modal :help dialog. Promotes :help from "write to the output log" to a proper Textual ModalScreen overlay with its own focus, ESC-to-close, and a live filter input. Lists every meta-command grouped by category (loading / inspection / program exploration / live editing / control) plus the full keybinding table. The TUI's F1 binding pushes the same modal.

Changed

• TUI env-tree builder unified. Replaced the 12 per-kind _children_for_* builders with a single uniform walker that consults scope_children(). Each node's display label comes from a single per-kind type-line renderer; each node's data is its full scope path. Result: every container kind expands to its declared children in a single layered tree without duplicate per-kind logic.
• Compiler.compile_env() returns every populated bucket. Adds programs, deductions, signatures, encoders, decoders, losses, bundles, contractions, transformations to the union, so consumers that walk the env dict see every declared atom.

Fixed

• Compiler.losses and compile_env() called reg.entries() (parentheses). LossRegistry.entries is a plain list attribute, not a method. The misplaced call broke every module that declared a loss. The accessors now read the attribute directly.

Full Changelog: v0.11.5...v0.12.0

v0.11.5

Fixed

• qvr repl rendered every token in the same colour on customised terminal palettes. The STYLE_TABLE used palette-indexed colour names ("bold magenta", "bold blue", "bold cyan", "default"). Terminals whose palettes mapped those four into the same warm hue (common in custom themes) collapsed every span into a single colour, so :info's body looked uniformly red. Switched the table to truecolor #RRGGBB codes (One-Dark inspired) so palette mapping does not apply and the keyword / type / operator / variable distinctions remain visible regardless of the user's terminal theme.
• Clicking a program / deduction / signature / encoder / decoder node in the env tree raised a "compile error: undefined morphism" or did nothing at all. The click handler read the node's display label (lda(alpha : Real, beta : Real) : Word -> Word) and dispatched :info against that whole string. After 0.11.3 added nested-children expansion, expandable nodes also stopped firing the handler entirely because of an allow_expand gate. The handler now reads the bare binding name from a dedicated node.data slot populated at tree-build time, and the allow_expand gate is gone, so a click on any named declaration fires :info NAME correctly.

Added

• Comprehensive TUI regression suite at tests/cli/test_repl_tui.py. 20 tests covering: click-target resolution under every node shape (root / category heading / named binding / nested step / non-identifier data); the STYLE_TABLE truecolor invariant; each per-kind nested-children builder; the rendered ANSI for a real :info body (truecolor codes only, distinct codes per token class, keyword / type colour distinct); the full :type and :browse signature lines including typed parameter lists; the completion engine surfacing program names with the correct kind detail; and the TUI module's import-cleanliness on a minimal install.

Full Changelog: v0.11.4...v0.11.5

v0.11.4

Fixed

• :type on a parametric program dropped its parameter list. Typed program parameters (alpha : Real, beta : Real, G : FinSet, k : Mor[A, B]) live on the AST's type_params slot, not on params (which holds bare names). The REPL session and the TUI env-tree builder were both reading only params, so loading lda.qvr and running :type lda printed program lda : Word -> Word instead of program lda(alpha : Real, beta : Real) : Word -> Word; the env tree's program node had the same problem. Both call sites now walk both slots and render the typed parameter list with its ScalarParam / ObjectParam / MorphismParam annotation.

Full Changelog: v0.11.3...v0.11.4

v0.11.3

Fixed

• REPL environment was missing eight declaration categories. qvr repl, :browse, and the TUI env browser only surfaced objects / spaces / morphisms / rules — every other top-level declaration (program, composition, deduction, signature, encoder, decoder, loss, bundle, contraction) compiled successfully but was invisible at the user-facing surface. Loading lda.qvr showed three objects and "0 programs" despite the declared program lda. The compiler now exposes public @property accessors (programs, deductions, signatures, encoders, decoders, losses, bundles, contractions, transformations) and compile_env() returns the full set; the REPL session, :browse, the completer, and the TUI status bar / env tree all surface every populated bucket.

Added

• Nested env-tree rendering. The TUI env pane now expands structural declarations to their internal AST shape on click: a program opens to its sample / observe / let / marginalize / return step list (with marginalize recursively opening to its body); a deduction opens to its rules (each labelled with its premises |- conclusion line) plus semiring / tolerance metadata; a signature opens to its sorts / constructors / binders / vertex_kinds / edge_kinds tables; a bundle opens to its constituent rule names. The plain-text :browse meta-command renders the same hierarchy as indented text so plain-mode users (qvr repl --plain, Jupyter kernel) see the same structure the TUI shows.

Full Changelog: v0.11.2...v0.11.3

v0.11.2

Changed

• panproto>=0.48.4 and panproto-grammars-all>=0.48.4. Upstream now vendors the homogenized QVR grammar (the unified KIND NAME : SIGNATURE [k = v, ...] [~ INIT] [BODY] surface, the composition NAME as <level> keyword, the [role=...] option-block roles, the indented-body deductions / signatures / encoders / decoders / marginalize blocks). The QVR_USE_LOCAL_GRAMMAR shim is no longer required for the runtime parser: a fresh wheel install parses every gallery example out of the box.

Fixed

• qvr repl, qvr-lsp, qvr-kernel parse-error on every .qvr load. 0.11.0 / 0.11.1 against panproto-grammars-all 0.48.3 (the latest at release time) used a pre-homogenization grammar whose object_decl node had no init field; the in-tree parser walker raised ParseError: object_decl missing value on the first homogenized declaration. With panproto-grammars-all>=0.48.4 the vendored grammar matches the walker's expectations and every example in docs/examples/source/ loads cleanly.

Full Changelog: v0.11.1...v0.11.2

v0.11.1

Fixed

• Wheel shipped without grammar.json. _grammar_introspection walks the tree-sitter grammar.json to derive the keyword / punctuation / builtin sets the Pygments lexer, the REPL completer, the TUI highlighter, and the LSP semantic-tokens legend all consume. The canonical file lives at grammars/qvr/src/grammar.json (regenerated by tree-sitter generate), which sits outside src/quivers/ and so was excluded from the wheel build. The 0.11.0 install crashed on first import of quivers.dsl.pygments_lexer with FileNotFoundError: grammars/qvr/src/grammar.json not found above ..., which in turn blocked qvr repl, qvr-lsp, and qvr-kernel. A package-local copy at src/quivers/dsl/_grammar_data/grammar.json is now committed and included in the wheel; _grammar_json_path() prefers the package-local copy and falls back to the in-tree source for editable installs. tools/sync_grammar_data.py keeps the two copies in lockstep, with a --check mode CI can gate on.

Full Changelog: v0.11.0...v0.11.1