Skip to content

Producers consumers and sessions

Jump to bottom Edit New page
Sjoerd Visscher edited this page Oct 6, 2026 · 4 revisions

In a dialogue category every object A has a dual A*, and a morphism into A* is the same thing as a way to use up an A. So every output can be read as an input of the dual type, and the other way round. Several notations are built on that idea. This page puts four of them side by side, on the same three small examples:

  • the category itself, with morphisms built from the structure of a dialogue category, which is a symmetric monoidal category with a tensorial negation; a *-autonomous category is one whose negation is an involution;
  • CP, Wadler's process calculus from Propositions as Sessions, where a type is a protocol and a process has a channel for each session;
  • the μμ̃-calculus of Curien and Herbelin, the core of what is now called System L, with producers, consumers and commands;
  • SMC, the Haskell terms of Proarrow.Tools.SMC, described in Linear terms for monoidal categories.

The μμ̃ notation below is the classical, linear one with pairs. It is two-sided: a term t producing an A is typed Γ ⊢ t : A | Δ, with its inputs Γ and its outputs Δ around it, and a coterm e consuming an A is typed Γ | e : A ⊢ Δ, with the A on the left. Presentations of System L differ in the details, some are one-sided, and the polarised versions add shifts. SMC is polarised, and the section on call by push value at the end says what the shift adds; the dictionary and the examples work without it.

The dictionary

