4 ms·

Great work and obscure enough that I'm sure one of the authors made the submission :) If so, here are a few things that I saw while glancing over the paper (I'

by fmap 9y ago

Great work and obscure enough that I'm sure one of the authors made the submission :) 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.

rntz 9y ago
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.

by fmap 9y ago

rntz 9y ago

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.