Repository navigation
Programming with monoidal categories
Proarrow.Tools.SMC lets you program with named wires in any symmetric monoidal category. Ordinary Haskell functions, tuple patterns and do blocks describe how existing morphisms connect. The notation mirrors Haskell's arrow notation, but works beyond the Arrow interface: the wires can be qubits, audio signals, matrix indices or objects of another category.
A term records in its type which variables it uses. Using a variable once is a wire; using it twice copies it, and leaving it unused discards it. The types ask for copying and discarding on that object's type where they are needed. Variables can be reused or left unused when the category permits it, without requiring every object to support those operations.
The same program can be interpreted in different categories. This page starts with a Toffoli circuit run as matrices, ZX diagrams and string diagrams, then uses feedback to make an audible echo with Yampa and to compose morphisms in the Int construction. Further structure adds functions in closed categories, duals in compact closed categories, inputs and outputs in dialogue categories, sessions, and the additives.
Two further worked examples develop this approach: A clocked digital circuit follows a counter from feedback and registers to simulation and Verilog; From a build pipeline to a parallel schedule reads one dependency graph into sequential and concurrent builds, with diagrams and measured timelines.
The design follows Jean-Philippe Bernardy and Arnaud Spiwack, Evaluating Linear Functions to Symmetric Monoidal Categories (Haskell Symposium 2021): their ports are SMC's terms, encode is lift, decode is toSMC, and their !: is **. SMC records only the variables a term uses, rather than the whole surrounding context, so combining terms connects those wires, with copying where a variable is shared.
This example is ported from the examples of linear-smc, the library that accompanies Bernardy and Spiwack's paper.
The Toffoli gate flips its third qubit when the first two are both set. As a circuit it is built from Hadamard, T and T† gates and six controlled-nots. The gates are passed in as a record of morphisms, so the circuit can be compiled in any category that has them:
data Gates q = Gates
{ hadamardG :: q ~> q
, tG :: q ~> q
, tInvG :: q ~> q
, cnotG :: q ** q ~> q ** q
}
toffoliWith :: forall {k} (q :: k). (SymMonoidal k, Ob q) => Gates q -> q ** q ** q ~> q ** q ** q
toffoliWith (Gates h t t' controlledNot) = toSMC @(F q :** F q :** F q) @(F q :** F q :** F q) \(a0, b0, x0) -> SMC.do
(a1, x1) <- cnot a0 (h -< x0)
(b1, x2) <- cnot b0 (t' -< x1)
(a2, x3) <- cnot a1 (t -< x2)
(b2, x4) <- cnot b1 (t' -< x3)
(b3, a3) <- cnot b2 (t -< a2)
(b4, a4) <- cnot (t -< b3) (t' -< a3)
a4 ** b4 ** (h -< t -< x4)
where
cnot :: (Merge g1 g2) => Term d g1 (F q) -> Term d g2 (F q) -> Term d (Union g1 g2) (F (q ** q))
cnot c x = controlledNot -< (c, x)-< applies a morphism to a term or tuple of terms, mirroring Haskell's arrow notation: h -< x0 applies the Hadamard gate, and controlledNot -< (c, x) applies a controlled-not to two qubits. ** puts two terms side by side, and toSMC turns the whole function into a morphism from three qubits to three qubits. The do block is Proarrow.Tools.SMC's own, used with QualifiedDo (import Proarrow.Tools.SMC qualified as SMC): each bind takes a pair apart with a pattern, which can be nested, and binds the halves as new variables. A controlled-not returns its two qubits as a pair, so each bind gives them new names: a0, a1, … are the first qubit at successive steps, and b0, b1, … and x0, x1, … the other two.
- In
Mat, gates are complex matrices, and the compiled morphism is checked against the Toffoli matrix on every basis state. - In
ZX, the ZX calculus, gates are spiders, and the result agrees with the Toffoli gate up to a scalar, the usual convention there. - In
SVG, gates are boxes, and the result is a string diagram:
type SQ = S '[Wire "q"]
svgGates :: Gates SQ
svgGates =
Gates
{ hadamardG = node "H"
, tG = node "T"
, tInvG = node "T†"
, cnotG = (obj @SQ ** node @'[Wire "q", Wire "q"] @'[Wire "q"] "⊕") . (comult @SQ ** obj @SQ)
}The controlled-not copies the control with a point (comult) and joins the copy to the target in a ⊕ box. The picture on the right is render (toffoliWith svgGates).
The diagram is the term, drawn as the term builds it. Between two gates the wires are ordered by when their variables were introduced, oldest on the left. The two qubits coming out of a controlled-not are new variables, so they continue on the right, and the qubit the gate did not touch moves left to make room. The few crossings in the picture are those moves: each is a swap the term performs.
The complete example is test/Examples/Toffoli.hs.
Arrow notation is often used for functional reactive programming: variables name signals, and a recursive binding connects an output back to an input. SMC can describe the same signal networks. A feedback echo needs just a mixer and a delay:
echoWith mix delay = proc @(F a) @(F a) \input -> SMC.do
rec output <- mix -< (input, delay -< output)
returnA -< outputmix adds the input to half of the delayed output. delay holds 0.3 seconds of audio, initially filled with silence. A sound comes back after 0.3 seconds at half its amplitude, then after 0.6 seconds at a quarter, and so on. The positive delay breaks the instantaneous dependency: the network can produce a sample before it needs that sample back.
output is used before it is bound, so rec feeds it back. It is also the result, so the output wire is copied: one copy goes to the listener and the other to the delay. The source names these connections without managing an audio buffer or rearranging tuples.
For audio, the supplied arrows are Yampa signal functions wrapped in Arr. The wrapper lets SMC use their Arrow and ArrowLoop instances, and proc compiles the term back into a computation:
echo :: Double -> Double -> SF Double Double
echo seconds gain =
unArr (echoWith (Arr (arr (\(dry, wet) -> dry + gain * wet)))
(Arr (delay seconds 0)))For the picture, the supplied arrows are boxes in SVG. The same echoWith draws their connections, including the feedback wire:
echoPicture =
render (echoWith @(S '[Wire "audio"])
(node "mix: dry + 0.5 wet")
(node "delay: 0.3 s"))The example plays a short arpeggio through this network. Listen to the dry tune, then the tune with echo.
To render the files locally, run from the repository root:
cabal run smc-audio -- /tmp/proarrow-audioPlay dry.wav, then echo.wav from that directory to hear the repeating echoes. Both files contain five seconds of mono audio at 44,100 Hz; the tune stops after two seconds, leaving time for the echo to fade. The command also writes echo.svg.
The complete example is tools/smc-audio/SmcAudio.hs, with the renderer and usage instructions beside it.
A traced monoidal category can feed an output back into an input: its trace turns a morphism x ** u ~> y ** u into a morphism x ~> y. In Haskell's own category the trace is a lazy fixed point, the same knot that mdo and rec tie for monads. Proarrow.Tools.SMC uses that syntax for the same purpose. With RecursiveDo, a rec block in an SMC.do block is traced: the variables it uses before binding them are fed back, and the others are passed on to the rest of the block.
The Int construction turns a traced monoidal category into a compact closed one. An object is a pair of objects I plus minus, and a morphism from I ap am to I bp bm is a morphism ap ** bm ~> am ** bp of the underlying category: the plus parts flow forwards, the minus parts backwards. Composing two of them connects them along the middle object, in both directions at once, which is a trace:
Int @bp @bm @cp @cm f . Int @ap @am g =
Int $ toSMC @(F ap :** F cm) \x -> SMC.do
let g' = lift @(F ap :** F bm) @(F am :** F bp) g
f' = lift @(F bp :** F cm) @(F bm :** F cp) f
(ap, cm) <- x
rec ((am, bp), (bm, cp)) <- g' (ap ** bm) ** f' (bp ** cm)
am ** cpg and f run side by side. g needs bm, which only f produces, and f needs bp, which only g produces. Both are used in the rec statement before its pattern binds them, so both are fed back, and am and cp go on to the result.
The picture is this composition over string diagrams, which are traced too: each fed back wire loops round the side of the diagram it is nearest to. It is render of Int f . Int g, with f and g two boxes:
type W1 s = S '[Wire s]
gInt :: IntConstruction (I (W1 "a⁺") (W1 "a⁻")) (I (W1 "b⁺") (W1 "b⁻"))
gInt = Int (node @'[Wire "a⁺", Wire "b⁻"] @'[Wire "a⁻", Wire "b⁺"] "g")
fInt :: IntConstruction (I (W1 "b⁺") (W1 "b⁻")) (I (W1 "c⁺") (W1 "c⁻"))
fInt = Int (node @'[Wire "b⁺", Wire "c⁻"] @'[Wire "b⁻", Wire "c⁺"] "f")The composition is in Proarrow/Category/Instance/IntConstruction.hs, and the picture in test/Examples/IntComposition.hs.
In a closed category terms can be functions. lam binds a variable, and ! applies a function term to an argument term. Swapping the arguments of a curried function takes a dozen lines of curry, apply and associators when written by hand, and one line as a term:
flipExp :: (x ~~> (m ~~> a)) ~> (m ~~> (x ~~> a))
flipExp = toSMC @(F x :-> F m :-> F a) @(F m :-> F x :-> F a) \f -> lam \m -> lam \x -> f ! x ! mSMC can alo be used as a language for cartesian closed categories: PROD k is the same category as k except with products as its tensor
operation, so using SMC in this category automatically gives you this language. Proarrow.Tools.CCC does exactly this, its exported functions
are SMC's wrapped in PROD.
A variable used twice is copied, which needs its type to be a cocommutative comonoid, and a variable that is never used is discarded, which needs a comonoid. The reader monad (the exponential by a comonoid m) copies its environment i to both sides:
-- ignore the environment
one = toSMC @I @(F m :-> I) \u -> lam (const u)
-- give a copy of the environment to each side
l ** r = toSMC @(F x1 :** F y1) @(F m :-> F x2 :** F y2) \(x, y) ->
lam \i -> (l -< x) ! i ** (r -< y) ! iCopying a variable copies the value it stands for, which is not the same as running the term that made it twice: in relations, say, copying after a relation h differs from running h on two copies of its input. A do bind computes its right hand side once and binds the result to a variable, so y <- lift h x followed by y ** y copies the value, while a Haskell function that uses its argument twice, given lift h x, runs h twice.
When every index type is a special commutative Frobenius algebra, as in a hypergraph category, terms can be written in index notation, as with Einstein summation. Using an index twice copies it, so both uses see the same value. sumOver binds an index that is summed over, delta says two wires carry the same value, and *^ multiplies a term by a scalar, a term of type I. A summed index that the term also returns is an output index, so matrix multiplication is:
matMulT f g = toSMC @(F a) @(F c) \i -> sumOver \k -> sumOver \j ->
delta (f -< i) j *^ delta (g -< j) k *^ kIn matrices this is the product, in relations the sum is "there is" and the product is composition of relations, and in the diagram categories it draws the tensor network. The tests are in test/Props/SMC.hs.
In a compact closed category a pair of wires, one the dual of the other, can be created from nothing and joined back into nothing. produce creates the pair, and annihilate joins a dual with its wire. With them, a wire can be bent back on itself, and bending it twice gives back the wire, which is the zigzag law. On the dual of a it reads:
snakeDualT :: Dual a ~> Dual a
snakeDualT = toSMC @(Not (F a)) \x -> SMC.do
(a, a') <- produce
() <- annihilate x a
a'The picture is this term over string diagrams: produce is the cup, and annihilate the cap. The snake on a itself, which joins the input with the second end of the pair, is the same shape with one crossing, because a new pair always sits to the right of the wires that were there before.
The same two operations give a trace in any compact closed category, without a trace of its own: feed the value in along one end of a new pair, and join its new value with the other end.
loopCC :: (a ** u ~> b ** u) -> a ~> b
loopCC h = toSMC @(F a) \a -> SMC.do
(u, u') <- produce
(b, v) <- lift @(F a :** F u) @(F b :** F u) h (a ** u)
() <- annihilate u' v
bA dialogue category has duals too, a negation Not, but no way to create a pair of wires from nothing, and joining a dual with its wire gives the unit of par, Not I, rather than the unit. A term of Not a then consumes an a: it is an output of type a, seen as an input. This is how System L, the μμ̃-calculus, reads its terms, and it treats inputs and outputs alike:
- A
Termofaproduces ana, and aConsumerofa, a term ofNot a, consumes one. -
t |> ksends the producertinto the consumerk(cut k tis the same, the other way round). The result is aCommand, a term ofNot I. -
cont \x -> cis a term ofNot a: it receives anathrough the patternxand runs the commandcwith it. What thatais depends on how the result is used. As a consumer ofa, theais an input andcontis the μ̃ of System L; the seller below receives an order this way. As a term of the negative typeNot ain its own right, theais the consumer of an output andcontis μ, Haskell'scallCC: a computationUp breceives the consumer of its result,cont \k -> … |> k, a parb :## creceives a consumer for each side,cont \(kb, kc) -> …, and a command,Not I, receives nothing,cont \() -> ….
The types have a polarity: Not a is negative, everything else positive, and Up a = Not (Not a) is a computation that will produce an a. Binding an output of type a with cont gives an Up a, since the only way to use an output is to have a consumer for it. ret turns a value into the computation that produces it, and binding a computation in a do block runs it. Only a *-autonomous category, whose negation is an involution, collapses Up a back to a, with classical.
This reading is also the one of Wadler's Propositions as Sessions, where a type describes a protocol, a process has a channel for each of its sessions, and connecting two processes on a channel is a cut. Its example is a shop. The buyer sends the name of a product and a credit card number, and gets a receipt back:
type Buy = F Name :** F Credit :** Not (F Receipt) -- Name ⊗ Credit ⊗ Receipt⊥
type Sell = Not Buy
piece p = lift @I p unit -- a separately compiled process with no inputs
buyer r = put "tea" ** put 1234 ** r
seller = piece $ toSMC \() -> cont \(name, credit, toBuyer) -> compute (name ** credit) |> toBuyer
deal = toSMC @I @(Up (F Receipt)) \() -> cont \r -> buyer r |> sellerReceiving a message is taking a tensor apart, and replying is sending into a consumer that came with the order. The buyer passes on where its receipt should go, r, and the seller sends the receipt there. The session of the seller is the dual of the buyer's, so the two meet in one |>, and cont \r makes the deal a computation that produces the receipt that ends up in r. Run in Linear Haskell functions with a continuation for the receipt, deal gives "tea, paid with 1234".
A process with two channels is a par: a :## b in a term's type and Par a b in the category, built with cont and a pair pattern, cont \(ka, kb) -> …, and consumed by ret (ka, kb), a pair of consumers as a consumer of the par. Producers, consumers and sessions shows it on a broker between the buyer and the seller, and goes through all of this more slowly, next to CP, the μμ̃-calculus and the category itself. The shop and the broker are in test/Examples/Sessions.hs, and the double negation maps, the symmetry of par and linear distributivity among the examples of Proarrow.Tools.SMC.
The additives are the product, whose two alternatives share their inputs and only one of which will be used, and the coproduct, taken apart by case analysis. A variable that several alternatives use is shared, not copied, and one that an alternative does not use is discarded there. with s t pairs two terms, and caseOf x f g takes the coproduct x apart, with a function for each branch that receives the contents of its alternative through a pattern. With RebindableSyntax enabled, caseOf can be written with if-then-else. Distributivity itself is a case analysis where both branches use a:
distT :: a ** (b || c) ~> (a ** b) || (a ** c)
distT = toSMC @(F a :** (F b :|| F c)) \(a, bc) ->
if bc
then \b -> inl (a ** b)
else \c -> inr (a ** c)With with, one alternative keeps the pair and the other swaps it, without requiring a and b to be Comonoids:
bothWaysT :: a ** b ~> (a ** b) && (b ** a)
bothWaysT = toSMC @(F a :** F b) \(a, b) -> (a ** b) `with` (b ** a)exl and exr project out of a product, inl and inr inject into a coproduct, and the units Top and Zero have absorb and absurd.
The examples are in Proarrow/Tools/SMC.hs, and their tests in test/Examples/LinearLogic.hs.
- Jean-Philippe Bernardy and Arnaud Spiwack, Evaluating Linear Functions to Symmetric Monoidal Categories, Haskell Symposium 2021: the paper SMC is based on, and its library linear-smc.
- Producers, consumers and sessions: the inputs-and-outputs part of SMC next to CP, the μμ̃-calculus and the category itself, with call by push value at the end.