# Type-based lift

*July 15, 2014*

In mtl, the `ask`

method of the `MonadReader`

class will automatically «lift» itself to the topmost `ReaderT`

layer in the stack, which is very convenient, but only works as long as the topmost layer is the one you need. If you have multiple `ReaderT`

s in the stack, you often have to insert manual lifts.

Previously I described why a smarter automatic lifting mechanism is needed to build truly reusable pieces of monadic code without too much boilerplate.

In this article I show two ways to achieve a type-based lift (that is, a lift which takes into account the `r`

of `ReaderT r`

), one relying on `IncoherentInstances`

, the other — on closed type families.

## Class-based approach and IncoherentInstances

In Two failed attempts at extensible effects, I wrote that simply removing the fundep from mtl wouldn’t work. This claim was recently disproved by Ben Foppa and his extensible-transformers library.

Why did I think that such an approach wouldn’t work?

```
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, OverlappingInstances #-}
import Control.Monad.Trans.Reader hiding (ask)
import qualified Control.Monad.Trans.Reader as Trans
import Control.Monad.Trans.Class
class MonadReader r m where
ask :: m r
instance Monad m => MonadReader r (ReaderT r m) where
ask = Trans.ask
instance (Monad m, MonadReader r m, MonadTrans t) => MonadReader r (t m) where
ask = lift ask
```

GHC, when asked to compile something that uses the above instances, will ask you in return to enable the `IncoherentInstances`

extension. My experience with GHC told me that such a request is just a polite way for GHC to say «You’re doing something wrong!», so I immediately dismissed that approach. I had never seen a case where `IncoherentInstances`

would be an acceptable solution to the problem. Well, this one seems to be exactly such a case!

Switching `IncoherentInstances`

on here not only makes the type checker happy, but also makes the code work as expected, at least in the few tests that I tried.

## Closed type classes

Intuitively, the reason why GHC needs so many ugly extensions to make the above code work is that we’re trying to simulate a closed type class with an open one.

Our type class is essentially a type-level *if* operator comparing two types, and its two instances correspond to the two branches of the *if* operator.

If only we had closed type classes, we could write

```
import Control.Monad.Trans.Reader hiding (ask)
import qualified Control.Monad.Trans.Reader as Trans
import Control.Monad.Trans.Class
class MonadReader r m where
ask :: m r
instance Monad m => MonadReader r (ReaderT r m) where
ask = Trans.ask
instance (Monad m, MonadReader r m, MonadTrans t) => MonadReader r (t m) where
ask = lift ask
```

(where I put instance declarations inside the class declaration to show that the class is closed).

Alas, GHC 7.8 does not have closed type classes, and I have not even heard of them being developed. All we have is closed type families. Closed type families would let us compute, say, a type-level number showing how far we have to `lift`

a monadic action to reach the right level. They, however, do not allow us to compute a value-level witness — the very lifting function!

## Closed type families

Still, it is possible to achieve automatic lifting using closed type families alone. We developed this approach together with Andres Löh at ZuriHac’14.

The main idea is to split the problem into two.

First, we compute the amount of lifting required using a closed type family

```
-- Peano naturals, promoted to types by DataKinds
data Nat = Zero | Suc Nat
type family Find (t :: (* -> *) -> (* -> *)) (m :: * -> *) :: Nat where
Find t (t m) = Zero
Find t (p m) = Suc (Find t m)
```

Second, assuming we know how far to lift, we can compute the lifting function using an ordinary (open) MPTC:

```
class Monad m => MonadReaderN (n :: Nat) r m where
askN :: Proxy n -> m r
instance Monad m => MonadReaderN Zero r (ReaderT r m) where
askN _ = Trans.ask
instance (MonadTrans t, Monad (t m), MonadReaderN n r m, Monad m)
=> MonadReaderN (Suc n) r (t m)
where
askN _ = lift $ askN (Proxy :: Proxy n)
```

It is important to note that our instances of `MonadReaderN`

are non-overlapping. The instance is uniquely determined by the `n :: Nat`

type parameter.

Finally, we glue the two components together to get a nice `ask`

function:

```
-- Nice constraint alias
type MonadReader r m = MonadReaderN (Find (ReaderT r) m) r m
ask :: forall m r . MonadReader r m => m r
ask = askN (Proxy :: Proxy (Find (ReaderT r) m))
```

## Problem solved?

Not quite. Both solutions described here do abstract from the position of a monad transformer in the stack, but they do not abstract from the transformer itself. The `MonadReader r`

constraint can only be satisfied with `ReaderT r`

but not, say `StateT r`

. Moreover, a `MonadState`

constraint, defined as

`type MonadState s m = MonadStateN (Find (Control.Monad.State.Lazy.StateT s) m) s m`

can only be satisfied by the lazy, but not strict, `StateT`

.

I address this issue in the subsequent article.