vellvm/ctrees

Allowing for an heterogeneous relation on labels

Opened this issue · 4 comments

YaZko commented

The current notion of bisimulation we use requires the computations to share the same signature of effects, and the same return type. This is reflected by the fact that the bisimulation checks that the challenges in the bisimulation game request to expose the same label, up-to coq's eq.

Relaxing this constraint on the return type is necessary to recover eutt's flexibility, but @nchappe has already a use case where he needs the additional flexibility to relate syntactically distinct events.

It should be slightly verbose but relatively straightforward to expand the current definition without breaking the current theory. Extending the theory should not be too bad, but a bit more work.

YaZko commented

There appears to be a bug in the coinduction library that needs to be fixed before going forward with this issue: the coinduction tactic seems to fail its reification when the greatest fixed point is an heterogeneous relation (see damien-pous/coinduction#5).

elefthei commented

I also have a use case for this feature -- making a note here for posterity :)

YaZko commented

I was planning on getting started on this Today, but got sidetracked slightly and am a bit hesitant as to what is the best pragmatic path.

As mentioned above, the necessary extension has been only recently added to the coinduction library. Damien went even further today by supporting not only heterogeneous relations (the only thing we need) but also heterogeneous dependent relations. However this complicates the unification problems that arise during typeclass resolution of setoid rewrites, and it has broken some of our code.

So I am basically hesitating between:

  • First thinking hard as to how to improve rewriting in general (this latest extension straight up makes some rewrites loops, but they were already slower than they should before)
  • Or starting to implement the heterogeneous bisimulation by pinning against a564ba8d6ef590e6f717f412c8954b3bb948ac5c (a.k.a. before the dependent generalization)

If I understand correctly the lack of this feature is straight up blocking for you @elefthei ? It's gonna soon be for @nchappe so the latter should probably be started now.

elefthei commented

I got unblocked! With a post-processing hack which is ugly but works for now :)