Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Disallowing looking up non-constructor functions #420

Open
yihozhang opened this issue Sep 4, 2024 · 1 comment
Open

Disallowing looking up non-constructor functions #420

yihozhang opened this issue Sep 4, 2024 · 1 comment
Assignees

Comments

@yihozhang
Copy link
Collaborator

(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 FTRobbin self-assigned this Sep 4, 2024
@FTRobbin
Copy link
Collaborator

FTRobbin commented Sep 4, 2024

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:

// TODO(yz): we can delete this code once we enforce that all rule bodies cannot read the database (except EqSort).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants