Repository navigation
Equivalence up-to-effects #65
Description
Activity
I wondering if this could be used to unify
eq_itreeandeutt...While I'm triaging issues, I'm not sure this is essential for a first release, but I would definitely like
eq_itreeandeuttto be parameterized by a heterogeneous relation between effects.I don't see
eq_itreeandeuttbeing unified any time soon even with this resolved, but that's not entirely out of the picture.Not essential for a first release, but would be very useful in the future.
In the compiler (#59) we had to generalize the relation for
Retineuttto be a parameter (also we opted to make it heterogeneous). This gave us additional flexibility in stating theorems that seems quite useful. I'm interested to know if we can do the same thing for effects themselves. @Lysxia mentioned that you guys considered this, but it is difficult. I definitely believe this, but it seems like it could be a fruitful line of investigation because (I think) it will dramatically improve the power of the library.