Distinguish datatypes from other tables #223

oflatt · 2023-09-03T22:42:13Z

Tables with merge functions are fundamentally different than those without- we have places in the code where we check for a merge function or defaults. This PR clarifies that distinction.

It also enforces that the set keyword is only used on non-datatype tables, clarifying the confusion between set and union and making it clear when set is needed.

Depends on #222

…tatypes

saulshanabrook · 2023-09-04T11:27:25Z

src/ast/mod.rs

+    /// - The output is not a primitive
+    /// - No merge function is provided
+    /// - No default is provided
    Function(FunctionDecl),


Oh I wasn't aware you could have functions with non primitive return values and custom merge functions...

It's currently a very under-tested feature! I plan to use it more in the future though, it's essential for encoding proofs.

It can be used to simulate the choice construct in Datalog literature by setting :merge old (as is used in proofs)

saulshanabrook · 2023-09-04T18:52:39Z

I am giving this branch a test with the Python test suite to see if anything breaks and will let you know this week!

oflatt · 2023-09-04T19:16:25Z

I am giving this branch a test with the Python test suite to see if anything breaks and will let you know this week!

Thanks! That's super helpful

yihozhang · 2023-09-06T23:34:24Z

Does this PR disallow :merge old for datatypes?

oflatt · 2023-09-06T23:39:25Z

Yep, datatypes can't have merge functions

yihozhang · 2023-09-06T23:53:28Z

Doesn't this cause issues for proofs? Proof terms are datatypes, right?

I like the ability to simulate the choice construct (for data types) in Datalog. I'm even thinking about having a :choice keyword in function declarations. Or maybe you are sure we don't need this anymore?

PR to try out upstream PR: egraphs-good/egglog#223

saulshanabrook · 2023-09-07T14:55:48Z

I gave it a go on the Python bindings, and almost all the tests pass. The one that doesn't might be on my end, so I'll keep looking into it. It's a more complicated example that I am looking to refactor anyway a bit

egraphs-good/egglog-python#46

saulshanabrook · 2023-09-07T19:46:52Z

src/ast/mod.rs

-            default: None,
+            default: Some(Expr::Lit(Literal::Unit)),


I am curious why the relation now needs a default to work? It does make it a little more cumbersome to define relations with the function syntax. Would you ever want to define a function that returns Unit but doesn't have this as a default?

Good question-
Unit is a primitive just like i64. Before, we had special logic for making default units, making them special in a weird way. Now, I make it explicit that the relation syntax is sugar for this function for convenience.

You can still have a function that returns Unit without this default and use set everywhere. But this is more convenient

Ah I see.

Is it true then that using a function that does not return a default as an action is a no-op? And that's why you needed the special case before and now with it removed you have added a default?

As a test, this rule seems to have no effect, when there is no default (based on the viz):

(datatype Expr) (function trigger () Expr) (function foo () i64) (trigger) (rule ((= x (trigger))) ((foo))) (run 1)

But it does when there is a default:

(datatype Expr) (function trigger () Expr) (function foo () i64 : default 10) (trigger) (rule ((= x (trigger))) ((foo))) (run 1)

Hmm, shouldn't you get an exception when there isn't a default?
Otherwise, the action might fail halfway-through!

Yeah, so if I am understanding that correctly, only functions with defaults can be used as actions?

oflatt · 2023-09-08T16:14:30Z

Doesn't this cause issues for proofs? Proof terms are datatypes, right?

I like the ability to simulate the choice construct (for data types) in Datalog. I'm even thinking about having a :choice keyword in function declarations. Or maybe you are sure we don't need this anymore?

Yep, this PR supports proofs. For proofs we need a way to talk about stable ids for terms, so we need some kind of table which is stable (I call those datatypes). If you want something else, just use a non-datatype table instead.

yihozhang

Thanks! This makes sense now. I left a small comment but looks great!

yihozhang · 2023-09-08T17:57:47Z

src/typecheck.rs

@@ -747,9 +752,6 @@ impl EGraph {
                    let value = if let Some(out) = function.nodes.get(values) {
                        out.value
                    } else if make_defaults {
-                        if function.merge.on_merge.is_some() {


why's this no longer needed?

make_defaults implies that this isn't a datatype. Either there is a merge function, or you get an exception because you tried to merge two primitives.

oflatt added 7 commits September 3, 2023 13:37

desugar function declarations

0acee28

get rid of unit

18aaaf2

Merge branch 'oflatt-desugar-merge-action' into oflatt-distinguish-da…

7f4b58e

…tatypes

okay we still need unit

9d47f2c

make unit work again- as well as reading datatypes

8f78900

enforce difference between set and union

b6fe9c4

sprinkle a little docs

5d47d73

oflatt requested a review from a team as a code owner September 3, 2023 22:42

oflatt requested review from mwillsey and yihozhang and removed request for a team September 3, 2023 22:42

writle a little documentation

f6df3ff

saulshanabrook reviewed Sep 4, 2023

View reviewed changes

saulshanabrook added a commit to egraphs-good/egglog-python that referenced this pull request Sep 7, 2023

Update for "Distinguish datatypes from other tables"

23e4dce

PR to try out upstream PR: egraphs-good/egglog#223

saulshanabrook mentioned this pull request Sep 7, 2023

Update for "Distinguish datatypes from other tables" egraphs-good/egglog-python#46

Merged

saulshanabrook reviewed Sep 7, 2023

View reviewed changes

yihozhang approved these changes Sep 8, 2023

View reviewed changes

oflatt mentioned this pull request Sep 9, 2023

RFC: fix semi-naive and table problems #228

Open

oflatt merged commit 4d67f26 into egraphs-good:main Sep 12, 2023
3 checks passed

saulshanabrook mentioned this pull request Dec 1, 2023

Remove code path for calling set on union merge fn #307

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Distinguish datatypes from other tables #223

Distinguish datatypes from other tables #223

oflatt commented Sep 3, 2023 •

edited

Loading

saulshanabrook Sep 4, 2023

oflatt Sep 4, 2023

yihozhang Sep 6, 2023

saulshanabrook commented Sep 4, 2023

oflatt commented Sep 4, 2023

yihozhang commented Sep 6, 2023 •

edited

Loading

oflatt commented Sep 6, 2023

yihozhang commented Sep 6, 2023

saulshanabrook commented Sep 7, 2023

saulshanabrook Sep 7, 2023

oflatt Sep 8, 2023 •

edited

Loading

saulshanabrook Sep 8, 2023

oflatt Sep 8, 2023

saulshanabrook Sep 9, 2023

oflatt commented Sep 8, 2023 •

edited

Loading

yihozhang left a comment

yihozhang Sep 8, 2023

oflatt Sep 8, 2023

Distinguish datatypes from other tables #223

Distinguish datatypes from other tables #223

Conversation

oflatt commented Sep 3, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

saulshanabrook commented Sep 4, 2023

oflatt commented Sep 4, 2023

yihozhang commented Sep 6, 2023 • edited Loading

oflatt commented Sep 6, 2023

yihozhang commented Sep 6, 2023

saulshanabrook commented Sep 7, 2023

Choose a reason for hiding this comment

oflatt Sep 8, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

oflatt commented Sep 8, 2023 • edited Loading

yihozhang left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

oflatt commented Sep 3, 2023 •

edited

Loading

yihozhang commented Sep 6, 2023 •

edited

Loading

oflatt Sep 8, 2023 •

edited

Loading

oflatt commented Sep 8, 2023 •

edited

Loading