(lam $x (pack (var $x) (lit 3 Nat))
- The type of the lambda body would be:
-
Now since the way we are dealing with types is to store a syntactic recursive expression that represents the type of an eclass as analysis data, we are unable to capture updates in slots that aren't bound in the types themselves but rather outside of them (here $x by the lam node) because these updates happen in the egraph but the representations live in the analysis data
-
If we now perform equality saturation and somehow end up with a term like the following in place of the original term:
(lam $f1 (pack (var $f1) (lit 3 Nat))
- We would expect the type of the lambda body to now also contain the slot $f1 in place of $x but it will still remain the same:
(arr (var $x) Nat) <-- should also contain $f1
-
This makes it impossible to reconstruct this term in the rewrite phase because variable lookups there are performed by name (in this case the symbol $f1 is mapped to the lambda var Def but the type will try to look up $x and find nothing)
-
I tried to solve this by adding the types to the e-graph as well and then extracting the semantic rec expr corresponding to the syntactic rec expr of the analysis data which would have worked if I had not added the types as separate root terms but somehow made them subterms i.e. adding something like this would propagate slot updates correctly:
(lam $x (@ (arr (var $x) Nat) (pack (var $x) (lit 3 Nat)))
- But this would necessitate a rephrasing of all rewrite rules because I would need to always account for the type annotations if I wanted to write a simple rule like:
(@ ?type (tuple 1 2)) => (@ ?type (tuple 2 1))
-
Unless this adding of annotation patterns into unannotated rules can be automated somehow I don't think this is a good solution
-
Maybe it would be possible to generate a trace of the transformations a particular slot undergoes during eqsat like $x -> $f1 and then we generate such a trace for all occurences of external slots in types?
Occasionally, a type can contain slot uses that are initially bound by a term in an outer context
Consider for example:
Now since the way we are dealing with types is to store a syntactic recursive expression that represents the type of an eclass as analysis data, we are unable to capture updates in slots that aren't bound in the types themselves but rather outside of them (here $x by the lam node) because these updates happen in the egraph but the representations live in the analysis data
If we now perform equality saturation and somehow end up with a term like the following in place of the original term:
This makes it impossible to reconstruct this term in the rewrite phase because variable lookups there are performed by name (in this case the symbol $f1 is mapped to the lambda var Def but the type will try to look up $x and find nothing)
I tried to solve this by adding the types to the e-graph as well and then extracting the semantic rec expr corresponding to the syntactic rec expr of the analysis data which would have worked if I had not added the types as separate root terms but somehow made them subterms i.e. adding something like this would propagate slot updates correctly:
Unless this adding of annotation patterns into unannotated rules can be automated somehow I don't think this is a good solution
Maybe it would be possible to generate a trace of the transformations a particular slot undergoes during eqsat like $x -> $f1 and then we generate such a trace for all occurences of external slots in types?