A Relational Theory of Effects and Coeffects
summary
Paper gives an operational, relational framework for higher-order languages with graded modal types and algebraic effects, using a monadic semantics (Maybe, subdistribution, etc.) and ternary modal relations indexed by a monoidal preorder. It defines a new corelator (graded/comonadic lax extension) alongside the usual relator, lifts relations to the monad, and formulates applicative similarity, contextual approximation and logical preorders. It proves a concrete sufficient condition—corelator laxly distributes over relator—for all these program refinements to be compositional.
AI-written summary · about