Search code examples
haskellcategory-theory

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


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?


Solution

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