Linear terms for monoidal categories
Proarrow.Tools.SMC builds morphisms of any symmetric monoidal category from ordinary Haskell functions on terms. Every variable must be used exactly once, and the types check this: the functions on terms are linear, and a term records which variables it uses, so using one twice, or not at all, doesn't compile. A variable is then just a wire, and nothing is copied or thrown away unless the term says so. 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 differs in what the context in a term's type is: theirs is the whole context, the same for every port, so a term's type mentions variables it does not use and splitting is a projection in a cartesian structure that is shown afterwards to be used only monoidally; SMC's is exactly the variables the term uses, so merging two terms only reorders wires.
The same terms get more features as the category gets more structure. This page starts with the Toffoli gate, in a symmetric monoidal category, and composition in the Int construction, where recursive do gives terms for traced monoidal categories. Then it goes through the rest of linear logic: functions in closed categories, copying where the category allows it, duals in compact closed categories, inputs and outputs in dialogue categories, with sessions as an example, and the additives.
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 = toSMC @(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
h, t, t' :: Term d g (F q) %1 -> Term d g (F q)
h = lift (hadamardG gates)
t = lift (tG gates)
t' = lift (tInvG gates)
cnot :: (Merge g1 g2) => Term d g1 (F q) %1 -> Term d g2 (F q) %1 -> Term d (Union g1 g2) (F q :** F q)
cnot c x = lift (cnotG gates) (c ** x)lift turns a morphism of the category into a function on terms, so the gates become functions h, t, t' and cnot; ** 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.
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, which the body must use exactly once, 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 ! mThe objects the exponentials need are found from the type annotations, so there are no withObExp calls to write.
A variable can't be used twice, but a value whose type is a comonoid can be copied and discarded explicitly: (x1, x2) <- dup x gives two copies, and () <- drop x uses x up. The pattern () takes apart a term of the unit type. 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 \i -> SMC.do () <- drop i; u
-- give a copy of the environment to each side
l ** r = toSMC @(F x1 :** F y1) @(F m :-> F x2 :** F y2) \xy -> SMC.do
let l' = lift @(F x1) @(F m :-> F x2) l
r' = lift @(F y1) @(F m :-> F y2) r
(x, y) <- xy
lam \i -> SMC.do
(i1, i2) <- dup i
l' x ! i1 ** r' y ! i2
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
buyer r = put "tea" ** put 1234 ** r
seller = closed $ 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. Alternatives that share variables can't be written as parts of one linear function, so they are functions of their own, and what they share is passed in as one term. with f g s pairs two functions of s, and caseOf e x f g takes the coproduct x apart, giving the shared term e to whichever branch runs, paired with the contents of its alternative. Like the argument of toSMC, each of these functions can take its input apart with a pattern. Distributivity itself is a case analysis where the shared term goes to both branches:
distT :: a ** (b || c) ~> (a ** b) || (a ** c)
distT = toSMC @(F a :** (F b :|| F c)) \(a, bc) ->
caseOf a bc (\(a', b) -> inl (a' ** b)) (\(a', c) -> inr (a' ** c))With with, each alternative takes the same pair apart in its own way. Here one keeps the pair and the other swaps it:
bothWaysT :: a ** b ~> (a ** b) && (b ** a)
bothWaysT = toSMC @(F a :** F b) \p -> with (\q -> q) (\(x, y) -> y ** x) pexl 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.