Quivers

A functional probabilistic programming language for PyTorch.

Quivers is a functional probabilistic programming language for PyTorch. The syntax will look familiar if you have used Pyro, NumPyro, Stan, or PyMC, with a few distinguishing features:

  • Programs are first-class composable typed values. A program has a domain, codomain, algebra, and effect signature (Sample, Score, Marginal, Pure), checked at compile time. Programs compose with >>, parallel-compose with @, change base across algebras with change_base, and marginalize discrete latents with marginalize z : K <- ... followed by an indented body.
  • Shared substrate for inference, deduction, and structural compression. A CKY parser written as a deduction block, a transformer-as-encoder over a signature block, and a Bayesian regression all compile to the same underlying semantics, with the same composition operators, and can therefore compose with each other.
  • Algebra-parametric semantics. Programs can be parameterized by eleven built-in or user-defined algebras. Homomorphisms between algebras are values you can transport models along, with the laws checked at compile time.

It also has some features you are used to from other PPLs:

  • An inference toolkit. Forty distribution families. SVI with nine automatic guides (mean-field through full-rank multivariate normal, low-rank, mixture, IAF, neural-spline flow, AutoDAIS) and four objectives (ELBO, IWAE, Renyi, VR-IWAE) with reparameterized, score-function, sticking-the-landing, and DReG gradient estimators. NUTS and HMC with dual-averaging step-size adaptation and Welford mass-matrix adaptation.
  • An analysis toolkit. Static introspection of compiled programs (per-step algebra, chain depth, intermediate shape, source mapping); algebra-aware, saturation-free initialization recipes that adapt to whichever value algebra a program is parameterized over; compile-time diagnostics flagging latents whose default initialization would saturate the active algebra.
  • Diagnostics and model comparison. ArviZ ecosystem integration: posteriors from any inference method (NUTS, HMC, or SVI) export to ArviZ for trace plots, rank plots, ESS, and \(\hat R\). PSIS-LOO (Pareto-smoothed importance-sampling leave-one-out cross-validation) for ranking competing models; posterior-predictive checks against user-defined test statistics; LOO-PIT for calibration.
  • A mixed-effect model API. A brms-style formula frontend for mixed-effect regression compiles formulas to typed QVR programs through a bidirectional lens, taking pandas / polars dataframes as input and using R-canonical conventions (orthogonal polynomials, R-style transforms in the formula evaluation namespace) as defaults. The emitted QVR is inspectable, so a formula-fitted model is a starting point you can hand-edit rather than a closed black box.
  • Interactive tooling out of the box. qvr repl is a GHCi-style four-pane Textual TUI with live syntax highlighting, env browser, file-watcher auto-reload, command palette, and meta-commands (:type, :info, :browse, :edit, :save, :watch, …). qvr-lsp is a full LSP 3.17 language server (hover, definition, references, document symbols, semantic tokens, completion, formatting, live diagnostics) that VS Code, Cursor, Zed, and Neovim consume out of the box. A Jupyter kernel (qvr-kernel install) drives the same elaborator from notebooks.

Quick start

object Item : FinSet 100
# Predictor `x` flows in as exogenous data via the observations
# dict; free variables in `let` expressions resolve from the
# conditioning data at trace time (host-data channel).
program regression : Item -> Item [effects=[Sample, Score]]
    sample sigma  <- HalfNormal(1.0)
    sample beta_0 <- Normal(0.0, 5.0)
    sample beta_1 <- Normal(0.0, 2.0)
    let mu = beta_0 + beta_1 * x
    observe y : Item <- Normal(mu, sigma)
    return y

export regression

from quivers.dsl import load
from quivers.inference import AutoNormalGuide, ELBO, SVI
import torch

program = load("docs/examples/source/bayesian_regression.qvr")
model   = program.morphism
guide   = AutoNormalGuide(model, observed_names={"y"})
optim   = torch.optim.Adam(guide.parameters(), lr=1e-2)
svi     = SVI(model, guide, optim, ELBO())
# Training loop (illustrative shape; pass real x_data, y_data in practice).

The same regression also expresses through a brms-style formula frontend:

