|
| |||
|
|
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. |
||||||||||||||