Monoidal Adventures
summary
A prototype brat language encodes quantum circuits as composable monoidal pieces and enforces wiring with thinnings as bitvectors so selection and composition are decidable locally rather than via global unification. It separates kernel designs ($ kind) from higher‑order values, uses nouns/verbs/patterns for silent forcing and silent vectorization of replicated designs, and carries bounded dependent lengths via a numeric fragment where full(n)=2^n−1 so parity and predecessor are decidable. The system runs as a working prototype and aims to avoid heavy SAT or Gaussian elimination for most common circuit sizing.
AI-written summary · about
chapters (7)
- 0:00Welcome to monoidal adventures
- 1:05Quantum programming journey
- 3:55Prioritize monoidal structure
- 7:27Adventure one: Thinning monoidal category
- 17:39Adventure two: Monoidal functional programming in Brat
- 27:23Dependent types in Brat
- 38:08Key insights and future adventures
related talks
42mMonoidal Parsing
33mDeriving a Kronecker-Free Functional Quantum Simulator
34mThe Monoiad: an epic poem on monoids
01h 01mFunction Composition in Programming Languages
01h 33mComposition Intuition II
31mAbstract nonsense
57mApplied category theory and abstract algebra
42mEvaluating Linear Functions to Symmetric Monoidal Categories