> Can you expand on your understanding of GRIN doing parts of supercompilation? GRIN, if I am not mistaken, performs partial evaluation. For example, it constr

> Can you expand on your understanding of GRIN doing parts of supercompilation? GRIN, if I am not mistaken, performs partial evaluation. For example, it constrains, for each eval site, a set of tags and set of heaps allocations an eval site can receive. This is close to a partial evaluation step of a supercompilation. GRIN does not perform unification, though, it is not described in the original thesis, but data flow graph matching would be close to unification, reducing code size. > The downsides should be obvious: execution traces rapidly grow massive, compilation resources grow superlinearly, and there are many cases in which the result is worse than the original. This can be constrained. Supercompilation usually gets ran to a fixed point, where no partial evaluation steps can be performed that are not unifiable with previously encountered evaluation steps. But supercompilation can be stopped at any point. I believe you can read on that in Simon Peyton-Jones works, I am unable to find a link to that paper right now, I have troubles with the internet connection. EDIT: here it is: https://simon.peytonjones.org/improving-supercompilation/ https://simon.peytonjones.org/improving-supercompilation/ EDIT: Note "tag-bags," it rhymes with the tag sets of GRIN. > What value would Fuse get from equivalence of terms, do you think? I think that equivalence of terms is an efficient way to verify properties of programs. Myself, I am looking at consensus protocol implementation verification.