The paper "Programming and reasoning with algebraic effects and dependent types" by Edwin C. Brady on effects in Idris contains the (unreferenced) claim that:
Although [effects and monad transformers] are not equivalent in power — monads and monad transformers can express more concepts — many common effectful computations are captured.
What examples are there that can be modelled by monad transformers but not effects?
Continuations can be modelled as monads, using CPS, but they are not algebraic effects as they cannot be modelled using Lawvere theories. See Martin Hyland and John Power, 2007, The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads (pdf), ENTCS 172:437-458.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With