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.

Answer 2

"Lifting" comes up many times in functional programming, not only in fmap but in many other contexts. Examples of "liftings" include:

• fmap :: (a -> b) -> F a -> F b where F is a functor
• cmap :: (b -> a) -> F a -> F b where F is a contrafunctor
• bind :: (a -> M b) -> M a -> M b where M is a monad
• ap :: F (a -> b) -> F a -> F b where F is an applicative functor
• point :: (_ -> a) -> _ -> F a where F is a pointed functor
• filtMap :: (a -> Maybe b) -> F a -> F b where F is a filterable functor
• extend :: (M a -> b) -> M a -> M b where M is a comonad

Other examples include applicative contrafunctor, filterable contrafunctor, and co-pointed functor.

All these type signatures are similar in one way: they map one kind of function between a and b into another kind of function between a and b.

In these different cases, the function types are not simply a -> b but have some kind of "twisted" types: e.g. a -> M b or F (a -> b) or M a -> b or F a -> F b and so on. However, each time the laws are very similar: twisted function types need to have identity and composition laws, and twisted composition needs to be associative.

For example, for applicative functors, we need to be able to compose functions of type F (a -> b). So we need to define a special "twisted" identity function (pure id :: F (a -> a) ) and a "twisted" composition operation, call it apcomp, with type signature F (a -> b) -> F (b -> c) -> F (a -> c). This operation needs to have identity and associativity laws. The ap operation needs to have identity and composition laws ("twisted identity maps to twisted identity" and "twisted composition maps to twisted composition").

Once we go through all these examples and derive the laws, we can prove that the laws turn out to be the same in all cases, if we formulate the laws via the "twisted" operations.

This is because we can formulate all these operations as functors in the sense of category theory. For example, for the applicative functor, we define two categories: the F-applicative category (objects a, b, ..., morphisms F(a -> b)) and the F-lifted category (objects F a, F b, ..., morphisms F a -> F b). A functor between these two categories requires us to have a lifting of morphisms, ap :: F(a -> b) -> F a -> F b. The laws of ap are completely equivalent to the standard laws of that functor.

Similar arguments hold for other typeclasses. We need to define categories, morphisms, composition operations, identity morphisms, and functors in each case. Once we verify that the laws hold, we will see that each of these typeclasses has an associated pair of categories and a functor between them, such that the laws of the typeclass are equivalent to the laws of these categories and the functor.

What have we gained? We have formulated the laws of many typeclasses in the same way (as the laws of categories and functors). This is a great economy of thought: we don't need to memorize all these laws each time; we can just memorize which categories and which functors need to be written down for each typeclass, as long as the methods of the typeclass can be reduced to some kind of "twisted lifting".

In this way, we can say that "liftings" are important and provide an application of category theory in functional programming.

I have made a presentation about this, https://www.youtube.com/watch?v=Zau8CxsfxOo and I'm writing a new free book where all derivations will be shown. https://github.com/winitzki/sofp