Since CRDTs are just join-semilattices with a zero element, and the category of join-semilattices with zero is a model for linear logic[1], I suspect that there may be an even cleaner way to write eventually consistent programs, using a linear lambda calculus (or possibly a process calculus, since those also model linear logic). I've been looking into this area in my off-time but haven't managed to get very far, perhaps because I still don't understand category theory well enough. Nice to see there's demand for a language with this property, though :).
[1] Linear logic's "tensor product" corresponds to tensor product of semilattices; linear maps correspond to semilattice-morphisms with a pointwise join operation. Linear "with" and "tensor sum" both correspond to cartesian product of semilattices. It's a rather degenerate model in this respect.
There are languages built on join semi-lattices such as Bloom^L for writing eventually consistent programs[0].
The idea being that logical monotonicity removes the need for co-ordination and eventual consistency in the language can be guaranteed by co-ordination around non-monotonic points.
If you like logic-based programming it's a rather interesting language to research.
Programs written using a deterministic-by-construction model of parallel computation are guaranteed to always produce the same observable results, offering programmers freedom from subtle, hard-to-reproduce nondeterministic bugs that are the scourge of parallel software. We present LVars, a new model for deterministic- by-construction parallel programming that generalizes existing single-assignment models to allow multiple assignments that are monotonically increasing with respect to a user-specified lattice.
LVars ensure determinism by allowing only monotonic writes and "threshold" reads that block until a lower bound is reached. We give a proof of determinism and a prototype implementation for a language with LVars and describe how to extend the LVars model to support a limited form of nondeterminism that admits failures but never wrong answers
Some of the CRDT data types already are (if I understand correctly).
Or maybe this can be the base of a new type of database -- a CRDT only database -- an eventually consistent database but which auto-resolves conflicts between siblings and always converges to one value.
I've been thinking about a CRDT datastore for a while, especially one based on the delta state paper. I've gotten tripped up on which features to support/provide however.
6 comments
[ 3.7 ms ] story [ 31.0 ms ] thread[1] Linear logic's "tensor product" corresponds to tensor product of semilattices; linear maps correspond to semilattice-morphisms with a pointwise join operation. Linear "with" and "tensor sum" both correspond to cartesian product of semilattices. It's a rather degenerate model in this respect.
The idea being that logical monotonicity removes the need for co-ordination and eventual consistency in the language can be guaranteed by co-ordination around non-monotonic points.
If you like logic-based programming it's a rather interesting language to research.
[0]https://webcache.googleusercontent.com/search?q=cache:gu5lBo...
Programs written using a deterministic-by-construction model of parallel computation are guaranteed to always produce the same observable results, offering programmers freedom from subtle, hard-to-reproduce nondeterministic bugs that are the scourge of parallel software. We present LVars, a new model for deterministic- by-construction parallel programming that generalizes existing single-assignment models to allow multiple assignments that are monotonically increasing with respect to a user-specified lattice.
LVars ensure determinism by allowing only monotonic writes and "threshold" reads that block until a lower bound is reached. We give a proof of determinism and a prototype implementation for a language with LVars and describe how to extend the LVars model to support a limited form of nondeterminism that admits failures but never wrong answers
[1] http://lambda-the-ultimate.org/node/4823
Some of the CRDT data types already are (if I understand correctly).
Or maybe this can be the base of a new type of database -- a CRDT only database -- an eventually consistent database but which auto-resolves conflicts between siblings and always converges to one value.