egraphs-good / egglog

egraphs + datalog!
https://egraphs-good.github.io/egglog/
MIT License
459 stars 54 forks source link

Disallowing looking up non-constructor functions #420

Open yihozhang opened 2 months ago

yihozhang commented 2 months ago

(assigning @FTRobbin) Currently, we allow looking up non-constructor functions (i.e., functions whose output is not an EqSort or have a :merge function) in actions. This can cause actions to fail and make the database end up in an intermediate state.

(function f () i64)
(function g () i64 :merge (min old new))
(datatype E)
(function h () E :merge old)
(rule () 
      ((let x (f))))
(rule () 
      ((let x (g))))
(rule () 
      ((let x (h))))
(run 1)

Moreover, in principle, we don't want actions in a rule to observe the database, because such an implicit dependency implies that if the database changes, the rule needs to be fired again on the database. This is why our desugaring phase needs special handling for our semi-naive evaluation to be sound.

A fix to this is that we should disallow looking up values of functions in actions. By doing so, we can also remove the special handling for our semi-naive evaluation. Note that we should still allow global actions to look up functions, so the following program should still be allowed:

(function f () i64)
(let x (f)) ;; typechecks and throws a run-time error
FTRobbin commented 2 months ago

This overrides #228 #197 #142.

This test from #93 would be obsolete: https://github.com/egraphs-good/egglog/blob/757c52f6dcf8fe5b7b5eefb4bdc872ef70a5433a/tests/semi_naive_set_function.egg

Related code: Extra desugar that ensures the soundness of the semi-naive evaluation: https://github.com/egraphs-good/egglog/blob/757c52f6dcf8fe5b7b5eefb4bdc872ef70a5433a/src/ast/desugar.rs#L110