In this extended abstract, we propose effect-oblivious equivalence, an equivalence relation for effectful programs that holds regardless of the implementation details of effects. Effect-oblivious equivalence is useful for reasoning about optimizations of programs whose effect implementations are unknown at the compile time, e.g., when the program can interact with different external environment at run time, or when the effect handlers are implemented separately, etc. When the effect implementations are known, effect-oblivious equivalence might still be useful for reasoning about optimizations that do not rely on assumptions over the effect implementations, e.g., the pure parts of a program.

We show that effect-oblivious equivalence in many programming languages can be encoded using general laws of classes of functors from Haskell. Furthermore, we can inherit the effect-oblivious equivalence properties if we use free structures of a suitable class of functors to model the semantics. We show that these free structures include the commonly used free monads, but also other structures like free applicative functors.