Monotonicity Types: Towards a Type System for Eventual Consistency
prl.ccs.neu.edu
prl.ccs.neu.edu
Personally, I've never done programming on distributed systems before so please correct me if I'm off at any point. The issue seems quite clear: you want to ensure that your function mutates inputs (or returns values relative to inputs) in a predictable way with values headed in one direction--increasing or decreasing. So, the idea of monotonicity types actually seems quite intuitive: ensure your outputs monotonicity are well-defined. It's mildly surprising this isn't something that has already been implemented.
On the other hand, could this monotonic type could be more generalized? Maybe something less two-dimensional, though perhaps this is overkill for most uses.
Also, as an aside, I don't have a Ph.D. in comp. sci, type theory, mathematics, or anything for that matter. This article was borderline gobbledygook to me and could be summarized far more succinctly (in a manner more friendly to the general programming public?)
If so, here are a few things that I saw while glancing over the paper (I'll read the paper in detail later):
- you might be interested in neel krishnaswami's paper on datafun, which is a functional language that includes datalog primitives in the form of least fixed points of monotone functions. Monotonicity is tracked in the type system, so this seems very relevant.
Edit: just saw that the paper was referenced after all, my bad!
- why do you need termination? Is it an artifact of the logical relation you use? If so, step indexing might help to relax this restriction.
It's very interesting to me to see the connections and differences here:
- Monotonicity Types and Datafun both track monotonicity, but for entirely different purposes; MT for CRDTs & distributed programming, Datafun for enforcing termination on recursive queries.
- MT uses a refinement-type-style system, while Datafun uses a modal type system. It's not clear to me whether this is related to their different use-cases, or just an accident of history.
- Relatedly, MT builds on an existing language (Lasp, which itself builds on Erlang), while Datafun is entirely new. MT is definitely more practical in this respect. My hope is that Datafun, while not practical to use directly yet, will have a big impact in the long run, as its namesake Datalog did, but that's just a dream :).
- MT and Datafun both care about semilattices: MT because CRDTs are based on semilattices, and Datafun because they give a natural and general way to comprehend over sets, and also guarantee a "bottom element" for our fixed-points to start computing from.
- Datafun has two kinds of function: monotone (preserves ordering) and discrete (could do anything). MT has five qualifiers on function arguments, representing whether the function respects the ordering, inverts the ordering, disrespects the ordering, ignores the argument entirely, or returns that argument unchanged. Wow! Are all those qualifiers really necessary? Maybe. Antitone functions (order-inverting) are something we're considering adding to Datafun, at least.
Based on the names, I guess that getAt is for value access, joinAt updates an entry of a map with a new value, span returns the maximum key with an associated entry, max is the maximum of two numbers, emptyMap is a map without entries and + and > are the usual mathematical functions. The GCounter type is essentially just a wrapper around maps that will be used to count things, apparently.
The function sumCounters they define first unwraps the maps backing the counters and determines the maximum key that will have to be considered.
Then there's a helper function sumCell which takes a key k and an accumulator acc containing the intermediate result for all previous keys. The helper function then checks whether all keys have been handled already, and returns the accumulator if that's the case. Otherwise it updates the accumulator with the sum of the entries for the given key in the two input maps. Then it calls itself recursively to handle the next key with the new accumulator.
The final line just starts off the helper function with an empty accumulator and the first key.