Description
We should try to implement a sharing handler that can work with any effect that can be shared.
Motivation
Currently, we have a separate sharing handler for every relevant effect (ND and Trace). If we wanted to add a new effect that interacts with sharing, we would need a separate sharing handler for it, as well. And if we wanted to handle programs with more than one such effect, we would need a handler for each combination.
However, these handlers are all largely the same and only differ in a few parts. Therefore, we should try to generalize the sharing handler so that it can be used with any effect (and ideally any combination of effects, too).
Currently, an implementation for an effect-generic sharing handler exists in Haskell, so it should be investigated whether (and how) the implementation can be transferred to Coq.
Dependencies
Depends on #116
Alternatives
Additional Context
Description
We should try to implement a sharing handler that can work with any effect that can be shared.
Motivation
Currently, we have a separate sharing handler for every relevant effect (
NDandTrace). If we wanted to add a new effect that interacts with sharing, we would need a separate sharing handler for it, as well. And if we wanted to handle programs with more than one such effect, we would need a handler for each combination.However, these handlers are all largely the same and only differ in a few parts. Therefore, we should try to generalize the sharing handler so that it can be used with any effect (and ideally any combination of effects, too).
Currently, an implementation for an effect-generic sharing handler exists in Haskell, so it should be investigated whether (and how) the implementation can be transferred to Coq.
Dependencies
Depends on #116
Alternatives
Additional Context