Type-based lift

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