Monotonicity Types

In the face of the increasing trend in application development to interact with more and more remote services, and cognizant of the fact that issues arising from data consistency and task coordination are core challenges in distributed programming, the systems and data management communities have taken a keen interest in developing eventually consistent coordination-free models of distributed programming. These efforts have a striking similarity; they can all be characterized by the use of monotone functions as fundamental primitives of composition as well as the monotonic evolution of data over time. Yet, ensuring that application code conforms to the monotonicity constraints of these programming models is a tricky and manual affair, without support from the underlying language or system. In this paper, we present Monotonicity Types, a language and type system for proving functions monotone, which we believe could enable the customization and extension of this class of distributed programming models. We provide a full formalization of Monotonicity Types, including a novel operational semantics oriented from the perspective inside of a function, as well as a type soundness proof using logical relations.