[Haskell-cafe] Functional programmer's intuition for adjunctions?

[Dan Piponi]

Edsko asked:

>  Is there an intuition that can be used to explain adjunctions to
>  functional programmers, even if the match isn't necessary 100% perfect
>  (like natural transformations and polymorphic functions?).

I think there's a catch because many interesting examples of
adjunctions involve multiple distinct categories. So there's a sense
in which you have to go outside of programming to explain what they
are, apart from a few simple examples like currying. But if you're
familiar with the category of monoids and monoid homomorphisms, then
we can generate another example:

One intuition is the notion of trying to approximate an object in one
category using objects in another.

For example, consider the category of monoids. How best can we
approximate an arbitrary type in a monoid? Suppose our type, T, has
elements a,b and c. We could try to represent this as a monoid. But
monoids should have products and an identity. So if the monoid
contains a,b and c it should also contain 1, ab, bc, abcba and so on.
And what should ab equal? Might it be the same as bc? The simplest
strategy is to assume that all of these products are distinct and
approximate the type T with the monoid containing 1, a, b and c and
assuming no element equals any other unless the monoid laws say so
(ie. 1a=a1=a). This is called the *f*ree monoid generated by T, and we
can write it F(T).

Now go the other way: given a monoid, S, how can we map it back to a
type? There's an obvious idea, just make a type whose elements are the
*u*nderlying elements of the monoid, discarding the multiplication
rule. Call this U(S). (We're treating Hask like Set here.)

So what's U(F(T))? T gets mapped to the free monoid generated by T,
and mapped back to the elements of this monoid. In other words, the
elements of U(F(T)) are (possibly non-empty) strings of elements of T.
So UF is the list type constructor.

Any homomorphism, f, between monoids is completely determined once you
know where a set of generators of the monoid map under the
homomorphism, and vice versa. All of the other elements can be deduced
using f(1) = 1 and f(xy)=f(x)f(y). So if F(a) is the free monoid
generated by a, then a homomorphism F(a)->b is completely determined
by a function a->U(b), and vice versa. We have an isomorphism
(F(a)->b) <-> (a->U(b)) and (F,U) forms an adjunction, according to
Derek's definition.

So intuitively, what's going on is that Haskell lists emerge as a
result of an attempt to approximate types with monoids and adjunctions
formalise what we mean by 'approximation'. When we go from a type, to
a monoid, and back again, we don't end up where we started, but at a
new type.

Other adjunctions can be seen in this way. But because different
examples use different categories, it's hard to picture a uniform way
of viewing adjunctions that spans them all.

It's also no coincidence now that lists form a monad...
--
Dan