Lasp: A language for distributed, coordination-free programming | Hacker News Reader

Lasp: A language for distributed, coordination-free programming

blog.acolyer.org

33 pointsmrry5 comments

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.

[0]https://webcache.googleusercontent.com/search?q=cache:gu5lBo...

What do you make of LVars? [1]

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

Will this be incorporated into Riak?

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.

Reply on news.ycombinator.com