How does lifting (in a functional programming context) relate to category theory?
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 lift
s, I have no idea why they're called that!
EDIT: Actually, I think that again, Haskell's lift
s 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 fmap
ing 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.