v0.4.0

quivers v0.4.0

This release lands three deeply-interconnected bodies of work in a single minor bump, all motivated by the goal of making quivers a unified surface for probabilistic, weighted-deductive, and neural-symbolic programs:

1. DSL surface homogenisation — one Kleisli-bind sigil <-, type-annotated indexed binds, scoped marginalize, and !-prefixed effect signatures.
2. Agenda-based weighted-deduction framework — a single engine subsuming CKY, Earley, Viterbi, inside-outside, semi-naïve Datalog, A* parsing, Knuth's algorithm, and MLTT proof search, declared via deduction { … } blocks with first-class differentiable charts.
3. Hierarchical-Bayesian + arrow / algebraic-effects substrate — plate draws, vectorised observations, marginalisation, LKJ priors, Cholesky factor spaces, the Hughes arrow tower (Arrow, ArrowChoice, ArrowApply, ArrowLoop, ArrowZero, ArrowPlus), stdlib monads / monad transformers, algebraic effects + handlers via FreeMonad.
4. Structural compression: signatures, encoders, decoders, losses — a uniform algebraic interface for compressing arbitrary structured objects (sequences, trees, graphs, charts, typed lambda terms) to fixed-length vectors and decoding them back under a learned distribution. Realises transformers, tree-LSTMs, graph-NNs, autoregressive LMs, VAEs, and vector-inside-outside parsers as instances of one F-algebra / F-coalgebra pattern.

Changed (breaking, pre-1.0 clean cut)

Surface DSL homogenisation. The program-block surface is reorganised around a single Kleisli-bind sigil <-, type-annotated indexing on the binder, scoped marginalisation, and !-prefixed effect signatures. The categorical denotation is unchanged; only the surface forms shift to a Haskell-PPL aesthetic.

• draw v ~ F(args) → v <- F(args) — the draw keyword is retired in favour of the unique Kleisli-bind sigil <-. The surface-arrow alternative (the v0.4 do-notation v <- F form) is unified with the new sigil; there is now one and only one way to introduce a random variable.
• draw v : A -> K ~ F(args) → v : A <- F(args) — indexed (plate) binds use a type annotation on the binder rather than a separate keyword family. The per-fiber codomain is taken from the family; the : A annotation declares the index set.
• observe v ~ F(args) → observe v <- F(args) — scored binds retain the observe prefix; the rest of the line matches the Kleisli-bind shape.
• observe r[n] ~ F(args) for n in N → observe r : N <- F(args) — the vectorised-observe for n in N shape collapses into the type-annotated form. Bracket-indexed family arguments theta[N] annotate that an argument is a section of an N-indexed family.
• marginalize c (trailing) → marginalize c : A <- F(args) in { … } — marginalisation is always scoped; the integration target and the scope are visible at the binding site. The categorical pushforward becomes visually local to its binding.
• posterior name (model) [params] : dom -> cod → program name (params) : dom -> cod ! Pure over model — posterior blocks are encoded as program declarations with a ! Pure effect signature and an over model modifier. The parser routes such programs to the posterior registry and the compiler enforces the determinism constraint.
• ! effect signature on programs — program P : X -> Y ! Sample, Score declares the body's capability set. Effects: Sample, Score, Marginal, Pure. The compiler verifies the body's actual effects are a subset of the declared set (or rejects any effect when Pure is declared).
• output X → export X — module-level exports replace output; multiple export declarations per module are allowed.
• Drop labelled-tuple return form — the v0.4 return (a: x, b: y) form was purely syntactic rebinding without semantic effect; it is removed as dead surface.

Internal

• BindStep unifies the four old step shapes (DrawStep, PlateDrawStep, VectorisedObserveStep, MarginalizeStep) at the AST level; the old shapes remain as compiler-internal IR consumed by the runtime step-builder. The parser emits only BindStep and LetStep; the compiler's _expand_bind_steps pass translates to the internal IR.
• ProgramDecl gains effects: frozenset[str] | None and over_model: str | None fields.
• MonadicProgram gains an effect_set: frozenset[str] | None field for introspection by downstream inference / dispatch code.
• ExportDecl replaces OutputDecl. The first declared export is the module's primary output; subsequent exports are accessible as additional module bindings.
• The DSL's <- arrow now binds with prec.right, eliminating the previous GLR ambiguity between draw-args and following steps.

