search

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq
MIT License
204 stars 51 forks source link

Equivalence up-to-effects #65

Open gmalecha opened 5 years ago

gmalecha commented 5 years ago

In the compiler (#59) we had to generalize the relation for Ret in eutt to 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.

gmalecha commented 5 years ago

I wondering if this could be used to unify eq_itree and eutt...

Lysxia commented 5 years ago

While I'm triaging issues, I'm not sure this is essential for a first release, but I would definitely like eq_itree and eutt to be parameterized by a heterogeneous relation between effects.

I don't see eq_itree and eutt being unified any time soon even with this resolved, but that's not entirely out of the picture.

gmalecha commented 5 years ago

Not essential for a first release, but would be very useful in the future.