Recursive lifting

I looked at some MonadTrans instances, for MaybeT the implementation looks like this:

instance MonadTrans MaybeT where
    lift = MaybeT . liftM Just

      

As I understand it, the instance for MonadIO is used to make a variable number of lifts from the innermost, IO monad, directly to the outermost. For the MaybeT case, it looks like this:

instance (MonadIO m) => MonadIO (MaybeT m) where
    liftIO = lift . liftIO

      

I don't understand how this recursive function breaks out of an infinite loop. What is a base case?

+3


source to share


2 answers


Perhaps surprisingly, the definition below is not recursive, even if it looks like this.

instance (MonadIO m) => MonadIO (MaybeT m) where
    liftIO = lift . liftIO

      

This is because the liftIO

left side is liftIO

for the monad MaybeT m

and the right side liftIO

is liftIO

for the monad m

.

Hence, it simply defines liftIO

in one monad in terms of liftIO

another monad. There is no recursion here.

It looks like, for example,



instance (Show a, Show b) => Show (a,b) where
   show (x,y) = "(" ++ show x ++ ", " ++ show y ++ ")"

      

Above, we define how to print a pair depending on how you print your components. It looks like it is recursive, but it really isn't.

It can help visualize this by inserting explicit type arguments, at least mentally:

-- pseudo-code
instance (Show a, Show b) => Show (a,b) where
   show @(a,b) (x,y) = 
      "(" ++ show @a x ++ ", " ++ show @b y ++ ")"

      

Now show @(a,b)

, show @a

and show @b

are different functions.

+5


source


Simple definitions of conditional reasoning and rewriting for some specialization might help you. Basic case for MonadIO

equal IO

. MaybeT

is a monad transformer, so let's combine MaybeT

and IO

in some simple example.

foo :: MaybeT IO String
foo = liftIO getLine

      

Now, let's rewrite this function definition using the instance implementations from your question step by step.



foo
= liftIO {- for MaybeT -} getLine
= lift (liftIO {- for IO here -} getLine)  -- step 2
= lift (id getLine)
= lift getLine
= MaybeT (liftM Just getLine)

      

  • getLine

    is of type IO String

  • liftM Just getLine

    is of type IO (Maybe String)

  • MaybeT m a

    the constructor needs a value of the type m (Maybe a)

    , where m = IO

    and a = String

    in our case.

Probably the hardest step to analyze is step 2. But itโ€™s actually very easy if you remind yourself of the types liftIO :: IO a -> m a

and lift :: Monad m => m a -> t m a

. Thus, all the work is done by inference type.

+4


source







All Articles