Published on December 6, 2014; tags: Haskell, Extensible effects

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!

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.

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?

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.

`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 `ZoomT`

s stacked on top of each other, thus handling multiple different `EffState`

effects simultaneously.

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!