Migration guide

For most programs the mechanical translation is:

pre-0.4	0.4
draw v ~ F(args)	v <- F(args)
draw v : A -> K ~ F(args)	v : A <- F(args)
observe v ~ F(args)	observe v <- F(args)
observe r[n] ~ F(args) for n in N	observe r : N <- F(args)
marginalize c	marginalize c <- F(args) in { … }
posterior P (M) [v] : … body	program P(v) : … ! Pure over M body
output E	export E

Tests

• All example .qvr files migrated to the 0.4 surface.
• Tree-sitter corpus covers the new surface shapes (20/20 parses).

Agenda-based weighted-deduction framework

0.4 also lands the full agenda-engine substrate underneath a declarative deduction { … } block. The framework subsumes CKY, Earley, Viterbi, inside-outside, semi-naïve Datalog evaluation, A* parsing, Knuth's algorithm, depth-first MLTT proof search, and edit-distance dynamic programming as parameter settings on a single engine.

• Surface form: qvr deduction CG : Atom -> Atom { atoms { NP, S, VP } rule fwd_app : X/Y, Y |- X rule bwd_app : Y, Y\X |- X semiring LogProb start S depth 4 } Single-uppercase-letter pattern names (X, Y) bind as wildcards; non-wildcard atoms match literally. The block declares the seven irreducible parameters of an agenda-based deduction (item algebra via atoms, rule set, semiring, axiom source, goal predicate, start symbol, depth bound). Concrete parsing strategies are selected by the compiler from these parameters.

• Charts as first-class differentiable values: each deduction's runtime view exposes chart.weight(item), chart.enumerate(pattern), chart.derivations(item), chart.goal_weight() — all returning torch.Tensor values whose gradients flow back through the agenda's semiring operations to any requires_grad=True axiom / rule weight, enabling end-to-end gradient-based learning over deduction systems (the Goodman 1999 semiring framework lifted to PyTorch tensors).

• Pre-registered stdlib deductions (quivers.stochastic.stdlib): CCG, Lambek, STLC, MLTT, Datalog, Dijkstra, HMM, ViterbiHMM, EditDistance. Users import and run them directly: python from quivers.stochastic.stdlib import Datalog view = Datalog(edge_axioms) reaches = view.enumerate(("reach", source, Wildcard("Y")))

• Agenda strategies: cky_agenda(), earley_agenda(), viterbi_agenda(priority_fn), astar_agenda(g_plus_h), knuth_agenda(), depth_first_agenda(), semi_naive_agenda(). Strategy independence (Goodman 1999 §3) is verified in test_agenda.py: under idempotent semirings, chart values agree across all strategies.

• panproto integration: QVR_DEDUCTION_PROTOCOL and extract_deduction_schema(compiler) make deduction systems first-class panproto schemas. Schema morphisms over the protocol correspond to deduction-system specialisations (e.g., CCG ⊂ Lambek ⊂ MultimodalLambek).

Structural compression: signatures, encoders, decoders, losses

The release lands a uniform algebraic interface for compressing arbitrary structured objects to fixed-length vectors and decoding them back under a learned distribution. Categorically: every constructor algebra a user declares is the initial Σ-algebra T_Σ of a multi-sorted signature; a encoder is a Σ-algebra homomorphism T_Σ → Vec_D, and a decoder is a Kleisli coalgebra Vec_D → Kern(T_Σ). The recursion / corecursion is supplied by the framework; the analyst supplies only the per-operation parametric functions. This single abstraction subsumes RNN / transformer / tree-LSTM / graph-NN encoders, autoregressive LM and variational decoders, and the proposal's vector inside-outside parser (the chart's item signature is Σ, the parser's combine / split^L,R are the per-operation encoder functions, the attention-weighted aggregation lives entirely inside the encoder — outside the chart's role, so the semiring abstraction is not broken).

