|
| |||
|
|
Exponential-polynomial monads Monadic functors represent computational contexts that can be linearly concatenated such that the later computational contexts may depend on the earlier ones. The defining properties of a monadic functor are the existence of two natural transformations "point": Id ~> M [that is, t ~> M t] and "join": M ∘ M ~> M [that is, M (M t) ~> M t]. All polynomial and recursive polynomial functors are monadic as long as they are pointed. (Of course, some monad implementations may be more interesting than others.) What about exp-polynomial functors? It is not easy to characterize those functors, except by building them up from simpler parts. The simplest exp-polynomial functor is the Reader functor Reader t = c -> t where c is a fixed type. The Reader functor is monadic, and it can be generalized to monads of the form c -> M t where M is another monadic functor. Statement 1. The functor F t = c -> M t is a monadic functor if M is monadic, where c is a fixed type. Proof. The "join" map for F must have the type F (F t) = (c -> M(c -> M t)) ~> F t = c -> M t. Since we have c, we can obtain M(c -> M t). Now we can also map c -> M t into M t, using modus ponens with the same value of type c. Thus we can map M(c -> M t) into M(M t) and hence, using M-join, into M t. The map t -> F t = t -> c -> M t is simply the M-point that ignores the "c" argument. Q.E.D. More complicated exp-polynomial functors are built as maps from contrafunctors. The simplest example of a contrafunctor is the "contra-representable" S t = t -> c (where c is a fixed type). If S is a contrafunctor and A is a functor then S t -> A t is again a functor. The next statement uses a map from a contrafunctor to construct a new monad out of a given monad. Statement 2. S t -> M t is a monadic functor if M is monadic and co-pointed (i.e. we have M t ~> t), and S is any contrafunctor. Proof. The natural transformation t ~> S t -> M t is simply the M-point that ignores the S t argument. It remains to produce a natural transformation (S(S t -> M t) -> M(S t -> M t)) ~> S t -> M t. The only way to get M t is to map from M(...) to M t. Since we have a value of type S t and no other value of type M(...), the only way to proceed is to obtain a value of M(S t -> M t) and then map to M(M t) using our value of S t. Now it remains to find a value of S(S t -> M t). Since S is a contrafunctor, we can get S(S t -> M t) only if we can map S t -> M t into some x such that we have S x. The only value we actually have is S t. This value allows us to map (S t -> M t) into M t using modus ponens. By assumption, M is co-pointed, hence we can map M t -> t. Therefore, we can map (S t -> M t) into t. Since S is a contrafunctor, this allows us to map S t -> S(S t -> M t) and hence we obtain the required map. Q.E.D. The requirement that M be co-pointed seems to be significant. For example, M t = 1 + t is not co-pointed. The simplest nonconstant contrafunctor is S t = t -> c. Now, if we build the functor F t = S t -> M t = (t -> c) -> 1 + t, we find that F is not a monad (and not even an applicative functor). Co-pointed monads are few and far between. (One nontrivial example of a co-pointed monad is a "non-empty list" functor.) It appears that there aren't many exp-polynomial monads! One nontrivial example is the continuation monad Cont t = (t -> r) -> r where r is a fixed type. Note that the Cont monad cannot be derived using Statement 2 because the constant functor r is not a monad. It is significant that both fixed types in Cont are the same type "r": the functor F t = (t -> a) -> b is not a monad when "a" and "b" are different types! So generalizations are not possible in this direction. Another nontrivial example is the state monad: State t = s -> (t × s). The type is isomorphic to (s->s)×(s -> t), which looks like a product of the Reader monad s -> t and a constant type s -> s. However, the value of type s -> s is used nontrivially in the monadic transformations. It does not seem likely that the State monad can be generalized to a wide class of exp-polynomial monads. Yet another nontrivial example is the "density" monad D t = (t -> c) -> t and its generalization (M t -> c) -> M t for any monad M. The "density" monad satisfies the conditions of Statement 2 since t is a (trivially) co-pointed monad and S t = t -> c is a contrafunctor. The reason why (M t -> c) -> M t is a monad is that D is an exp-poly monad of the class that admits a monad transformer that puts the foreign monad M inside, -- that is, defining the transformed monad as D(M t). For the same reason, Cont(M t) = (M t -> c) -> c is always a monad for any monad M. Statement 1 can be seen as a particular case of the monad transformer construction for the Reader monad. |
||||||||||||||