Category CP μμ̃ SMC
dual of A A* A⊥ A⊥, a convention added here Not a
makes an A morphism Γ → A process ⊢ Γ⊥, x : A term Γ ⊢ t : A | Δ Term g a
uses up an A morphism Γ → A* process ⊢ Γ⊥, x : A⊥ coterm Γ | e : A ⊢ Δ Consumer g a
a finished computation morphism Γ → ⊥ process ⊢ Γ⊥ command c : (Γ ⊢ Δ) Command g
connect the two counit A* ⊗ A → ⊥ νx.(P | Q) ⟨t | e⟩ t |> k
name an input, giving a consumer transpose (linDist) a channel μ̃x.c cont \x -> c
name an output, giving a computation transpose, into A** a channel μα.c cont \k -> c, of type Up a
make a pair f ⊗ g x[y].(P | Q) (t, u) t ** u
take a pair apart the structure maps x(y).P μ̃(x, y).c the pattern (x, y)
name two outputs at once transpose x(y).P μ(α, β).c cont \(ka, kb) -> c
two consumers as one consumer of the par doubleNegInv on A* ⊗ B* x[y].(P | Q) the pair (e, e') ret (ka, kb)
pass something on identity x ↔ y a variable a variable
a producer of A as a consumer of A⊥ doubleNegInv the same process the same term, by the convention ret
and back doubleNeg, *-autonomous only the same process the same term, by the convention classical, *-autonomous only

Three things differ between the columns. The category has no variables at all, so every wire is placed with associators, unitors and swaps. CP has only channels: a process does not return anything, and what other notations call its inputs and its output are all channels, each with its own type. μμ̃ and SMC have both sides: a term produces, a consumer consumes, and naming an output (μα) is as easy as naming an input (μ̃x). In SMC the two are one operation, cont, since a consumer of A is a term of Not a and naming the output of an a is naming the input of its consumer.

The category writes the dual as A*, as nLab does, and Dual A in Haskell; CP and μμ̃ write A⊥. The difference matters: in CP, and in the μμ̃ used here, A⊥⊥ is A by definition, while in the category A** is only isomorphic to A when the category is *-autonomous, and in a dialogue category it is a different object. SMC follows the category: Not (Not a) is a different type from a, and has a name, Up a.

Swapping a pair

The warm up has no duals in it: turn A ⊗ B into B ⊗ A.

Category. swap : A ⊗ B → B ⊗ A, one of the structure maps.

CP. The process has a channel x for the pair it receives and a channel y for the pair it sends. Receiving on x : A⊥ ⅋ B⊥ gives a new channel u for the first component, and x goes on with the second. Sending on y : B ⊗ A makes a new channel v for the first component. Then the halves are forwarded:

x(u).y[v].(x ↔ v | u ↔ y)        ⊢ x : A⊥ ⅋ B⊥, y : B ⊗ A

μμ̃. The input is a variable x : A ⊗ B, the output a covariable α that consumes B ⊗ A. A consumer takes the pair apart, and the swapped pair goes to α:

⟨x | μ̃(a, b).⟨(b, a) | α⟩⟩

SMC. The input pattern is the μ̃(a, b), and the result of the body goes to the output that μμ̃ calls α:

swapT = toSMC @(F a :** F b) \(a, b) -> b ** a

An SMC function is a μμ̃ command with one input variable and one output covariable left implicit. That makes it look like an ordinary functional program, and the classical part only shows when a consumer is named explicitly.

The shop

The example of Propositions as Sessions: a buyer sends the name of a product and a credit card number, and gets a receipt back. The paper ends every protocol in a unit, so that the channel is closed after the last message. Here the units are left out, since they only mark the end.

CP. The buyer's side of the session, and the seller's, which is its dual:

Buy  = Name ⊗ (Credit ⊗ Receipt⊥)
Sell = Name⊥ ⅋ (Credit⊥ ⅋ Receipt)

buy  = x[u].(put-name_u | x[v].(put-credit_v | x ↔ r))   ⊢ x : Buy, r : Receipt
sell = x(u).x(v).compute_{u,v,x}                         ⊢ x : Sell
deal = νx.(buy | sell)                                   ⊢ r : Receipt

x[u].(P | Q) sends a new channel u on x, served by P, and Q goes on with the rest of x. After sending the name and the card, what is left of the buyer's x is Receipt⊥: the receipt will come in on it. The buyer forwards it to its own channel r, so the receipt is the result of the whole deal. The seller receives u and v, and what is left of its x is Receipt, so compute reads the name and the card from u and v and provides the receipt on x.

μμ̃. A consumer of Receipt and a term of type Receipt⊥ are taken to be the same thing, so a consumer can be put inside a pair, and a component of type Receipt⊥ can be used as a consumer. The buyer's side of the session is then just a value, given the place ρ where the receipt should go, and the seller is a consumer that takes the order apart:

buy(ρ) = (tea, (1234, ρ))                        : Buy
sell   = μ̃(n, (c, κ)).⟨compute(n, c) | κ⟩        : consumes Buy
deal   = μρ.⟨buy(ρ) | sell⟩                      : Receipt

μρ names the output of the whole deal, and the buyer is given it and passes it on as part of its order. It ends up as the seller's κ, and the receipt is sent there.

SMC. The same three lines, with the order associated to the left instead, which is isomorphic (:** nests to the left without parentheses, and so do tuple patterns):

type Buy = F Name :** F Credit :** Not (F Receipt)
type Sell = Not Buy

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 |> seller

cont \r -> … is μρ, cont \(name, credit, toBuyer) -> … is μ̃(n, (c, κ)), and |> is the angle brackets. The only extra is compiling the seller on its own, as a piece with no inputs that piece lifts into any other term. One thing is more honest than in μμ̃: the deal has type Up (F Receipt), a computation that produces the receipt once it is told where the receipt should go, not a receipt. The tests run it by handing it a continuation.

Category. The same deal written with the structure of the category, as a morphism of linear Haskell functions:

dealByHand :: Unit ~> Dual (Dual Receipt)
dealByHand =
  dual (rightUnitorInv @_ @(Dual Receipt))
    . linDist @_ @Unit @(Dual Receipt) @Unit (dualityCounitSA @BuyObj . (sellerByHand ** buyerByHand))

sellerByHand :: Unit ~> Dual BuyObj
sellerByHand =
  dual (rightUnitorInv @_ @BuyObj)
    . linDist @_ @Unit @BuyObj @Unit
      ( dualityCounitSA @Receipt
          . swap @_ @Receipt @(Dual Receipt)
          . (computeByHand ** obj @(Dual Receipt))
          . leftUnitor @_ @BuyObj
      )

buyerByHand :: Dual Receipt ~> BuyObj
buyerByHand =
  ((tea ** card) ** obj @(Dual Receipt))
    . (leftUnitorInv @_ @Unit ** obj @(Dual Receipt))
    . leftUnitorInv @_ @(Dual Receipt)

The parts are the same as in the other notations. dualityCounitSA is the meeting of a consumer with what it consumes: the outer one is ⟨buy | sell⟩, the inner one the seller sending the receipt. Each linDist, followed by dual of a unitor, names an input: the seller's is the μ̃, and the deal's is the μ, which on the category side is the same operation, applied to the consumer of the receipt. The rest is unitors and one swap to put the wires where the next step wants them. This is roughly what toSMC generates from the SMC version, and the tests check that both give the same receipt.

A broker

A broker stands between a buyer and a seller: it reads the order from the buyer, places it with the seller, and passes the receipt back with a note. It is a process with two channels, one to each side, and so a par.

CP. The broker has a channel to each side, x to the buyer and y to the seller:

broker = x(u).x(v).y[u'].(u ↔ u' | y[v'].(v ↔ v' | annotate_{y,x}))     ⊢ x : Sell, y : Buy

It receives the name and the card on x, sends them on y, and annotate passes the receipt that comes in on y back out on x, with a note.

μμ̃. A term of A ⅋ B binds two covariables at once, μ(ξ, η).c, and is consumed by a pair of consumers. The broker is such a term of Sell ⅋ Buy, with ξ consuming the buyer's side and η the seller's:

broker = μ(ξ, η).⟨ξ | μ̃(n, (c, κ)).⟨(n, (c, μ̃r.⟨annotate(r) | κ⟩)) | η⟩⟩

ξ consumes Sell, so with the convention above it is the buyer's order itself. The consumer takes the order apart and sends it on to η, with a new place for the receipt that annotates it and passes it to κ.

SMC. μ(ξ, η) is cont with a pair pattern, the output side's mirror of cont \(name, credit, toBuyer): a pattern for an output takes apart a par, as one for an input takes apart a tensor. SMC keeps a consumer of Sell apart from a producer of Buy, so the step that the convention hides is visible: fromBuyer has type Not Sell, which is Up Buy, a computation that produces the order, and binding it in the do block runs it.

broker = piece $ toSMC @I @(Not Buy :## Buy) \() -> cont \(fromBuyer, toSeller) -> SMC.do
  (name, credit, toBuyer) <- fromBuyer
  name ** credit ** cont (\receipt -> annotate receipt |> toBuyer) |> toSeller

The whole system connects the broker to both. In μμ̃ it is μρ.⟨broker | (buy(ρ), sell)⟩: the par is consumed by a pair, the buyer's order on one side and the seller on the other. In SMC the buyer's order becomes a consumer of Sell with ret, double negation introduction, and the rest reads the same:

brokeredDeal = toSMC \() -> cont \r -> ret (buyer r) ** seller |> broker

Call by push value

The dictionary above is about the two sides, producers and consumers. SMC's types also have a polarity: Not a is negative, everything else is positive, and the shift from positive to negative is Up a = Not (Not a). That is the other calculus hiding in the same terms, Levy's call by push value, and it has its own small dictionary, on a different axis:

CBPV polarised μμ̃ SMC Category
value type, computation type positive, negative not a Not, a Not object, algebra of ¬¬
F A ↑A Up a A**
return V μα.⟨V | α⟩ ret v doubleNegInv
M to x. N ⟨M | μ̃x.N⟩ x <- m in a do block bindDual
U B, thunk, force ↓B Dn n, thunk, force the same object
λx.M, V'M lam, ! curry, apply

A value is a term of a positive type and a computation is a term of an Up. ret turns a value into the computation that produces it, and a do bind of a computation runs it, with the rest of the block, which must be negative, as what happens next. That is where the terms get an evaluation order, which a symmetric monoidal category does not have by itself. thunk and force change the polarity and nothing else: Dn n stands for the same object as n, so on the morphism both are the identity, as they are in every model of CBPV given by a monad. What they decide is whether a bind runs the term: t <- thunk m names the computation, () <- force t runs it. A computation of a computation, Up (Not a), is not the same as Not a, just as m (m a) is not m a for a monad; what exists is the map running it into one, tripleNeg, the join of the ¬¬ monad, which CBPV writes M to x. force x.

The two dictionaries meet in the targets. Over the Kleisli category of the continuation monad, which is *-autonomous, Up a is isomorphic to a through classical, every term is a computation, and the polarity collapses into the two-sided picture above. Over pure functions with IO () as the answer object (Proarrow.Category.Instance.Cps), Up a is (a -> IO ()) -> IO (), a different type from a, the morphisms are pure, and the effects happen exactly at the binds. test/Examples/Cbpv.hs runs the same programs there: two actions made in one order and run in the other, a computation stored with thunk, copied and run twice, a computation that is made and dropped and so never happens, and a function whose effect happens at each application.

What SMC adds

  • Checked resources. A variable, input or output, used more than once or not at all needs a comonoid on its type, and GHC checks it. In the category this is automatic, in CP and μμ̃ it is part of the type system on paper.
  • Messages are values. Session types need no units to end a protocol, and a pattern takes a whole message apart at once: \(name, credit, toBuyer) -> instead of one receive per component.
  • Any dialogue category. The same terms run in linear Haskell functions, relations, the continuation monad's Kleisli category, or pure functions with an answer object of effects, and draw as string diagrams. The category column above is what they turn into.
  • No definitional A⊥⊥ = A. Up a is its own type, a computation, and binding it is where it runs. classical collapses it to a when the category is *-autonomous.

The shop and the broker are in test/Examples/Sessions.hs, with the by-hand version next to them.

Further reading

Add a custom footer
Add a custom sidebar

Clone this wiki locally