The Cont adjunction

https://gist.github.com/Lysxia/beb6f9df9777bbf56fe5b42de04e6c64

newtype (<-:) a b = Co { unCo :: b -> a }

-- The composition of adjoint functors is a monad or a comonad (depending on which way it goes)
newtype Compose f g a = Compose { unCompose :: f (g a) }

-- The continuation monad as an adjunction:
type Cont r = Compose ((<-:) r) ((<-:) r)

runCont :: Cont r r -> r
runCont (Compose (Co f)) = f (Co id)

Reason Isomorphically!

http://www.cs.ox.ac.uk/people/daniel.james/iso/iso.pdf

When are two types the same? In this paper we argue that isomorphism is a more useful notion than equality. We explain a succinct and elegant approach to establishing isomorphisms, with our focus on showing their existence over deriving the witnesses. We use category theory as a framework, but rather than chasing diagrams or arguing with arrows, we present our proofs in a calculational style. In particular, we hope to showcase to the reader why the Yoneda lemma and adjunctions should be in their reasoning toolbox.