What's the general notion of lifting in haskell?

Learn
#1

Discussing what’s the appropriate name the function of type MonadError e m => e -> Maybe a -> m a, I said that this doesn’t seems to be a “lifting” operation for me, because we add some new thing to Nothing value (compare with liftEither :: MonadError e m => Either e a -> m a. However, I realized, that don’t understand enough, what’s lfiting is. Does the lifting in haskell (like lift from MonadTrans, liftEither etc.) somehow correspond categorical notion of lifting?

#2

My impression is that Haskell people use “lift” as a natural-language word (i.e., bendable to fit one’s intuition, no matter how misguided).

But I haven’t rigorously checked that any of them cannot fit the factor-through-h definition you found. (I am always surprised that someone can find a contrived, after-the-fact fitting.)

1 Like
#3

I’ve always used it for functions that, given two monads M and N, defines the mapping: forall x. M x -> N x (so a natural transformation).

The function you are considering with the type MonadError e m => e -> Maybe a -> m a is isomorphic to MonadError e m => M e a -> m a where data M e a = M e (Maybe a). The question then is whether this M e is a monad. I think it is if e is a monoid:

instance Monoid e => Functor (M e) where
  fmap = liftM
instance Monoid e => Applicative (M e) where
  pure x = M mempty (Just x)
  (<*>) = ap
instance Monad M where
  M e Nothing >>= _ = M e Nothing
  M e (Just x) >>= k =
    case k x of
      M e' (Just y) -> M (e <> e') (Just y)
      M e' Nothing -> M (e <> e') Nothing

The only thing left is to prove the monad laws. I believe that is indeed the case, but I have no formal proof.

In conclusion, I’d say it would be a lifting operation if you add the Monoid e constraint.

#4

I don’t think there’s any formal definition of “lift” in the general sense, but most examples of functions named “lift” or “lift-something” seem to follow the pattern of converting some action or function to an equivalent action or function that involves additional context, usually in the form of adding some * -> * type variable, constrainted to something like Functor, Monad, MonadTrans, or similar. Just check out a quick Hoogle search for “lift”, and see if you can intuit the common pattern from it.

2 Likes