Reference
Combinators
A combinator takes CRDTs and returns a new one, together with the proof that the new one's effects commute. crdtlib has five principal combinators. The derived combinators below, and every CRDT in the catalog, are built from them and two families of primitive CRDTs.
Each section shows how a combinator changes the three type parameters: operations ω, state σ, and interpreted state γ. Highlighted slots are the ones it changes.
The code uses the timestamp-free CRDT. Each principal combinator also exists for CRDTₜ, with a ₜ suffix, such as productₜ.
Principal combinators
Product
product c₁ c₂producesωσσ₁ × σ₂γγ₁ × γ₂
This combinator composes two CRDTs such that a single operation is applied to both CRDTs. The combinator takes two CRDTs c₁ and c₂ such that the operation type ω for c₁.effect and c₂.effect is the same. The derived CRDT accepts the same operation type ω but maintains a state consisting of a tuple σ₁ × σ₂. The derived effect applies operations ω simultaneously to both substates.
def product {ω σ₁ γ₁ σ₂ γ₂ : Type*} (c₁ : CRDT ω σ₁ γ₁) (c₂ : CRDT ω σ₂ γ₂) :
CRDT ω (σ₁ × σ₂) (γ₁ × γ₂) where
effect e s := ⟨c₁.effect e s.1, c₂.effect e s.2⟩
interpret s := ⟨c₁.interpret s.1, c₂.interpret s.2⟩
commutative e₁ e₂ := ω:Type u_1σ₁:Type u_2γ₁:Type u_3σ₂:Type u_4γ₂:Type u_5c₁:CRDT ω σ₁ γ₁c₂:CRDT ω σ₂ γ₂e₁:ωe₂:ω⊢ ((fun s => (c₁.effect e₂ s.fst, c₂.effect e₂ s.snd)) ∘ fun s => (c₁.effect e₁ s.fst, c₂.effect e₁ s.snd)) =
(fun s => (c₁.effect e₁ s.fst, c₂.effect e₁ s.snd)) ∘ fun s => (c₁.effect e₂ s.fst, c₂.effect e₂ s.snd)
ω:Type u_1σ₁:Type u_2γ₁:Type u_3σ₂:Type u_4γ₂:Type u_5c₁:CRDT ω σ₁ γ₁c₂:CRDT ω σ₂ γ₂e₁:ωe₂:ωs:σ₁ × σ₂⊢ ((fun s => (c₁.effect e₂ s.fst, c₂.effect e₂ s.snd)) ∘ fun s => (c₁.effect e₁ s.fst, c₂.effect e₁ s.snd)) s =
((fun s => (c₁.effect e₁ s.fst, c₂.effect e₁ s.snd)) ∘ fun s => (c₁.effect e₂ s.fst, c₂.effect e₂ s.snd)) s
ω:Type u_1σ₁:Type u_2γ₁:Type u_3σ₂:Type u_4γ₂:Type u_5c₁:CRDT ω σ₁ γ₁c₂:CRDT ω σ₂ γ₂e₁:ωe₂:ωs:σ₁ × σ₂⊢ c₁.effect e₂ (c₁.effect e₁ s.fst) = c₁.effect e₁ (c₁.effect e₂ s.fst) ∧
c₂.effect e₂ (c₂.effect e₁ s.snd) = c₂.effect e₁ (c₂.effect e₂ s.snd)
ω:Type u_1σ₁:Type u_2γ₁:Type u_3σ₂:Type u_4γ₂:Type u_5c₁:CRDT ω σ₁ γ₁c₂:CRDT ω σ₂ γ₂e₁:ωe₂:ωs:σ₁ × σ₂⊢ c₁.effect e₂ (c₁.effect e₁ s.fst) = c₁.effect e₁ (c₁.effect e₂ s.fst)ω:Type u_1σ₁:Type u_2γ₁:Type u_3σ₂:Type u_4γ₂:Type u_5c₁:CRDT ω σ₁ γ₁c₂:CRDT ω σ₂ γ₂e₁:ωe₂:ωs:σ₁ × σ₂⊢ c₂.effect e₂ (c₂.effect e₁ s.snd) = c₂.effect e₁ (c₂.effect e₂ s.snd)
ω:Type u_1σ₁:Type u_2γ₁:Type u_3σ₂:Type u_4γ₂:Type u_5c₁:CRDT ω σ₁ γ₁c₂:CRDT ω σ₂ γ₂e₁:ωe₂:ωs:σ₁ × σ₂⊢ c₁.effect e₂ (c₁.effect e₁ s.fst) = c₁.effect e₁ (c₁.effect e₂ s.fst) All goals completed! 🐙
ω:Type u_1σ₁:Type u_2γ₁:Type u_3σ₂:Type u_4γ₂:Type u_5c₁:CRDT ω σ₁ γ₁c₂:CRDT ω σ₂ γ₂e₁:ωe₂:ωs:σ₁ × σ₂⊢ c₂.effect e₂ (c₂.effect e₁ s.snd) = c₂.effect e₁ (c₂.effect e₂ s.snd) All goals completed! 🐙
For example, productₜ (gsetₜ String) (mv_lwwₜ String) keeps a set of strings together with the most recently inserted one.
MapState
map_state f f'producesωσσ₂γγ
The map state combinator transforms the state of a CRDT, provided that the transformation admits a left inverse. The transformation is given by a function f together with a left inverse f'.
def map_state {σ₁ σ₂ ω γ} (f : σ₁ → σ₂) (f' : σ₂ → σ₁) (i : f' ∘ f = id := by funext; simp) (c : CRDT ω σ₁ γ) :
CRDT ω σ₂ γ where
effect e := f ∘ (c.effect e) ∘ f'
interpret := c.interpret ∘ f'
A typical use is flattening the nested tuples that other combinators produce, such as turning (σ₁ × σ₂) × σ₃ into σ₁ × (σ₂ × σ₃). The tagged union of three CRDTs does exactly this.
Associate
associate κ cproducesκ × ωσAssociate κ σγAssociateInterp κ γ
The associate combinator constructs CRDTs that are maps. The keys of the map are immutable values and the values are CRDTs. The associate combinator is well-suited for defining trees in the form of path-to-node associations.
def associate (κ : Type*) [DecidableEq κ] [Hashable κ] [DecidableEq σ] [Zero σ] (c : CRDT ω σ γ) :
CRDT (κ × ω) (Associate κ σ) (AssociateInterp κ γ) where
effect e s :=
s.alter e.fst (λ x ↦
some $ c.effect e.2 (x.getD 0)
)
interpret s := {
map k := c.interpret (s.getD k 0)
toList := s.map (λ _ ↦ c.interpret) |> Std.ExtHashMap.toListSorted
}
The interpretation exposes two functions: toList lists the keys, and map returns the state at a key or 0 if is not set.
Traverse
traverse f cproducesω₂σσγγThe traverse combinator makes it possible to apply multiple operations based on a single operation.
def traverse (f : ω₂ → List ω₁) (c : CRDT ω₁ σ γ) : CRDT ω₂ σ γ where
effect e := (f e).foldr c.effect
interpret := c.interpret
commutative e₁ e₂ := ω₂:Type ?u.16ω₁:Type ?u.8σ:Type ?u.11γ:Type ?u.10f:ω₂ → List ω₁c:CRDT ω₁ σ γe₁:ω₂e₂:ω₂⊢ ((fun init => List.foldr c.effect init (f e₂)) ∘ fun init => List.foldr c.effect init (f e₁)) =
(fun init => List.foldr c.effect init (f e₁)) ∘ fun init => List.foldr c.effect init (f e₂)
ω₂:Type ?u.16ω₁:Type ?u.8σ:Type ?u.11γ:Type ?u.10f:ω₂ → List ω₁c:CRDT ω₁ σ γe₁:ω₂e₂:ω₂x✝:σ⊢ ((fun init => List.foldr c.effect init (f e₂)) ∘ fun init => List.foldr c.effect init (f e₁)) x✝ =
((fun init => List.foldr c.effect init (f e₁)) ∘ fun init => List.foldr c.effect init (f e₂)) x✝
All goals completed! 🐙
The list CRDT uses it to turn one insertion between prev and next into two edges:
def edges : CRDT (σ × σ) (Associate σ (GSet σ)) (AssociateInterp σ (SetInterp σ)) :=
associate σ (gset σ)
def po_edges : CRDT (σ × σ × σ) (Associate σ (GSet σ)) (AssociateInterp σ (SetInterp σ)) :=
traverse (λ ⟨prev, elem, next⟩ ↦ [⟨prev, elem⟩, ⟨elem, next⟩]) (edges σ)MapInterpretation
map_interpretation f cproducesωσσγγ₂
This combinator transforms a CRDT's interpretation. The derived interpret delegates to the original c.interpret and uses f to transform the value from γ₁ to γ₂. The effect function remains the same.
def map_interpretation (f : γ₁ → γ₂) (c : CRDT ω σ γ₁) : CRDT ω σ γ₂ where
effect := c.effect
interpret := f ∘ c.interpret
commutative e₁ e₂ := γ₁:Type ?u.9γ₂:Type ?u.13ω:Type ?u.11σ:Type ?u.10f:γ₁ → γ₂c:CRDT ω σ γ₁e₁:ωe₂:ω⊢ c.effect e₂ ∘ c.effect e₁ = c.effect e₁ ∘ c.effect e₂
γ₁:Type ?u.9γ₂:Type ?u.13ω:Type ?u.11σ:Type ?u.10f:γ₁ → γ₂c:CRDT ω σ γ₁e₁:ωe₂:ωs:σ⊢ (c.effect e₂ ∘ c.effect e₁) s = (c.effect e₁ ∘ c.effect e₂) s
γ₁:Type ?u.9γ₂:Type ?u.13ω:Type ?u.11σ:Type ?u.10f:γ₁ → γ₂c:CRDT ω σ γ₁e₁:ωe₂:ωs:σ⊢ c.effect e₂ (c.effect e₁ s) = c.effect e₁ (c.effect e₂ s)
All goals completed! 🐙This is where conflict resolution often lives. The MV-LWW register keeps all concurrent writes, like a multi-value register, and only picks a winner when it is read.
Derived combinators
These are defined in terms of the principal combinators. They need no proofs of their own: their commutative fields come from the principal combinators they use.
MapOp
map_op f cproducesω₂σσγγ
The map_op combinator adapts the operation type of a CRDT by applying a pure function f : ω₂ → ω₁ to every incoming operation, translating it into exactly one operation of the underlying type. It is a specialization of traverse in which the list-valued function is always List.singleton ∘ f: the list produced by traverse is guaranteed to be a singleton, so no operation is ever skipped or duplicated – in contrast to traverse's general case, which allows fanout or filtering.
def map_op (f : ω₂ → ω₁) (c : CRDT ω₁ σ γ) : CRDT ω₂ σ γ :=
traverse (List.singleton ∘ f) cDisjointProduct
disjoint_product c₁ c₂producesω₁ ⊕ ω₂σσ₁ × σ₂γγ₁ × γ₂
The disjoint product combines two CRDTs into a product where each component is updated independently via its own operation type – in contrast to the product combinator, where both components share the same operation type and every operation is applied to both.
def disjoint_productₜ [PartialOrder τ] (c₁ : CRDTₜ τ ω₁ σ₁ γ₁) (c₂ : CRDTₜ τ ω₂ σ₂ γ₂) :
CRDTₜ τ (ω₁ ⊕ ω₂) (σ₁ × σ₂) (γ₁ × γ₂) :=
productₜ (traverseₜ (Option.toList ∘ Sum.getLeft?) c₁) (traverseₜ (Option.toList ∘ Sum.getRight?) c₂)JointProduct
joint_product c₁ c₂producesω₁ × ω₂σσ₁ × σ₂γγ₁ × γ₂
The joint product, like the disjoint product, combines two CRDTs with distinct operation types. The key distinction is that the composed operation type is a product ω₁ × ω₂ rather than a tagged union ω₁ ⊕ ω₂: every operation carries one sub-operation for each component CRDT, and both are always applied jointly in a single step – in contrast to the disjoint product where each incoming operation targets either c₁.effect or c₂.effect.
def joint_product (c₁ : CRDT ω₁ σ₁ γ₁) (c₂ : CRDT ω₂ σ₂ γ₂) :
CRDT (ω₁ × ω₂) (σ₁ × σ₂) (γ₁ × γ₂) :=
product (map_op (·.1) c₁) (map_op (·.2) c₂)TaggedUnion
tagged_unionₜ c₁ c₂produces(ω₁ ⊕ ω₂) ⊕ Choiceσ(σ₁ × σ₂) × …γγ₁ ⊕ γ₂The tagged union combinator, like the disjoint product before, is a fundamental building block for encoding algebraic data types as CRDTs.
def tagged_union_interp : (γ₁ × γ₂) × Choice → γ₁ ⊕ γ₂
| ⟨⟨s₁, _⟩, Choice.left⟩ => Sum.inl s₁
| ⟨⟨_, s₂⟩, Choice.right⟩ => Sum.inr s₂
def tagged_unionₜ [PartialOrder τ] [DecidableLT τ] [DecidableEq τ] (c₁ : CRDTₜ τ ω₁ σ₁ γ₁) (c₂ : CRDTₜ τ ω₂ σ₂ γ₂) :
CRDTₜ τ ((ω₁ ⊕ ω₂) ⊕ Choice) ((σ₁ × σ₂) × (Finset (Event τ Choice))) (γ₁ ⊕ γ₂) :=
map_interpretationₜ tagged_union_interp (disjoint_productₜ (disjoint_productₜ c₁ c₂) (mv_lwwₜ Choice))