
Dear Café, 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 with trans' . trans = id and 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. Olaf
participants (1)
-
Olaf Klinke