Recently, a fellow in category land discovered a fact that we in Haskell land have actually known for a while (in addition to things most of us probably don't). Specifically, given two categories and
, a functor
, and provided some conditions in
hold, there exists a monad
, the codensity monad of
.
In category theory, the codensity monad is given by the rather frightening expression: