[Haskell-cafe] bootstrapping a monad via continuations
olf at aatal-apotheke.de
Thu May 6 21:17:42 UTC 2021
I've been scratching my head over a monad instance. I wonder whether
there is a deeper theory behind this. Suppose you have a functor T and
you happen to find a special type r such that there is a natural
embedding into the continuation monad Cont r. More precisely, if there
are natural transformations
trans :: forall x. T x -> Cont r x
trans' :: forall x. Cont r x -> T x
trans' . trans = id
trans . trans' . return = return
trans . trans' . (=<<) (trans . f) = (=<<) (trans . f)
then you can define monad operations for T so that trans becomes a
monad morphism. Once that T is a monad, one can invoke a theorem from a
1970 paper by Anders Kock and obtain Eilenberg-Moore T-algebra
structure on r, and the entire monad structure of T can be recovered
from this single T-algebra.
Examples of this scheme in the mathematical literature are the Riesz
representation theorem, which identifies measures on X with a subset of
the space of real functionals (X -> R) -> R. Ultimately, the monad
structure of the functor of measures is encoded in the operation that
sends a measure on R to its mean.
Anders Kock's theorem says:
(1) There is a bijecitive correspondence between natural
transformations T -> Cont r and functions T r -> r.
(2) In particular if T is a monad, (1) restricts to a bijection between
monad morphisms and Eilenberg-Moore algebra structures.
(Incidentally, this is what underlies the continuation monad
transformer: Apply to the structure join :: m (m r) -> m r.)
It thus seems that my observation is a kind of converse to part (2),
namely if a function T r -> r is an Eilenberg-Moore algebra structure,
then T is a monad. The preceding sentence is self-referential though,
because the property of being an Eilenberg-Moore algebra depends on
monad structure already present.
As usual I suspect the answer in one of Edward Kmett's packages, but my
Category-Fu is not strong enough to identify the matching concept.
More information about the Haskell-Cafe