§ Adjunctions as advice
An adjunction F |- U allows us to go from F a -> x to a -> U x. We
can look at this as shifting the "before-advice" from the input to an
"after advice" of the output , where I'm using
Also, to remember this, we can write it as:
F a <--F--- a
| |
v v
x ----U--> U x
Where F is for Free and U is for forgetf Ul.
Recall that if F is free and U is forgetful, then U(F(x)) = x, since
adding more structure through the free functor and then stripping it away gives
us the object back. We can prove that if U(F(x)) = x and U, F are functors,
then we have a function fwd: (f a -> x) -> (a -> u x) as:
f :: (f a -> x)
fmap :: (p -> q) -> (u p -> u q)
fmap :: (p -> q) -> (u ( p ) -> u q)
fmap f :: (f a -> x) -> (u (f a) -> u x)
fmap f :: (f a -> x) -> (a -> u x) [using u (f a) = a]
§ References