pacta/session/patterns

Reusable protocol fragments, and the duality witnesses that go with them.

A fragment is an ordinary protocol from pacta/session/core with one extra type parameter: then, standing for whatever follows it. That single convention is what makes protocols composable, and it is worth understanding before reading anything else here.

Composition is type application

Sequencing two protocols means replacing the first one’s Done with the second. That is a substitution, and Gleam’s type system cannot perform substitutions. But it does not have to: if a fragment leaves a hole where its continuation goes, sequencing is just filling the hole.

/// Ask once, then whatever comes next.
pub type Request(question, answer, then) =
  core.Send(question, core.Recv(answer, then))

/// Ask twice, then stop. No combinator involved.
pub type AskTwice =
  Request(String, Int, Request(String, Int, core.Done))

The same holds for the proofs. A fragment’s witness takes the continuation’s witness and returns the whole one, so composing two fragments is composing two functions:

pub fn ask_twice() -> Dual(AskTwice, ServeTwice) {
  patterns.request(patterns.request(duality.done()))
}

This is why there is no combinators module and no seq operator. Both would be a wrapper around something the language already does: type application in one case, function application in the other. Writing your own fragments needs nothing from this module beyond the convention.

There is a second reason. A general seq would have to apply a fragment whose type variables are instantiated differently at each use, which needs rank-2 polymorphism. Gleam does not have it, so fn(f) { fn(x) { f(f(x)) } } does not type check for any real fragment. Nesting at the call site is unaffected and has no depth limit; only abstracting over the nesting is out of reach.

What cannot be composed this way

Iteration. A protocol that repeats needs its own name to appear inside its own definition, and Gleam rejects that outright as a type cycle. No arrangement of parameters gets around it, because the hole would have to be filled with the very thing being defined. Repetition has to be flattened into a state graph with an edge back to an earlier marker, which is a generator’s job rather than a type’s.

Interleaving. Filling a hole can only put one protocol after another. It cannot weave two protocols together, which is what you need when a service and the authentication it depends on have to advance in step: the login must precede the menu, and each payment needs its own second factor. No arrangement of then parameters expresses that, because the two protocols constrain each other in both directions.

This is a real gap rather than an impossibility. Bocchi, Orchard and Voinea’s A Theory of Composing Protocols (2023) resolves it by annotating protocols with assert / require / consume contact points and computing the valid interleavings, yielding a single protocol to program against. Because the result is one ordinary protocol, it needs nothing from the type system: it belongs in a specification-time generator, alongside the flattening that iteration also needs. See docs/Session_Types.md.

pub type Coordinator =
  patterns.Coordinate(Transaction, Vote, Outcome, core.Done)

pub type Coordinate(proposal, vote, outcome, then) =
  core.Send(proposal, core.Recv(vote, core.Send(outcome, then)))

pub type Decide(proposal, accepted, rejected) =
  core.Recv(proposal, core.Choose(accepted, rejected))

pub type Participate(proposal, vote, outcome, then) =
  core.Recv(proposal, core.Send(vote, core.Recv(outcome, then)))

/// Offer a price. If they take it, settle up; if not, we are done.
pub type Haggle =
  patterns.Propose(Price, patterns.Request(Card, Receipt, core.Done), core.Done)

pub type Propose(proposal, accepted, rejected) =
  core.Send(proposal, core.Offer(accepted, rejected))

/// Look up a balance, then hang up.
pub type Lookup =
  patterns.Request(AccountId, Money, core.Done)

pub type Request(question, answer, then) =
  core.Send(question, core.Recv(answer, then))

pub type Teller =
  patterns.Serve(AccountId, Money, core.Done)

pub type Serve(question, answer, then) =
  core.Recv(question, core.Send(answer, then))

pub fn coordinate(
  then: duality.Dual(a, b),
) -> duality.Dual(
  core.Send(proposal, core.Recv(vote, core.Send(outcome, a))),
  core.Recv(proposal, core.Send(vote, core.Recv(outcome, b))),
)

/// Two rounds of two-phase commit over the same channel.
let proof = patterns.coordinate(patterns.coordinate(duality.done()))

pub fn decide(
  accepted: duality.Dual(a, b),
  rejected: duality.Dual(c, d),
) -> duality.Dual(
  core.Recv(proposal, core.Choose(a, c)),
  core.Send(proposal, core.Offer(b, d)),
)

pub fn participate(
  then: duality.Dual(a, b),
) -> duality.Dual(
  core.Recv(proposal, core.Send(vote, core.Recv(outcome, a))),
  core.Send(proposal, core.Recv(vote, core.Send(outcome, b))),
)

pub fn propose(
  accepted: duality.Dual(a, b),
  rejected: duality.Dual(c, d),
) -> duality.Dual(
  core.Send(proposal, core.Offer(a, c)),
  core.Recv(proposal, core.Choose(b, d)),
)

let proof = patterns.propose(patterns.request(duality.done()), duality.done())

pub fn request(
  then: duality.Dual(a, b),
) -> duality.Dual(
  core.Send(question, core.Recv(answer, a)),
  core.Recv(question, core.Send(answer, b)),
)

/// Two round trips, then done.
pub fn proof() -> Dual(
  patterns.Request(String, Int, patterns.Request(String, Int, core.Done)),
  patterns.Serve(String, Int, patterns.Serve(String, Int, core.Done)),
) {
  patterns.request(patterns.request(duality.done()))
}

pub fn serve(
  then: duality.Dual(a, b),
) -> duality.Dual(
  core.Recv(question, core.Send(answer, a)),
  core.Send(question, core.Recv(answer, b)),
)

let proof = patterns.serve(duality.done())