Pacta
![[Nix] Build & Test](https://github.com/byzantine-systems/pacta/actions/workflows/build.yml/badge.svg){kind=icon}
Pacta sunt servanda pietate, agreements must be kept.
Pacta is an experiment with session types for Gleam: a two-party protocol becomes a type, and using a conversation wrongly becomes a compile error rather than a bug you find in production. It is built on top of eparch and gen_statem.
Status: experimental. The API moves. This package exists so that it can move without dragging
eparch’s OTP wrappers through a major version every time it does.
The two layers
A protocol as a type, walked step by step:
| Module | Purpose |
|---|---|
pacta/session/core | The protocol grammar (Send / Recv / Choose / Offer / Done) as continuation-carrying phantom markers, the opaque Channel(protocol, msg), and the steps that walk it. Does no I/O. |
pacta/session/duality | Dual(a, b) witnesses proving two protocols fit together, their combinators, flip, connect, opposite. |
pacta/session/patterns | Reusable protocol fragments (Request/Serve, Propose/Decide, Coordinate/Participate) and their witnesses. |
pacta/protocol_machine | Drives a protocol from a gen_statem, by lowering onto eparch/state_machine. |
And a specification layer beside it, which runs before compilation rather than during it. This is what buys recursion and more than two participants, neither of which the type-level encoding can express:
| Module | Purpose |
|---|---|
pacta/protocol/spec | The specification language: Protocol, Spec, directed Choice, Loop/Continue, and the Assert/Require/Consume contact points. |
pacta/protocol/graph | Well-formedness checking and projection onto each participant, producing a flat cyclic state graph per role. |
pacta/protocol/relations | Decides duality, equivalence and subtyping over projected graphs by coinduction. |
pacta/protocol/weave | Interleaving composition: weaves two protocols into one, guided by their contact points. |
pacta/protocol/emit | Writes a projected graph out as Gleam source, one module per participant, plus review for checking committed output against the specification. |
Full API reference: https://hexdocs.pm/pacta.
Relationship to Eparch
eparch wraps Erlang/OTP behaviours (gen_statem, gen_event) in a type-safe API. Pacta is the experimental layer that used to live inside it, split out so the two can version independently.
The dependency is one-way and narrow: only pacta/protocol_machine imports eparch, and only to lower a protocol position onto eparch/state_machine. Everything else here is pure.
Installation
gleam add pacta
Usage
See the Session Types guide for the full walkthrough, or run the examples/atm project, which specifies a protocol once, projects it onto both participants, generates typed positions from it, and drives one side from a gen_statem.
Development
The project uses devenv and Nix for a hermetic development environment:
nix develop
Or, if you are already using direnv:
direnv allow .