Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to get the “inflexible semantics of monad transformers” using extensible effects?

Consider the following example.

newtype TooBig = TooBig Int deriving Show

choose :: MonadPlus m => [a] -> m a
choose = msum . map return

ex1 :: (MonadPlus m, MonadError TooBig m) => m Int
ex1 = do
    x <- choose [5,7,1]
    if x > 5
        then throwError (TooBig x)
        else return x

ex2 :: (MonadPlus m, MonadError TooBig m) => m Int
ex2 = ex1 `catchError` handler
  where
    handler (TooBig x) = if x > 7
        then throwError (TooBig x)
        else return x

ex3 :: Either TooBig [Int]
ex3 = runIdentity . runExceptT . runListT $ ex2

What should the value of ex3 be? If we use MTL then the answer is Right [7] which makes sense because ex1 is terminated since it throws an error, and the handler simply returns the pure value return 7 which is Right [7].

However, in the paper “Extensible Effects: An Alternative to Monad Transformers” by Oleg Kiselyov, et al. the authors say that this is “a surprising and undesirable result.” They expected the result to be Right [5,7,1] because the handler recovers from the exception by not re-throwing it. Essentially, they expected the catchError to be moved into ex1 as follows.

newtype TooBig = TooBig Int deriving Show

choose :: MonadPlus m => [a] -> m a
choose = msum . map return

ex1 :: (MonadPlus m, MonadError TooBig m) => m Int
ex1 = do
    x <- choose [5,7,1]
    if x > 5
        then throwError (TooBig x) `catchError` handler
        else return x
  where
    handler (TooBig x) = if x > 7
        then throwError (TooBig x)
        else return x

ex3 :: Either TooBig [Int]
ex3 = runIdentity . runExceptT . runListT $ ex1

Indeed, this is what extensible effects do. They change the semantics of the program by moving the effect handlers closer to the effect source. For example, local is moved closer to ask and catchError is moved closer to throwError. The authors of the paper tout this as one of the advantages of extensible effects over monad transformers, claiming that monad transformers have “inflexible semantics”.

But, what if I want the result to be Right [7] instead of Right [5,7,1] for whatever reason? As shown in the examples above, monad transformers can be used to get both results. However, because extensible effects always seem to move effect handlers closer to the effect source, it seems impossible to get the result Right [7].

So, the question is how to get the “inflexible semantics of monad transformers” using extensible effects? Is it possible to prevent individual effect handlers from moving closer to the effect source when using extensible effects? If not, then is this a limitation of extensible effects that needs to be addressed?

like image 391
Aadit M Shah Avatar asked Jan 06 '21 05:01

Aadit M Shah


1 Answers

I'm also a little confused about the nuance in those excerpts from that particular paper. I think it's more useful to take a few steps back and to explain the motivations behind the enterprise of algebraic effects, to which that paper belongs.

The MTL approach is in some sense the most obvious and general: you have an interface (or "effect"), put it in a type class and call it a day. The cost of that generality is that it is unprincipled: you don't know what happens when you combine interfaces together. This issue appears most concretely when you implement an interface: you must implement all of them simultaneously. We like to think that each interface can be implemented in isolation in a dedicated transformer, but if you have two interfaces, say MonadPlus and MonadError, implemented by transformers ListT and ExceptT, in order to compose them, you will also have to either implement MonadError for ListT or MonadPlus for ExceptT. This O(n^2) instance problem is popularly understood as "just boilerplate", but the deeper issue is that if we allow interfaces to be of any shape, there is no telling what danger could hide in that "boilerplate", if it can even be implemented at all.

We must put more structure on those interfaces. For some definition of "lift" (lift from MonadTrans), the effects we can lift uniformly through transformers are exactly the algebraic effects. (See also, Monad Transformers and Modular Algebraic Effects, What Binds Them Together.)

This is not truly a restriction. While some interfaces are not algebraic in a technical sense, such as MonadError (because of catch), they can usually still be expressed within the framework of algebraic effects, just less literally. While restricting the definition of an "interface", we also gain richer ways of using them.

So I think algebraic effects are a different, more precise way of thinking about interfaces before all. As a way of thinking, it can thus be adopted without changing anything about your code, which is why comparisons tend to look at the same code twice and it is difficult to see the point without having a grasp on the surrounding context and motivations. If you think the O(n^2) instances problem is a trivial "boilerplate" problem, you already believe in the principle that interfaces ought to be composable; algebraic effects are one way of explicitly designing libraries and languages around that principle.

"Algebraic effects" are a fuzzy notion without a fixed definition. Nowadays they are most recognizable by syntax featuring a call and a handle construct (or op/perform/throw/raise and catch/match). call is the one construct to use interfaces and handle is how we implement them. The idea common to such languages is that there are equations (hence "algebraic") that provide a basic intuition of how call and handle behave in a way that's independent of the interface, notably via the interaction of handle with sequential composition (>>=).

Semantically, the meaning of a program can be denoted by a tree of calls, and a handle is a transformation of such trees. That's why many incarnations of "algebraic effects" in Haskell start with free monads, types of trees parameterized by the type of nodes f:

data Free f a
  = Pure a
  | Free (f (Free f a))

From that point of view, the program ex2 is a tree with three branches, with the branch labeled 7 ending in an exception:

ex2 :: Free ([] :+: Const Int) Int  -- The functor "Const e" models exceptions (the equivalent of "MonadError e")
ex2 = Free [Pure 5, Free (Const 7), Pure 1]
-- You can write this with do notation to look like the original ex2, I'd say "it's just notation".
-- NB: constructors for (:+:) omitted

And each of the effects [] and Const Int corresponds to some way of transforming the tree, eliminating that effect from the tree (possibly introducing others, including itself).

  • "Catching" an exception corresponds to handling the Const effect by converting Free (Const x) nodes into some new tree h x.

  • To handle the [] effect, one way is to compose all children of a Free [...] node using (>>=), collecting their results in a final list. This can be seen as a generalization of depth-first search.

You get the result [7] or [5,7,1] depending on how those transformations are ordered.

Of course, there is a correspondence to the two orders of monad transformers in a MTL approach, but that intuition of programs as trees, which is generally applicable to all algebraic effects, is not as obvious when you're in the middle of implementing an instance such as MonadError e for ListT. That intuition might make sense a posteriori, but it is a priori obfuscated because type class instances are not first-class values like handlers, and monad transformers are typically expressed in terms of the final interpretation (hidden in the monad m they transform) instead of the initial syntax.

like image 93
Li-yao Xia Avatar answered Nov 10 '22 16:11

Li-yao Xia