from quivers.formulas import fit
# Call shape: fit("y ~ x + (1 | g)", data=df, family="gaussian", method="nuts")
# returns a result with a `.dump_qvr(path)` method for inspecting the emitted QVR.
print(fit.__name__)

Where to start

  • Installation for setup.
  • Quickstart for a working model in five minutes.
  • QVR tutorial for probabilistic-programming users: seven chapters from linear regression through hierarchical models, sequence models, and inference-algorithm choice, with Pyro / NumPyro / Stan equivalents side-by-side.
  • Python API tutorial for library developers and category-theory-fluent users: seven chapters covering the typed categorical API.
  • Examples gallery: 36 end-to-end models grouped by family.
  • Conceptual guides for feature-area deep dives.
  • API reference for the typed Python API.
  • Denotational semantics for the formal meaning of every well-typed program.

Architecture

The DSL is a thin layer over a typed categorical API. If you want to extend the library, write a new distribution family, or prove anything about a model, the categorical layer is what you read. If you just want to fit models, you can ignore it.

The library decomposes into eight layers. Each is consumable in isolation; each builds on those below it:

flowchart TB
    L8["Layer 8: QVR DSL<br/>.qvr files, tree-sitter grammar, panproto AST"]
    L7["Layer 7: Structural compression<br/>signature, encoder, decoder, loss blocks"]
    L6["Layer 6: Inference<br/>guides, objectives, MCMC kernels, hybrid samplers"]
    L5["Layer 5: Continuous probabilistic programs<br/>MonadicProgram, distribution families, flows, plates"]
    L4["Layer 4: Stochastic morphisms<br/>Markov kernels, Giry monad, chart deduction surface"]
    L3["Layer 3: Monadic and enriched constructs<br/>monads, algebras, ends, coends, Kan, profunctors"]
    L2["Layer 2: Categorical structure<br/>functors, naturals, adjunctions, monoidal, traced"]
    L1["Layer 1: Core V-enriched algebra<br/>FinSet, Morphism, CompositionRule hierarchy, wiring"]
    L8 --> L7 --> L6 --> L5 --> L4 --> L3 --> L2 --> L1

The central abstraction is a morphism between finite sets, parameterized by an algebra (a complete lattice with a monoidal product distributing over joins). A morphism f : A -> B is a PyTorch tensor of shape (|A|, |B|) whose entries take values in the algebra; composition f >> g contracts along the shared dimension under the algebra's tensor product and join. Different algebras give different composition semantics: Boolean composes by AND / OR (relational composition), ProductFuzzy by multiplication / noisy-OR, Real by sum-product, Markov by row-stochastic kernel composition, and so on.

The denotational semantics gives every well-typed QVR phrase a formal meaning in a \(\mathcal{V}\)-enriched symmetric monoidal closed category. The implementation rests on enriched category theory (Kelly, 1982), the categorical foundations of probability (Giry, 1982; Fritz, 2020), and the SVI / HMC inference substrate (Hoffman, Blei, Wang & Paisley, 2013; Neal, 2011; Hoffman & Gelman, 2014).

References

  • Tobias Fritz. 2020. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239.
  • Michèle Giry. 1982. A categorical approach to probability theory. In Bernhard Banaschewski, editor, Categorical Aspects of Topology and Analysis, volume 915 of Lecture Notes in Mathematics, pages 68–85. Springer, Berlin, Heidelberg.
  • Matthew D. Hoffman and Andrew Gelman. 2014. The No-U-Turn Sampler: adaptively setting path lengths in Hamiltonian Monte Carlo. Journal of Machine Learning Research, 15(47):1593–1623.
  • Matthew D. Hoffman, David M. Blei, Chong Wang, and John Paisley. 2013. Stochastic variational inference. Journal of Machine Learning Research, 14(40):1303–1347.
  • Gregory M. Kelly. 1982. Basic Concepts of Enriched Category Theory. Cambridge University Press; reprinted as Reprints in Theory and Applications of Categories 10 (2005):1–136.
  • Radford M. Neal. 2011. MCMC using Hamiltonian dynamics. In Steve Brooks, Andrew Gelman, Galin L. Jones, and Xiao-Li Meng, editors, Handbook of Markov Chain Monte Carlo, chapter 5. Chapman & Hall/CRC.