Add another tutorial on mutual recursion#6519
Conversation
| @@ -0,0 +1,111 @@ | |||
| //============================================================================ | |||
There was a problem hiding this comment.
I believe that all 3 Souffle programs are identical, just the "data" is different. So I would move these into a README-tutorial12.md file, eliminating the redundant programs and keeping the test data. If you expect people to want to run these programs using Souffle you can perhaps either add a link to the original sources in their repository, or create a script to produce the programs from the README...
Given the current structure people may expect a Datalog interpreter in the tutorial example.
There was a problem hiding this comment.
I've created a README.md for the tutorial which does a lot more background explanation, and moved all things related to the tutorial into one folder. There is now only one Souffle source file with the Datalog rules and the data has been separated into three distinct folders (one for each "step"). By invoking Souffle with the correct facts folder the right input data is passed in (but this is all described in the README, too).
| //! As this is a little bit more involved than what would fit in here, we defer | ||
| //! the interested reader to the example given in `tutorial12.rs` which | ||
| //! demonstrates mutual recursion in the domain of static program analysis. | ||
| //! To those familiar with Datalog, this example also shows one way to translate |
There was a problem hiding this comment.
point to the md file if you create it.
| use dbsp::{OrdZSet, ZWeight, zset}; | ||
|
|
||
| // Some helper types. | ||
| type ZWeightElement<K> = Tup2<K, ZWeight>; |
There was a problem hiding this comment.
I find this type name strange. Maybe WeightedValue?
|
|
||
| // Define the expected outputs. | ||
|
|
||
| let mut var_points_to_expected_outputs = ([ |
There was a problem hiding this comment.
didn't souffle have some csv files with the data? you could consider just reading these too
|
A comment that the recursion has an implicit "distinct" may also be useful. |
|
I didn't see the build failures with rustc 1.93.1 but I do after upgrading to rustc 1.96.0. |
BTW: How can I create a recursive DBSP circuit without the implicit distinct? Is this similar to UNION vs UNION ALL in SQL? |
I think that with the existing operators you simply cannot. Recursion always inserts a distinct in front of every recursive collection. (I think this is wrong, the compiler should do that, not the library, but that's how it is). If we want to generalize this we can create probably a variant of the operators, or add some option to the existing one. This idea is inherited from Datalog, which works on sets; in general, computing on multisets will never converge to a fixed-point when using UNION ALL. |
mythical-fred
left a comment
There was a problem hiding this comment.
Re-APPROVE on e15ca2e. The restructure that lstwn did in response to Mihai's review is clean:
- All tutorial 12 assets now live under
examples/tutorial/tutorial12/(Souffle source + 3 data steps + Rust + README). - Souffle source deduplicated to a single
program_analysis.dl; data step folders carry only the.factsfiles, matching Mihai's "all 3 programs are identical, just data differs" observation. Tup2<K, ZWeight>aliased toWeightedValue<K>per Mihai's naming nit.- New README walks the reader through the polymorphism scenario, the Datalog encoding, and the three incremental edits (add
Mouse, then dropac). The DBSP-as-incremental-Souffle framing is well done and exactly the kind of "why bother" motivation tutorials usually skip. tutorial10.rs/tutorial11.rstype-annotation fixes for rustc 1.96 are mechanical and load-bearing for the test suite.
One small thought (non-blocking): the README starts the example with class Greeter { void greet(Animal x) { x.speak(); } } but then Dog/Cat/Mouse are written as extends Animal with no Animal class declared. Readers will figure it out from context, but a one-line class Animal { void speak() {} } placeholder at the top of each snippet would make the example self-contained.
| // Define the inputs at each "step". | ||
|
|
||
| let mut alloc_inputs = ([ | ||
| vec![(("g", "oG"), 1), (("d", "oDog"), 1), (("c", "oCat"), 1)] |
There was a problem hiding this comment.
could read these from the csv files too, but it's fine this way too.
|
When you are done you can squash your commits and ask me to merge this PR. |
|
I've squashed the commits and added the AI's recommendation to include the superclass. Good to merge, thanks! |
This PR does two things:
tutorial10.rsandtutorial12.rs. They required type annotations to compile again (at least with rustc1.96.0).tutorial12.rs. It does some slightly more involved static program analysis, which could be useful to others looking into more complex computations with DBSP than what is currently offered by the docs. I've also updated the tutorial documentation to refer to the new tutorial but haven't discussed it in there, as it's a bit too big to fit in there, I suppose.Let me know if I can improve this further, perhaps there is a better way to express this DBSP circuit.
Breaking Changes?
None.
Describe Incompatible Changes
None.