Solution to Puzzle 1
Write out the types and then copy them to the term level.
instance Adjunction ((,) e) ((->) e) where
Solution to Puzzle 2
-- leftAdjunct :: ((e, a) -> b) -> (a -> (e -> b))
leftAdjunct u a e = u (e, a)
-- rightAdjunct :: (a -> (e -> b)) -> ((e, a) -> b)
rightAdjunct v (e, a) = v a e
This part requires some choices (type unification).
unit :: Adjunction f g => a -> g (f a)
unit = leftAdjunct id
Reasoning: To produce g (f a) we have leftAdjunct at our disposal. rightAdjunct wouldn't work because its g b is in negative position. Now, matching g (f a) against g b in our case says that b = f a. Hence
leftAdjunct :: (f a -> f a) -> (a -> g (f a))
and we can fill the first argument with id.
counit :: Adjunction f g => f (g a) -> a
counit = rightAdjunct id
Reasoning: Now the roles are reversed. We want to consume f (g a). This means
only a premise with f (g a) in negative position will be (or at least is likely to be) relevant. That premise is rightAdjunct. This time, matching f (g a) against f a gives a = g a (different a's). Hence
rightAdjunct :: (g a -> g b) -> (f (g a) -> b)
and after identifying the type variables a and b we can fill the first argument
again with id.
Further reflection on positive and negative positions: In both leftAdjunct and rightAdjunct both a and b occur in both positive and negative position. a has positive position in f a since f is a covariant functor, not contravariant. The difference is that leftAdjunct has f and g in positive position, and rightAdjunct has them in negative position.
I think I first encountered the notion of positive and negative positions in an error message in Agda. Something like https://stackoverflow.com/questions/2583337/strictly-positive-in-agda. There is an air of fundamentality about it. Or maybe it's just part of our boolean culture.