"Monad transformers more powerful than effects" - Examples?

functional-programming monads effects idris

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?

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.

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.

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

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.

@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?"

Charles Stewart

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.

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.

@geoff_h 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.

@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.

@geoff_h 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.

"Monad transformers more powerful than effects" - Examples?

Follow WeChat

Want to stay one step ahead of the latest teleworks?

相似问题

Platform

Support

Links

Contact US