How does lifting (in a functional programming context) relate to category theory?

Question

Looking at the Haskell documentation, lifting seems to be basically a generalization of fmap, allowing for the mapping of functions with more than one argument.

The Wikipedia article on lifting gives a different view however, defining a "lift" in terms of a morphism in a category, and how it relates to the other objects and morphisms in the category (I won't give the details here). I suppose that that could be relevant to the Haskell situation if we are considering Cat (the category of categories, thus making our morphisms functors), but I can't see how this category-theoretic notion of a lift relates the the one in Haskell based on the linked article, if it does at all.

If the two concepts aren't really related, and just have a similar name, are the lifts (category theory) used in Haskell at all?

Answer 1

Lifts, and the dual notion of extensions, are absolutely used in Haskell, perhaps most prominently in the guise of comonadic extend and monadic bind. (Confusingly, extend is a lift, not an extension.) A comonad w's extend lets us take a function w a -> b and lift it along extract :: w b -> b to get a map w a -> w b. In ASCII art, given the diagram

        w b
         |
         V
w a ---> b

where the vertical arrow is extract, extend gives us a diagonal arrow (making the diagram commute):

     -> w b
    /    |
   /     V
w a ---> b

More familiar to most Haskellers is the dual notion of bind (>>=) for a monad m. Given a function a -> m b and return :: a -> m a, we can "extend" our function along return to get a function m a -> m b. In ASCII art:

a ---> m b
|
V
m a

gives us

a ---> m b
 |  __A
 V /
m a

(That A is an arrowhead!)

So yes, extend could have been called lift, and bind could have been called extend. As for Haskell's lifts, I have no idea why they're called that!

EDIT: Actually, I think that again, Haskell's lifts are actually extensions. If f is applicative, and we have a function a -> b -> c, we can compose this function with pure :: c -> f c to get a function a -> b -> f c. Uncurrying, this is the same as a function (a, b) -> f c. Now we can also hit (a, b) with pure to get a function (a, b) -> f (a, b). Now, by fmaping fst and snd, we get a functions f (a, b) -> f a and f (a, b) -> f b, which we can combine to get a function f (a, b) -> (f a, f b). Composing with our pure from before gives (a, b) -> (f a, f b). Phew! So to recap, we have the ASCII art diagram

  (a, b) ---> f c
    |
    V
(f a, f b)

Now liftA2 gives us a function (f a, f b) -> f c, which I won't draw because I'm sick of making terrible diagrams. But the point is, the diagram commutes, so liftA2 actually gives us an extension of the horizontal arrow along the vertical one.