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