It seems like monotonicity (or a subset, stronger monotinicity, still covering many practical use cases) can be statically enforced in an algrebraic type system

It seems like monotonicity (or a subset, stronger monotinicity, still covering many practical use cases) can be statically enforced in an algrebraic type system. With some generics magic you can encode monotonicity as a type assertion on (optionally asynchronous) function calls mapping an underlying transport/RPC mechanism (REST over HTTP, RPC over Websocket, custom protocol over TCP/domain socket...). In TypeScript for example you can strongly type your communication protocol (web requests/reponses, websockets, parent/worker ipc, etc) and get some guarantees at compile time. For example, you can guarantee that your state updates over the wire are eventually consistent. The same goes of course for other algebraic type systems by encoding monotonicity in the form of static type assertions (Flow, Caml, Haskell...).