Chapter 2

Effects & coeffects, briefly

Two families of type systems organize reasoning about a computation's relationship to its environment:

Effect system

Γ ⊢ t : Teffect

The type is annotated with what the computation may do to the world. Lucassen–Gifford (1988); Moggi's monads; Plotkin–Power algebraic effects and Plotkin–Pretnar handlers (Koka, Eff, OCaml 5).

Coeffect system

Γcoeffect ⊢ t : T

The context is annotated with what the computation needs from the world: resources, permissions, services. Uustalu–Vene comonads; Petricek–Orchard–Mycroft; graded semirings (Gaboardi et al.).

Both are static instruments: effects are tracked within lexically fixed scopes and discharged by compile-time handlers; coeffect annotations are checked against contexts fixed before execution. The paper's move (§2.3) is not to add annotations but to reify the conceptual structures — the effect context and the coeffect context — as runtime values, so a runtime can establish dynamically what the type systems establish statically.

Haskell reading

You know effects-as-types (IO, MonadState s) and coeffects-as-constraints (MonadReader r, HasField, implicit params). The paper is not another such system. Its claim is that for runtime composition the two interesting objects are (a) the inverse of each effect and (b) the satisfaction status of each coeffect — and that the runtime, not the type checker, should own both.