For anybody looking for additional footing on understanding this, I found the following to be very helpful: <a href="http://bloom-lang.net/calm/" rel="nofollow">http://bloom-lang.net/calm/</a><p>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.<p>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.<p>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?)
Great work and obscure enough that I'm sure one of the authors made the submission :)<p>If so, here are a few things that I saw while glancing over the paper (I'll read the paper in detail later):<p>- 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.<p>Edit: just saw that the paper was referenced after all, my bad!<p>- 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.