"Monad transformers more powerful than effects" - Examples?

Question

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?

Disentangle

This is a useful question which can be answered by more people than just the paper's author. An example of more power is allowing duplicate effects. – Rein

I would like to know the answer to this question. I don't want to have to contact the paper's author when I could just find it here. – Euton

This is good question even when it mentions some paper... – Sappanwood

If I recall correctly from papers I found in Andrej Bauer's blog, algebraic effects are just stylized uses of the delimited continuation monad. So monads are at least as powerful as algebraic effects. The homepage of the Eff language, which is built to use algebraic effects from the ground up, contains links to some of these papers. I'm not posting this as an answer, because I don't really know the details myself. – Ludlow

@EduardoLeón Delimited continuations are given in Bauer and Pretnar 2010, Programming with Algebraic Effects and Handlers (pdf); the paper ends with the question "Finally, continuations are the canonical example of a non-algebraic computational effect, so it is a bit surprising that eff provides a flexible and clean form of delimited control, especially since continuations were not at all on our design agenda. What then can we learn from eff about control operators in an effectful setting?" – Capricorn

@CharlesStewart IIRC, Plotkin and Power (can't provide link, I'm using a tablet, but you must surely know what paper I'm talking about) also mention that the delimited continuation monad doesn't have a finite rank, whereas all algebraic effects give rise to monads of finite rank. – Ludlow

@Eduardo Is this the paper in question? homepages.inf.ed.ac.uk/gdp/publications/comb_cont.pdf – Disentangle

@geoff_h: The paper I originally had in mind was Notions of Computation Determine Monads, The paper you mentioned is a later work, and cites the former. – Ludlow

Answer 1

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.

Capricorn

Thanks for the answer. I'm thinking about it and trying to translate the category theory into something a bit more program-y to get my head around. @Eduardo commented above that effects were isomorphic to delimited continuations. So I suspect that there is some intuition about the fact that undelimited continuations can't be modelled. Effects, maybe, have to be scoped to a given region and handled before effectful values can escape whereas monads are more contagious. – Disentangle

@Disentangle I said algebraic effects could be modeled as uses of the delimited continuation monad, not that they are equivalent - which could well be the case but I don't really know. – Ludlow

@Eduardo But Eff does allow a representation of delimited continuations - albeit one which sometimes requires recursive types. This suggests an isomorphism - effects can be modelled as delimited continuations, delimited continuations can be modelled as effects - but maybe Eff can represent some non-algebraic effects as well - although I'm not sure I've got a good grasp of what a non-algebraic effect would mean. – Disentangle

@Disentangle I suspect that the relationship between algeberaic effects and delimited continuations is rather like the relationship between monads and CPS: the latter offers the expressiveness of control constructs of the former, but does not offer the ability to construct datatypes. – Capricorn