Exploring Adjunctions

Adjunctions.md

This might all be old-hat for you, but typing it out helps be understand it better anyways :)

Let's consider two examples as we talk about it, the first being curry/uncurry, the second being the case Hardy mentioned in an earlier episode where he had an adjunction between annotated/highlighted text and non-highlighted text.

Considering two Categories A and B; The definition of an adjunction (at least according to wikipedia) is a pair of Functors; F:A -> B and G:B -> A; so basically a pair of functors which map back and forth between categories. We also need an isomorphism between Hom-sets of the categories;

I believe the curry/uncurry example is a trivial adjunction because there's a direct Isomorphism between curried and uncurried functions; namely to = curry, from = uncurry, or vice versa. By proxy, there's also an isomorphism between their hom-sets; indeed for any isomorphism between elements of two categories there's an isomorphism between hom-sets as well, given the Iso between A and B, (toB and fromB respectively) we can define toHomB and fromHomB as follows:

toHomB :: (A -> A) -> (B -> B)
toHomB f = fromB . f . toB

fromHomB :: (B -> B) -> (A -> A)
fromHomB f = toB . f . fromB

Or in this example case, (though it's a bit less intuitive, because f is a function which operates on functions)

toUncurried = curry . f . uncurry
fromUncurried = uncurry . f . curry

So I'm pretty sure that any isomorphism is a trivial adjunction, so what makes adjunctions special? I think it's that they can (and typically do) LOSE information in the conversion, (hence the 'approximation/estimation' analogy you mentioned). The other example fits this idea.

Let's imagine simple Highlighted text as a tuple: (Bool, String); i.e. there's some text and it's either highlighted or not. We can imagine Free and Forgetful functors. The free functor will simply lift a string into a tuple with a default of being not highlighted, something like pure

newtype Highlighted = Highlighted (Bool, String)
pure :: String -> Highlighted
pure str = Highlighted (False, str)

The forgetful functor will extract it, forgetting whether it was highlighted or not:

extract :: Highlighted -> String
extract (Highlighted (_, str)) = str

There's clearly no isomorphism between the two since the highlighted text has more information; yet we can define an isomorphism for the hom-set:

toHomHighlighted :: (String -> String) -> (Highlighted -> Highlighted)
toHomHighlighted f = unlift . f . lift

fromHomHighlighted :: (Highlighted -> Highlighted) -> (String -> String)
fromHomHighlighted = lift . f . unlift

So we have an adjunction. Clearly information is lost in the transfer, which is why it's an adjunction but not an isomorphism.

EDIT: apparently a tuple like this represents the Product Comonad; Dominic talks about this (and also curry/uncurry) in this paper

By this token I think we can come up with a few more examples of adjunctions; I think you were on to something talking about how every adjunction defines a co-monad. I'm not sure about this, but I think any type with Applicative and Comonad could be an adjunction by using pure and extract just like we did above.

Let's consider zippers over a list which are comonads as another example:

-- A zipper contains the values to the left, the focus, and the values to the right
data Zipper a = Zipper [a] a [a]

The left-adjoint here is pure from Applicative, there are several applicative instances we could write, but we really only care about pure:

pure :: a -> Zipper a
pure a = Zipper [] a []

And extract comes from the comonad of the zipper; but it's simply:

extract :: Zipper a -> a
extract (Zipper _ a _) = a

So our Adjunction uses Free and Forgetful functors again, we have a Free functor to wrap any value in a zipper (pure); and a forgetful functor (extract) which 'forgets' all unfocused elements of the zipper, whether it's a useful adjunction, I'm not sure 😉