haskellmonadsmonad-transformerslifting

When exactly is lifting needed in monad transformers?


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?


Solution

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