ekzhang / crepe

Datalog compiler embedded in Rust as a procedural macro
Apache License 2.0
460 stars 16 forks source link

Potential for use in incremental programming language tooling #8

Open brendanzab opened 3 years ago

brendanzab commented 3 years ago

Hello! I'm making a programming language, Pikelet, and I've been wanting to start working on a query-driven, incremental driver for the language. Some of my requirements are:

I've been looking at salsa, differential-datalog, and souffle, but they all seem rather complicated and heavy-weight for my taste. datafrog also looks interesting, but I don't know what its development status is. My other option is to roll my own, in the manner of lucent. Do you think there is potential for crepe to be used for this kind of thing in the future, or is this out of scope for you?

ekzhang commented 3 years ago

Hello @brendanzab, interesting work. I think Datalog is a really useful, high-level abstraction for building contextual analyses on programming languages. Crepe lets you write very simple, declarative rules as you'd read in any specification, and also allows you to call Rust functions. It's most similar to Souffle, which compiles a .dl file into a .cpp program and comes with a complex build/link tool, except Crepe is much simpler by using Rust proc macros.

Multithreading is a feature I've thought about adding but haven't gotten to. Souffle's approach is to parallelize outer loops with #pragma omp parallel for, which works okay, and they maintain shared state (the intensional database) with a fancy B-Tree. I was thinking about adding a feature flag to Crepe that adds rayon and some appropriate concurrent data structures.

I can't comment on Salsa or DDlog due to lack of familiarity.

brendanzab commented 3 years ago

Yeah it's be super neat to actually be able to write the elaborator and typing rules in datalog, but I wasn't sure how feasible that would be. I did see this presentation recently which uses datalog: "A Systematic Approach to Deriving Incremental Type Checkers", but they seem to push metavariable solving and dependent type systems to later work. I was more thinking it would be cool to have a way of describing the higher level queries for now, then calling rust functions to do the heavy lifting. I think DDlog can do similar, but I'm not sure.

jaredly commented 3 years ago

@ekzhang from perusing the docs, it looks like crepe doesn't support incremental updates to the state, right? Like I can't "evalute some facts + rules, look at the resulting state, and then add some new facts and see what the new result is"? Because run() consumes the crepe object.

ekzhang commented 3 years ago

Yes @jaredly, that's correct. At the time, I wasn't able to figure out the best way of reconciling incremental updates with support for stratified negation, since when your program has negation, additional input relations might cause other relations not to be generated.

What do you think? Maybe it's possible to do this by having separate cases for when the program does / does not have negation?