-
Notifications
You must be signed in to change notification settings - Fork 51
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
Egglog interface from rust #232
Comments
@yihozhang said:
|
Just noting this seems like this would be similar to how the Python bindings provide a high-level Pythonic interface on top of the constructs, that works with Pyhon's type system. |
Another idea I've talked about with @rtjoa is that we could simply have one big 'ol egglog macro which does egglog's typechecking at rust compile time. I think that would be a nice design. |
You could run the egglog typechecker at compile time and report any errors and warnings as Rust compiler errors and warnings. Then there is no need for a likely-error-prone second representation of the typechecker rules in the |
tagging @Alex-Fischman on previous discussions on Egglog's Rust interface. |
We need a better way to use egglog from Rust. I propose that we have two ways to use egglog: first, the existing parser using a text-based input format. Second, an embedding of the whole egglog language as Rust macros.
Basically, I think we should bring back that beloved define_language! macro, and take that concept and run with it.
More ambitiously, it would be cool to write it in a way that lifts all egglog type errors to become rust compile-time errors.
Suppose we added back define language so that constructors become a rust enum. Now, all egg Expr that are grounded will be well typed by definition.
However how could we get compile-time errors for improperly-typed rules?
I think we could do this by leveraging rust’s type inference.
Imagine that for every sort we generate something like this:
Now, say we write a rule:
(rule (= (Add a b) (Add b a)) ...)
For the query, the rule macro could generate something like this:
Rust type inference ensures that each variable has one type, and that the type is correct in every usage
So this would be really slick for rust users I think, but the downside is that we have two type checkers- one that re-uses the rust typechecker and our internal one
The text was updated successfully, but these errors were encountered: