Extensible effects: abstracting from the transformer

In Type-based lift, we saw a way to lift monadic actions automatically to the right layer of a multilayer monad transformer stack, based only on the types involved.

Namely, we defined a closed type family

type family Find (t :: (* -> *) -> (* -> *)) (m :: * -> *) :: Nat where
  Find t (t m) = Zero
  Find t (p m) = Suc (Find t m)

that computes the type-level index of the layer t in the stack m. Such an index can then be used to construct an appropriate lifting function of type t n a -> m a.

This works well as a shortcut, so instead of writing lift, or lift . lift, or lift . lift . lift, we can write magicLift, and let it figure out how far to lift.

However, the lifting is expressed in terms of specific transformers, and not the effects they can handle. For example, a stateful computation may target the strict State monad or the lazy one, but not both, because they are implemented by distinct types.

Let’s fix this!

CanDo

To know which effects can be handled by each transformer, we’ll introduce a new type family, CanDo:

type family CanDo (m :: (* -> *)) (eff :: k) :: Bool

Now we need to modify the Find family to find the first (top-most) layer for which the CanDo predicate will return True. Since on the type level we don’t have lambdas and case statements, doing so is a bit cumbersome but still possible:

type family MapCanDo (eff :: k) (stack :: * -> *) :: [Bool] where
  MapCanDo eff (t m) = (CanDo (t m) eff) ': MapCanDo eff m
  MapCanDo eff m = '[ CanDo m eff ]

type family FindTrue (bs :: [Bool]) :: Nat where
  FindTrue (True ': t) = Zero
  FindTrue (False ': t) = Suc (FindTrue t)

type Find eff (m :: * -> *) = FindTrue (MapCanDo eff m)

Next, we need to introduce dummy types denoting effects, and relate them to transformers:

import qualified Control.Monad.Trans.State.Lazy as SL
import qualified Control.Monad.Trans.State.Strict as SS

data EffState (s :: *)
data EffWriter (w :: *)
data EffReader (e :: *)

type instance CanDo (SS.StateT s m) eff = StateCanDo s eff
type instance CanDo (SL.StateT s m) eff = StateCanDo s eff

type family StateCanDo s eff where
  StateCanDo s (EffState s) = True
  StateCanDo s (EffReader s) = True
  StateCanDo s (EffWriter s) = True
  StateCanDo s eff = False

As we see, the relationship between effects and transformers is many-to-many. A single effect can be implemented by multiple transformers, and a single transformer can implement multiple effects.

Should StateT implement EffReader?

It’s not only for demonstration that I made StateT implement the EffReader effect. One can view EffReader (and EffWriter) computations as a subclass of all stateful computations

Suppose that you have two computations with the same state that you want to execute sequentially, but one of them only needs read access to the state. Why not express that fact in its type?

Other cool tricks

Here are a couple of cool (and useful!) tricks that are possible with extensible effects. I will only describe what they do and not how they’re implemented; you can find all code in the repo.

Zooming

newtype ZoomT big small m a = ...

ZoomT handles EffState small effects by transforming them to EffState big effects. To enable this, we must supply a lens from big into small:

runZoom
  :: Lens big small 
  -> ZoomT big small m a
  -> m a

Compared to traditional zooming (as in lens), where we can only focus on a single state at a time, here we can apply many ZoomTs stacked on top of each other, thus handling multiple different EffState effects simultaneously.

Custom Writer handlers

The classic use case for a Writer monad is logging. Ironically, the way a writer monad does logging (accumulating log messages in memory) is wrong for almost all purposes, and possible right ways (flushing messages to disk or sending them over the network) are out of reach for it.

newtype CustomWriterT w m a = ...

evalWriterWith
  :: (w -> m ())
  -> CustomWriterT w m a
  -> m a

The idea here is that CustomWriterT handles EffWriter effect by calling the given handler for it — exactly what we wanted!