• Signature blocks declare sorts, constructors, binders, and (for graph signatures) vertex / edge kinds: qvr signature LF { sorts { Term : object dim 64 Type : object dim 32 Name : data dim 32 vocab { "dog", "cat", "every" } } constructors { Const : Name -> Term App : Term, Term -> Term } binders { Lam : binds (x : Term : ty : Type) in (body : Term) -> Term } } Three sort kinds: object (recursively decoded), data (opaque raw values; data sorts may declare a closed vocabulary via vocab { … } of string / integer / float literals), index (de-Bruijn slots). The reserved BoundVar op is a built-in de-Bruijn reference; binders thread a typed context Γ carrying (var_sort, embedding, type_term) per scope entry. Binder variables may carry an annotation sort via binds (x : Term : ty : Type) — the variable's type is structurally tracked through the de-Bruijn context.
• Encoder blocks declare an F-algebra homomorphism T_Σ → Vec_D. Per-constructor bodies are user-supplied or scaffolded as 2-layer MLPs by the compiler with correct per-arg dimensions. Sequence sugar — Cons(head, tail) recurrent state |-> body for left-folds and Cons(head, tail) attention prefix |-> body for iterative outside-in walks that thread a running prefix list — handles RNN / transformer-shaped encoders uniformly. Graph signatures use a message_passing-shaped body (init[V], message[E], update[V], readout, iterations N).
• Decoder blocks are Kleisli coalgebras Vec_D → Kern(T_Σ) with sample(vec) -> Term and log_prob(term, vec) -> Tensor. Per-sort structure / primitive / factor / binder_select heads are scaffolded as learnable neural networks; the corecursion (structure choice, factor split, recursive descent with extended Γ at binders, BoundVar fallback to in-scope variables, depth-bounded termination) is supplied by the framework. No silent type coercion or sentinel value: an observed term whose shape doesn't match the canonical form raises with a typed diagnostic.
• var_init per (var_sort, annot_sort) pair: multiple var_init Term from Type as ty |-> body declarations per encoder, one per pair of sorts the signature's binders introduce; the compiler scaffolds defaults for omitted pairs.
• Stdlib shapes (quivers.structural.shapes): Seq[A] with rnn_encoder, transformer_encoder, bow_encoder, ar_decoder; Tree[L, B] with tree_lstm_encoder and tree_decoder; Graph[V, E] with graph_signature and gnn_encoder (per-edge-kind message MLP, per-vertex-kind GRU update, mean / sum / max readout).
• Deduction integration: a deduction block may declare an item signature and attach a encoder; the chart's embedding(item) query returns a differentiable vector computed by the attached encoder's algebra-homomorphism recursion over the chart-item term.
• Loss attachments (loss <name> [weight ...] [on <site>] { body }): attachable at global, program <name>, deduction <name>, encoder <name>, decoder <name>, rule <name> in <D>, and chart of <D> sites. Rule-attached losses fire on every rule application during chart construction (the agenda's _fire path invokes a registered rule_callback with the full antecedent list); chart-attached losses fire once on the completed chart. LossRegistry.evaluate_on(kind, target, env) returns the weighted partial sum for a given attachment site; ChartView.attached_loss exposes the accumulated rule + chart losses fired during a deduction's run.
• Optional export: a module with only signatures / encoders / decoders / losses (no top-level morphism) now compiles into a Program(None) container; the artifacts are reachable through prog.signatures / prog.encoders / prog.decoders / prog.losses. The previous no export declaration found hard error is replaced by a precise diagnostic on forward().
• Strict declaration discipline: every sort referenced in a constructor's domain or a binder's variables / scoped arguments / codomain must be declared in the signature's sorts { … } block — no silent auto-registration. Every sort with no inline dim must have its dim supplied by every encoder / decoder over the signature. Reserved op names (BoundVar, Data) are rejected as user-declared constructors or binders. vocab clauses are only valid on data sorts; duplicate vocabulary entries are rejected.
• Public surface: quivers.structural exports Signature, Sort, Constructor, Binder, BinderVarSpec, BinderArgSpec, VertexKind, EdgeKind, Term, Context, EMPTY_CONTEXT, DataLeaf, Encoder, Decoder, LossEntry, LossRegistry, bound_var, make_term. quivers.structural.shapes exports the canonical sequence / tree / graph factories.
• 27 new tests in tests/test_structural.py cover every surface form, every strict-rule diagnostic, the typed-binder discipline, end-to-end compression and decoding for sequences / trees / graphs, rule-attached and chart-attached loss firing, per-pair var_init overrides, recurrent / attention modes, and the data-sort vocabulary pipeline.

Hierarchical-Bayesian primitives and arrow / effects tower

Added

• Hierarchical-Bayesian modelling primitives in quivers.continuous.bayesian, each carrying its categorical denotation in Kern:
• PlateDraw(index_size, family, domain) — finite-domain-indexed draw realised as a Kern-morphism A → B by the natural isomorphism Kern(1, B^A) ≅ Kern(A, B); subclass of ContinuousMorphism so it threads through the existing MonadicProgram step machinery.
• VectorisedObserve(family, response) — batched-observation kernel Φ → G_{≤1}(Φ) with score ∏_n p_F(r_obs(n); θ(n, φ)).
• marginalize_categorical(log_probs) — program-level pushforward through π_{Φ\C} realised as log_sum_exp over the class axis.
• LKJCorrelationFactor(K, eta) — LKJ prior on CholeskyFactor(K) via the Lewandowski-Kurowicka-Joe onion method; analytic log_prob matches Stan's lkj_corr_cholesky_lpdf.
• Truncated(base, lower, upper) — generic interval-truncation combinator (rejection sampling with Monte-Carlo truncation-mass estimation).
• cumsum(K), softmax(K) — deterministic morphisms for monotone splines and simplex projection.
• cholesky_quad_form(K) — covariance reconstruction Σ = diag(s) L L^T diag(s).
• CholeskyFactor(K) ContinuousSpace — manifold of K×K lower-triangular factors of correlation matrices.
• Surface syntax for hierarchical-Bayesian models in .qvr:
• draw v : A -> K ~ Family(args) — finite-domain-indexed plate draw.
• observe r[n] ~ Family(args) for n in N — vectorised observation.
• marginalize c — program-level discrete-latent marginalisation.
• arr[idx] — Kleisli pullback gather expression inside let-bodies.
• posterior name (model) : domain -> codomain { steps return ... } — deterministic post-conditioning block whose body consumes posterior latents.
• Parametric programs: program name (G : FinSet, scale : Real, prior : Mor[A, B]) : dom -> cod ... — programs polymorphic over objects, scalars, and morphisms; denote dependent kernels Π(p:P).Kern(dom(p), cod(p)). Instantiated at each call site draw v ~ name(args) by parameter substitution + α-renaming, so each call contributes fresh latent factors to the caller's joint kernel. Supports the random-effects reuse story without tying latents across call sites.
• Let-expression builtins: cumsum, softmax, cholesky_quad_form join the existing sigmoid / exp / log / abs / softplus.
• AST nodes in quivers.dsl.ast_nodes: PlateDrawStep, VectorisedObserveStep, MarginalizeStep, LetExprIndex, PosteriorDecl; each docstring carries the Kern denotation.
• Stan-model port at src/quivers/dsl/examples/event_structure.qvr — a faithful translation of the four-class telicity × durativity latent-class model from ~/Projects/supertelicity/analysis/event-structure-induction/models/event-structure-model.stan, demonstrating crossed random effects, ordinal monotone splines, vectorised observations, and marginalize over the discrete latent class.
• tests/test_bayesian.py — 15 tests covering every new primitive and every new AST node's parse / compile round-trip, plus a compile-time smoke test on the Stan-model port.

Changed

• _walk_program_step return type widened from DrawStep | LetStep to the ProgramStep union root.
• Tree-sitter grammar regenerated (grammars/qvr/src/parser.c, grammar.json, node-types.json) to recognise the new program steps and top-level declarations.

Added

• Pattern-polymorphic schema declarations: schema r[X, Y : Cat] : (X/Y) * Y -> X. Subsumes rule with explicit parameter types and a unified domain/codomain shape.
• New SetObject variants: EnumSet(name, elements) for named-element finite sets, FreeResiduated(generators, depth, ops) for residuated category universes. New surface syntax object Atoms = {NP, S, VP} and object Cat = FreeResiduated(Atoms, depth=4, ops=[slash]).
• FreeMonoid surface form: object Free = FreeMonoid(X, max_length=4).
• TypeSlash and TypeEffectApply TypeExpr variants — residuated patterns and effect-typed types are first-class. The CatPattern AST family is removed (folded into TypeExpr).
• chart_fold(lex=, binary=, unary=, start=, depth=, effect_depth=, handlers=) primitive expression — desugared form of parser(rules=...). unary= is wired through the inside algorithm's reflexive-transitive unary-rule closure. handlers= post-composes effect handlers on the parser output as log-space transition morphisms.
• .curry_right / .curry_left postfix combinators witnessing the residuation isomorphisms; backed by quivers.core.morphisms.CurriedMorphism.
• Typeclass tower in quivers.monadic.typeclasses: Functor, Applicative, Monad, Alternative, MonadPlus, Foldable, Traversable, MonadTrans. Concrete monads (FuzzyPowersetMonad, FreeMonoidMonad, GiryMonad) subclass Monad directly.
• Stdlib effect instances in quivers.monadic.instances: Identity, Maybe, Alternative_, Continuation, State, Reader, Writer, List. All operations (pure, fmap, apply, join, bind, lift_a2, empty, alt, foldr, traverse) are concrete V-relation realisations; function-space-dependent operations encode [A → B] as a finite FinSet of cardinality |B|^|A|. Monad transformers in quivers.monadic.transformers: StateT, ReaderT, MaybeT, ContT, WriterT.
• Algebraic effects + handlers in quivers.monadic.algebraic: Operation, EffectSignature, Handler, FreeMonad. FreeMonad carrier is the bounded-depth signature-tree set realised as a flat FinSet with structural decomposition via _decompose_carrier_index / _compose_carrier_index; pure, fmap, join, bind, lift_a2 satisfy the monad laws up to truncation. Handler.run is the post-order tree fold interpreting each leaf through return_clause and each operation node through operation_clauses. EffectSignature.to_theory() and Handler.as_theory_morphism() realise the panproto-side theory and theory morphism.
• quivers.monadic.bridges: Kleisli, ArrowMonad, CoKleisli, kleisli, arrow_monad, cokleisli connecting the monad and arrow towers. Kleisli.compose is fmap-then-join with structural recovery of the underlying B; Kleisli.first is realised via the canonical monad strength σ = (pure × id) >> lift_a2(id_{A⊗B}); Kleisli.app routes through the Applicative apply. ArrowMonad provides fmap/pure/apply/join/bind/lift_a2 via the underlying arrow's arr/id_arr/app/compose. CoKleisli is registered as Category_; promoting to Arrow requires an explicit comonad costrength supplied via first_via_costrength(f, C, costrength).
• quivers.arrows package — Hughes-style arrow hierarchy (Category_, Arrow, ArrowChoice, ArrowApply, ArrowLoop, ArrowZero, ArrowPlus) with panproto-theory mirrors. New quivers.arrows.instances with VRel, Function, Stochastic arrow instances; loop_arr realised via the V-quantale iterative trace (Joyal-Street-Verity 1996, §3).
• quivers.stochastic.effect_lifts.class_directed_lifts — class-driven schema lifting for effect-typed parsers. make_swap_schema / swap_rule_set emit swap_TU schemas from registered DistributiveLaw instances for commutation firings.
• quivers.core._factories module — concrete morphism constructors inj, case, pi, pair, parallel, terminal, constant, distrib_right, coproduct_map. The algebra on which the stdlib monads, arrows, and algebraic-effects layer are built.
• New tree-sitter grammar at grammars/qvr/ with regenerated parser; the unified _type_expr family subsumes the prior _cat_pattern productions.
• Local-grammar override at quivers.dsl._dev_grammar (activated by QVR_USE_LOCAL_GRAMMAR=1) using panproto 0.47's first-class AstParserRegistry.override_grammar() API. Compiles the in-tree grammar and installs it into the standard registry when the upstream panproto-grammars-all bundle hasn't yet vendored the latest grammar source.
• docs/guides/effects.md and docs/semantics/effects.md — user guide and formal denotational layer for the typeclass + algebraic-effects framework.
• quantifier_scope.qvr example demonstrating Charlow-style scope-taking via Continuation.

Changed

• The Monad ABC is the typeclass-tower one (quivers.monadic.typeclasses.Monad); the previous parallel ABC in quivers.monadic.monads is removed. Concrete monads provide both the typeclass operations (pure, apply, join) and the Eilenberg–Moore aliases (unit, multiply).
• RuleDecl premises and conclusion are typed at TypeExpr (previously CatPattern).
• ObjectDecl admits both : type_expr and = initializer forms.
• parser(...) infers category atoms from a uniquely-declared FreeResiduated in scope when no categories= argument is supplied.
• QVR_PROGRAM_PROTOCOL extended with enum_set, free_residuated, schema_decl vertex kinds.
• InsideAlgorithm accepts an optional unary morphism; the chart fills with reflexive-transitive unary-rule closure at each cell.
• chart_fold(effect_depth>0) no longer raises CompileError; the parameter flows through as informational metadata and the caller-supplied binary morphism (typically built via lift_rule_set over declared effects) provides the lifted firings. handlers= are post-composed via _ChartHandlerComposite log-space transitions.
• Denotational-semantics docs: corrected marginalisation formulas (proper handling of residual input Y), Kleisli composition ordering in programs.md (s_1 ⋄ ⋯ ⋄ s_n ⋄ ret, not the reverse), scan formula typing in expressions.md, profunctor typing in grammar.md, the row-stochastic/column-stochastic distinction in morphisms.md, the arrow_monad ∘ kleisli ≅ id natural isomorphism in effects.md.

Fixed

• FreeMonad carrier no longer collapses under CoproductSet auto-flattening when the leaf type is itself a coproduct; the flat-FinSet representation preserves the recursive leaf-vs-operation structure.
• FreeMonad.lift_a2 is the correct free-monad applicative recursion (bi-depth (d_a, d_b, d_c) tracking with proper continuation re-encoding), replacing a prior block-identity rule that misrepresented op-summand handling.
• FreeMonad.join splices outer trees correctly through _carrier_op_offset, replacing a prior block-identity that mapped op-summand indices without accounting for the differing inner/outer continuation cardinalities.
• CoKleisli.first was type-incorrect (W(A) × C → B × C vs the required W(A × C) → B × C); now registered as Category_ only, with first_via_costrength for promotion to Arrow when a comonad costrength is supplied.
• List.fmap_obj accepts non-FinSet inputs by re-encoding via cardinality; List(List(A)) now type-checks and the monad laws hold on its own image.
• TypeCoproduct was already correctly handled at resolution.py:119; documented as such.
• Bridge round-trip claim in effects.md §7 corrected from = to ≅ (Hughes 2000 proves natural isomorphism via the 1 ⊗ A ≅ A unitor, not equality).

Upstream

• panproto/panproto#89 closed and shipped in panproto 0.47.0 — first-class runtime grammar override via AstParserRegistry.override_grammar().
• panproto/didactic#38 closed and shipped in didactic 0.7.0 — tuple[Model, ...] field types accept any dx.Model element directly (the workaround tuple-of-TaggedUnion-roots is no longer needed).
• panproto/didactic#39 closed and shipped in didactic 0.7.0 — dx.field(opaque=True) for fields typed at typeclass ABCs (Monad, ArrowApply, etc.); opaque fields preserve in-process identity through with_ but drop to None on JSON round-trip.

Dependencies

• panproto >= 0.47.0 (was >= 0.45.0).
• panproto-grammars-all >= 0.47.0 (was >= 0.45.0).
• didactic >= 0.7.1 (was >= 0.6.0).

---

Install: pip install quivers==0.4.0

Full changelog: CHANGELOG.md · Docs: https://FACTSlab.github.io/quivers