# Type-based lift

Published on

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
= Trans.ask
ask
instance (Monad m, MonadReader r m, MonadTrans t) => MonadReader r (t m) where
= lift ask 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
= Trans.ask
ask
instance (Monad m, MonadReader r m, MonadTrans t) => MonadReader r (t m) where
= lift ask 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
= Trans.ask
askN _
instance (MonadTrans t, Monad (t m), MonadReaderN n r m, Monad m)
=> MonadReaderN (Suc n) r (t m)
where
= lift $ askN (Proxy :: Proxy n) askN _
```

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
= askN (Proxy :: Proxy (Find (ReaderT r) m)) ask
```

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