I'm actually the Datafun paper's other author, so folks can AMA if they're interested in Datafun.
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.