There's a reason why a lot of programming language papers use formal math notation, because it's a lot more concise to express the entire typing rules of your language in a dozen or so inference rules rather than a more convoluted implementation.[0]
Formulog looks like it could potentially replace that math notation for something as rigorous yet executable.
On the other hand, denotational semantics are usually straightforward enough to be implemented by reading off the math. As an example, it was quite easy for me to translate Scheme's semantics to code.[1]
I hope it gets reimplemented in a functional language as well, Formulog's current implementation is in Java[2] which might not be ideal for reducing implementation bugs.
Any advice for learning to read the PL math notation? The PL papers I've seen normally take it for granted, so I don't even know what it's called to search for it!
Roughly: the way facts work in Datalog and similar stuff have pretty strong monotonicity properties. So if you want to allow adding more predicates and computations to the system, you kinda wanna only allow monotonic functions! This has some pretty interesting surprises when it comes to how to model things like true or false!
Datafun is quite cool! Formulog and Datafun seem similar---both combine logic programming and pure functional programming---but they take wildly different approaches.
Datafun is a foundational re-imagining of what a Datalog could look like: start with a higher-order programming language and give it a first-class notion of least fixed points. A type system for tracking monotonicity lets you roll your own Datalog. It's impressive that you can reconstruct semi-naive evaluation (morally: in each 'round' of evaluation, only apply rules matching new results) in their setting (https://dl.acm.org/doi/abs/10.1145/3371090). Datafun is still a ways away from the performance and implementation maturity of existing Datalogs, though.
Formulog's approach is to try to let Datalog be Datalog as much as possible. We end up with restrictions around higher-order functions and other FP features in order to keep things simple on the Datalog side---quite the opposite of Datafun's fancy type system. Our Formulog interpreter does pretty well with internment, parallel execution, and magic sets, but you could easily port our design to existing Datalog compilers and get even bigger speedups. It's not clear how to do that for Datafun... yet.
(I suspect you could port our SMT interface to Datafun without too much of a problem, too.)
I would have thought the SMT queries would be the most time-consuming part of this, but the authors make a big deal of leveraging Datalog optimzations to drive performance.
Especially given they purposefully don't re-use the SMT context across SMT terms.
Aren't the big SMT solvers already doing a bunch of optimization to allow incremental (push/pop) queries to be fast?
Poplog was a 1980's integration of a Prolog, Common Lisp, C-like POP-11, and SML. Regrettably, it's academic authors had commercial dreams, which seemingly neutered the transformative impact I thought it might then have had.
It is also integesting to see how typeclasses/traits and OCaml's (still upcoming?) "modular implicits" are related to logic programming.
I commend the rustc team for taking this lineage seriously in developing Chalk[1] and using differential-dataflow for the next borrow checker. If they combine those into a differential-dataflow-powered Chalk it will be very formidable!
We'll have to catch up Haskell at some point, sigh.
[+] [-] siraben|5 years ago|reply
Formulog looks like it could potentially replace that math notation for something as rigorous yet executable.
On the other hand, denotational semantics are usually straightforward enough to be implemented by reading off the math. As an example, it was quite easy for me to translate Scheme's semantics to code.[1]
I hope it gets reimplemented in a functional language as well, Formulog's current implementation is in Java[2] which might not be ideal for reducing implementation bugs.
[0] Contrast the code and math: https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
[1] https://github.com/siraben/r5rs-denot
[2] https://github.com/HarvardPL/formulog
[+] [-] benrbray|5 years ago|reply
EDIT: Thank you all for the references :)
[+] [-] carterschonwald|5 years ago|reply
Roughly: the way facts work in Datalog and similar stuff have pretty strong monotonicity properties. So if you want to allow adding more predicates and computations to the system, you kinda wanna only allow monotonic functions! This has some pretty interesting surprises when it comes to how to model things like true or false!
[+] [-] mgreenbe|5 years ago|reply
Datafun is a foundational re-imagining of what a Datalog could look like: start with a higher-order programming language and give it a first-class notion of least fixed points. A type system for tracking monotonicity lets you roll your own Datalog. It's impressive that you can reconstruct semi-naive evaluation (morally: in each 'round' of evaluation, only apply rules matching new results) in their setting (https://dl.acm.org/doi/abs/10.1145/3371090). Datafun is still a ways away from the performance and implementation maturity of existing Datalogs, though.
Formulog's approach is to try to let Datalog be Datalog as much as possible. We end up with restrictions around higher-order functions and other FP features in order to keep things simple on the Datalog side---quite the opposite of Datafun's fancy type system. Our Formulog interpreter does pretty well with internment, parallel execution, and magic sets, but you could easily port our design to existing Datalog compilers and get even bigger speedups. It's not clear how to do that for Datafun... yet.
(I suspect you could port our SMT interface to Datafun without too much of a problem, too.)
[+] [-] fovc|5 years ago|reply
Especially given they purposefully don't re-use the SMT context across SMT terms.
Aren't the big SMT solvers already doing a bunch of optimization to allow incremental (push/pop) queries to be fast?
[+] [-] mgreenbe|5 years ago|reply
If you're interested, check out our ICLP 2020 extended abstract: https://cs.pomona.edu/~michael/papers/iclp2020_extabs.pdf. We should have more on this in not too long.
[+] [-] mncharity|5 years ago|reply
[+] [-] mncharity|5 years ago|reply
[+] [-] Ericson2314|5 years ago|reply
I commend the rustc team for taking this lineage seriously in developing Chalk[1] and using differential-dataflow for the next borrow checker. If they combine those into a differential-dataflow-powered Chalk it will be very formidable!
We'll have to catch up Haskell at some point, sigh.
[1]: https://github.com/rust-lang/chalk.git
[2]: https://github.com/TimelyDataflow/differential-dataflow