Clarifying Valid Types

[saulshanabrook]

I am looking to see if I can tighten the static analysis type in the Python bindings and wanted to get some feedback on my current understanding of what is allowed:

• union: Must be user-defined sorts
• set: Must be primitive sorts
• delete: Can be either
• rewrite: Must be user-defined sorts
• =: Can be either
• !=: Can be either, but only sound to use it on primitive sorts, since user-defined sorts could later become = even if they aren't at the moment. I would make this only work on primitive sorts

Does that seem right?

[oflatt]

That doesn't sound right: I use set with non-primitive sorts sometimes.
With set, it's important that the function isn't a normal datatype though (has a merge function or default).
I think we should have a different keyword than function for normal datatypes from the datatype form.

That seems right besides that.

[saulshanabrook]

Thanks @oflatt for the clarification.

I realized I am a little fuzzy on how adding a default or merge function changes the non-primitive sorts.

My current understanding of set is that it changes one row in a function Table with a new output Value for some set of Input values. With non-primitive sorts (EqSorts) their value is an index into the parents vec of the union-find data structure.

So I am unclear what the set would do in the case where it operates on EqSorts and how it would differ from union.

If I try out this example:

(datatype Math
  (Num i64)
  (Var String)
  (comb Math Math))

(function special () Math :cost 10 :merge (comb old new) :default (Num 0) )
(special)
(set (special) (Num 10))
(union (special) (Num 5))

It looks like the difference is that set will end using the merge function whereas union won't. Is that how you understand the semantics as well?

Taking a look at the code, this example is desugared as:

(sort Math)
(function Num (i64) Math)
(function Var (String) Math)
(function comb (Math Math) Math)
(function special () Math :cost 10 :merge (comb old new) :default (Num 0))
(let v0___ (special))
(let v2___ 10)
(let v1___ (Num v2___))
(set (special) v1___)
(let v3___ (special))
(let v5___ 5)
(let v4___ (Num v5___))
(union v3___ v4___)

If we add a println!("instructions: {:?}", checker.instructions) into the compiler_actions function, we see that we end up with Set and Union instructions, as we might expect:

instructions: [Global("v1___"), Set("special")]
instructions: [Global("v3___"), Global("v4___"), Union(2)]

The Union instruction will end up calling unionfind.union whereas the Set instruction will not use the unionfind directly if a custom merge function is set. If it is, it will eval that expression and use that value as the result.

So the semantics seem to be:

1. union only works on eqsorts and will union them using the unionfind data structure
2. set, if applied to eqsorts, will by default also just union them. However, if a custom merge function is supplied, then it will set the value to the result of that merge.

[oflatt]

Yes, union only works on eqsorts. On the other hand, set uses merge functions.

I thought we disallowed using set on things that don't have a user-specified merge function to clarify this distinction. Is that not true? If not, we should fix that.

[saulshanabrook]

Yes, union only works on eqsorts. On the other hand, set uses merge functions.

So this means that if you define a rewrite on a function with a custom merge function it won't be triggered if the return type is an eqsort? My assumption would be the reverse.

It makes me wonder if it's necessary to keep separate set and union commands and if they could just be unified into one command? Is it ever necessary to use the union behavior on eqsat types with merge functions to ignore the merge function? If they were unified, then rewrite would also be able to be used regardless of the type of the result.

I thought we disallowed using set on things that don't have a user-specified merge function to clarify this distinction. Is that not true? If not, we should fix that.

I think it was disallowed, but there was a leftover code path for when it was still there I was looking at. I just submitted a PR to remove that unused code #307

[oflatt]

Hmm, if you use rewrite on a function with a custom merge function, shouldn't you get a type error? If not we need to fix that.

[saulshanabrook]

No there is no type error for a rewrite with a custom merge function, it will just call the union which will ignore the merge function:

(datatype Math
  (Num i64)
  (Add Math Math))

(function custom (Math Math) Math :merge (Add old new) :default (Num 0))

(rewrite (custom (Num 1) (Num 2)) (Num 3))

(custom (Num 1) (Num 2))

(run 1)

[oflatt]

Okay, that's bad.
This thread is convincing me that we should make this distinction more clear. In egglog, there should be two types of tables:
datatype tables and function tables.
datatype tables can be unioned but function tables must be set.

[oflatt]

It also doesn't really make sense to have a default with no merge function in my mind. It seems like you could just union a datatype with your default.

[oflatt]

I'll try to come up with an RFC to solve this conundrum

[saulshanabrook]

I'll try to come up with an RFC to solve this conundrum

Thanks! Yeah it's definitely a bit idiosyncratic at the moment. If you want someone to bounce ideas off of happy to jump on a call too.

[saulshanabrook]

• !=: Can be either, but only sound to use it on primitive sorts, since user-defined sorts could later become = even if they aren't at the moment. I would make this only work on primitive sorts

I noticed that the lambda example uses != in some rules on eq sorts, so it seems like I should allow Python users to also call != on their user-defined sorts? Does that seem right?

[oflatt]

Created #309, let me know what you think!
Using != on user-defined sorts works- but you have to be very careful! If the inequality changes later, unsoundness might occur, or semi-naiive evaluation may skip evaluating your query (unsoundly).

[saulshanabrook]

Thanks, @oflatt, for all the clarifications on what's valid currently! Compared to the initial post I have realized that:

• != should be allowed on all types, not just eqsorts, since it is used in the lambda example
• set can be used on either primitive or eqsorts. It isn't allowed on eqsorts that have the default merge function, but is allowed on ones with custom merge functions or defaults.

I'll close this since the questions this issue raised have been resolved. They have brought to light some potential points of confusion around the existing implementation, but I will leave that to another issue to discuss if necessary.