The center-of-mass monad While studying monads, I stumbled upon the following functor:
G t = (t -> r) -> t
This functor can be interpreted as giving a "center of mass" of a space according to a weight function: assume that
t comes from a vector space, that
f : t -> r is a weight function where
r is a number, and that we compute the center of mass by integrating over all vector space with the weight function f. The result is a certain point t in the space, which is the result of evaluating G t on a weight function f.
Regardless of the usefulness of this interpretation, it was fascinating to find that G t is actually a monad.
To see this, we need to define two natural transformations:
pure : t ~> G t
join : G (G t) ~> G t
Defining "pure" is straightforward: just return a constant function _ -> t that ignores its argument.
Defining "join" is more difficult. The type of "join" is written out as
join : ((((t->r)->t) -> r) -> (t->r)-> t) -> (t->r) -> t
We are required to produce a value of t, given a function h of type (((t->r)->t) -> r) -> (t->r)->t and a function f of type t->r. The only way of producing a value of t would be to use h on two arguments: one of type ((t->r)->t) -> r and another of type t->r. We already have a value f of type t->r. It remains to produce a function of type ((t->r)->t) -> r; in other words, to produce r given a value g of type (t->r)->t. We now evaluate g f to obtain a value of type t, and finally apply f to that value. Hence, f (g f) has type r as required.
All this verbiage is equivalent to the terse Haskell syntax
join gg = \f -> gg (\g -> f (g f)) f
It remains to verify that the monadic laws hold. There are three laws: left unit, right unit, and associativity, which are roughly written as.
pure . join = id
join . G(pure) = id
join . G(join) = join . join -- that is, G(G(G t))) can be reduced to G t via "join" in two different ways, which must be equivalent.
Here G(f) is the lifting of a function f into the functor G.
Verifying these laws is a somewhat tedious calculation that involves substituting "join" into itself several times.
As a generalization of these calculations, we can also show that the functor (M t -> r) -> M t is a monad if M is a monad.
This suggests a "monad transformer"
G : M t ~> (M t -> r) -> M t
As simpler cases, consider also that c -> M t and M(c -> t) are monads if M is one.