When exactly is lifting needed in monad transformers?

Question

I am learning monad transformers and I am confused about when using lift is necessary. Assume that I have the following code (It's not doing anything interesting, just the simplest I could come with for demonstration).

foo :: Int -> State Int Int
foo x = do
  (`runContT` pure) $ do
    callCC $ \exit -> do
      when (odd x) $ do
        -- lift unnecessary
        a <- get
        put $ 2*a
      when (x >= 5) $ do
        -- lift unnecessary, but there is exit 
        a <- get
        exit a
      when (x < 0) $ do
        -- lift necessary
        a <- lift $ foo (x + 10)
        lift $ put a

      lift get

So there is a monad stack, where the main do block has type ContT Int (StateT Int Identity) Int.

Now, in the third when do block with recursion a lift is required for the program to compile. In the second block, there is no lift needed, but I somehow assume it's because of the presence of exit which somehow forces the line above line to be lifted to ContT. But in the first block, no lift is required. (But if it's explicitly added, there is no problem either.) This is really confusing to me. I feel all the when do blocks are equivalent and either the lift should be required everywhere or nowhere. But that's apparently not true. Where is the key difference that makes the lift required/not required?

score 10 · Accepted Answer · answered Jul 21 '17 at 11:25

The confusion here is arising because the monad transformer library you're using is being a bit clever. Specifically, the type of get and put doesn't explicitly mention State or StateT. Rather, they are along the lines

get :: MonadState s m => m s
put :: MonadState s m => s -> m ()

Therefore as long as we use this in a context with a MonadState implementing monad there is no need for explicit lifts. This is the case in all the instances where you use get/put since

instance MonadState s (StateT s m)
instance MonadState s m => ContT k m

both hold. In other words, the type class resolution will automatically handle doing the appropriate lifting for you. This in turn implies that you could elide the lifts on the get/put at the end of your program.

This cannot happen with your recursive calls because its type is explicitly State Int Int. If you generalized it to MonadState Int m => m Int you could even elide this final lift.

score 6 · Answer 2 · answered Jul 21 '17 at 15:59

I would like to provide an alternate answer that is both superficial and at the same time everything important.

You need to use lift when lift makes things type check that otherwise don't.

Yes, it sounds superficial and appears to lack any deep meaning. But that's not quite true. MonadTrans is a class for things that can lift monadic actions into a larger context in a neutral way. The class laws provide more explicit rules about what "neutral" means, if you want a technical description. But the upshot is that lift does nothing beyond what is necessary to make the provided action compatible with another type.

So - what does lift do? It provides the logic necessary for lifting a monadic action into a bigger type. When do you need to use it? When you have a monadic action that you need to lift into a bigger type. When do you have a monadic action that you need to lift into a bigger type? When that's what the types tell you.

This is a key part of using Haskell. You can modularize your understanding of code. The type system keeps track of a huge amount of bookkeeping for you. Rely on it to get the bookkeeping right, so you only need to keep the logic in your head. The compiler and type system are there to work as mental amplifiers. The more they take care of, the less you need to keep in your head while writing software.

When exactly is lifting needed in monad transformers?

2 Answers2