![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
I'm sure this is all well-known by the hardcore category theorists, but I don't have any references because I just invented it myself. This is going to involve some higher-order category theory, but I'm not going to be theoretical about it so don't worry if you have trouble grasping basic (first-order) category theory. I'll give some suggestive sounding theory, but I haven't verified it or bothered to figure out what other people call these things.
So what is a monad? A nice pithy explanation, which explains very little to the uninitiated, is that it is "a monoid on the category of endofunctors (for some category
First let's consider, not a single monad, but rather, a family of monads. For instance, the family of Reader monads indexed by the type of things they read, or the family of Writer monads indexed by the type of things they write. It's clear that the definition of Reader or Writer is independent of the type of thing read/written; that is, Reader and Writer are natural in their "state". But note that this is different than the fact that they, like any functor, are natural in the type of their "contents". The trivial thing is to just come up with a theory for each of the individual monads in these families, but we can generalize our notion of monads by trying to come up with a theory for describing the entire family as a single entity. If we called our original construction 0-monads, then we could call this generalization 1-monads.
In a sense, we've moved to talking about "a family of monoids on the category of endofunctors for some family of categories". Or another way of saying that which brings out the unity a bit more is that it's "a ___ on the category of categories-of-endofunctors" (leaving the blank there to simplify the discussion). But notice that our category of categories-of-endofunctors isn't very interesting. There are no arrows in this category other than those that have to be there and those induced by out 1-monad. That is, we have no way to get from a
If we wanted to make the carrier set closed under composition we could add some structure allowing us to transform
But we can take things further and discuss arbitrary functors instead of just endofunctors. For this to make sense, consider a family of 0-monads which has two indices, the State monad for instance. The State monad is just the composition of the Reader and Writer monads. In the usual implementation we use the same type for reading as for writing, but there's no reason we have to restrict ourselves thus. If we distinguish the reading type and the writing type then we'll need two indices, one naming each type. We can call such beasts 2-monads for obvious reasons. So how can we reason about 2-monads? Well, in the case that both indices are the same then it degenerates into behaving like a 1-monad. And in the case that the range of indices is singleton, a 1-monad degenerates into behaving like a 0-monad. But what happens to composition when the two indices are different? One natural thing we may want to have is the ability to transform
So let's go over the progression again. The original definition of monads describes a certain sort of structure on a category of categories-of-endofunctors. But the category (of C-of-E) was restricted to have a single object. Extending the definition to cover families of monads with a single index gives us the same structure but allows the category to have more than one object. However the category still has no arrows other than those induced by the 1-monadic structure. Extending the definition once again to cover families of monads with two indices gives us the same monadic structure, but allows the category to have arrows, one for each 0-monad instance of the 2-monad. Of course, for it to be a category we must have that for every composition
We could also consider enriching 1-monads to have exponentials for indices, i.e.
But note that the "function composition" nature of 2-monads or CCC-1-monads is orthogonal to the usual "function composition" arising from monads being applicative functors. That is, the natural transformation for applicative-application allows us to transform a value of type
So what is a monad? A nice pithy explanation, which explains very little to the uninitiated, is that it is "a monoid on the category of endofunctors (for some category
C)". Don't worry about fitting that all together, but do think for a moment about each of the individual words. First off, it's a monoid of some sort, which means that it has an associative operation (join) and an identity thingy for that operation (unit/return). Ignore the category part, or just think of it as meaning "set". Second off, it involves endofunctors, that is it involves a mapping of some particular category, C, to itself. But neither of those two aspects is crucial to the role that monads play in programming, and both can be generalized to gain a more powerful design pattern.First let's consider, not a single monad, but rather, a family of monads. For instance, the family of Reader monads indexed by the type of things they read, or the family of Writer monads indexed by the type of things they write. It's clear that the definition of Reader or Writer is independent of the type of thing read/written; that is, Reader and Writer are natural in their "state". But note that this is different than the fact that they, like any functor, are natural in the type of their "contents". The trivial thing is to just come up with a theory for each of the individual monads in these families, but we can generalize our notion of monads by trying to come up with a theory for describing the entire family as a single entity. If we called our original construction 0-monads, then we could call this generalization 1-monads.
In a sense, we've moved to talking about "a family of monoids on the category of endofunctors for some family of categories". Or another way of saying that which brings out the unity a bit more is that it's "a ___ on the category of categories-of-endofunctors" (leaving the blank there to simplify the discussion). But notice that our category of categories-of-endofunctors isn't very interesting. There are no arrows in this category other than those that have to be there and those induced by out 1-monad. That is, we have no way to get from a
(Reader A X) to a (Reader B X) using only the fact that they're both Readers. Also note that the join transformation is no longer a monoid. With a 0-monad M we can transform M∘M into M; but with a 1-monad N there's no general way to transform (N A)∘(N B), what would we transform it into? So composition is no longer total, or the carrier is no longer closed under composition, either way composition isn't a monoid.If we wanted to make the carrier set closed under composition we could add some structure allowing us to transform
(N A)∘(N B) into N(A×B). In this generalization we've introduced an additional way in which 1-monads are monoidal. If the original N which did not allow these compositions had S as the set of possible indices, then this new N is indexed by the free monoid generated by S. In the original N, each index effectively names an object of our category, that is the index names a particular category-of-endofunctors, and thus names a particular category (which the endofunctor acts on). With the new N it's not entirely clear what the indices are naming. In this second generalization we've declared that our category of C-of-E has products, and those products (whatever they mean) are the indices.But we can take things further and discuss arbitrary functors instead of just endofunctors. For this to make sense, consider a family of 0-monads which has two indices, the State monad for instance. The State monad is just the composition of the Reader and Writer monads. In the usual implementation we use the same type for reading as for writing, but there's no reason we have to restrict ourselves thus. If we distinguish the reading type and the writing type then we'll need two indices, one naming each type. We can call such beasts 2-monads for obvious reasons. So how can we reason about 2-monads? Well, in the case that both indices are the same then it degenerates into behaving like a 1-monad. And in the case that the range of indices is singleton, a 1-monad degenerates into behaving like a 0-monad. But what happens to composition when the two indices are different? One natural thing we may want to have is the ability to transform
(L A B)∘(L B C) into (L A C). Certainly this pattern should look familiar. It's the same "monoidal" pattern that defines a category, and the same as plain old function composition.So let's go over the progression again. The original definition of monads describes a certain sort of structure on a category of categories-of-endofunctors. But the category (of C-of-E) was restricted to have a single object. Extending the definition to cover families of monads with a single index gives us the same structure but allows the category to have more than one object. However the category still has no arrows other than those induced by the 1-monadic structure. Extending the definition once again to cover families of monads with two indices gives us the same monadic structure, but allows the category to have arrows, one for each 0-monad instance of the 2-monad. Of course, for it to be a category we must have that for every composition
(L A B)∘(L B C) there also exists an equivalent 0-monad (L A C)— otherwise we don't have all compositions, and thus it wouldn't be a category. We've essentially replaced the term "monoid" in our original definition for 0-monads with the term "category".We could also consider enriching 1-monads to have exponentials for indices, i.e.
N(A→B). If we have the version of "composition" which takes (N A)∘(N B) to N(A×B), and we also have a natural transformation taking N((A→B)×A) to (N B), then the category of categories-of-endofunctors is cartesian closed. Thus, if we allow exponential indices and have some additional structure, then we can embed 2-monads in our 1-monadic CCC.But note that the "function composition" nature of 2-monads or CCC-1-monads is orthogonal to the usual "function composition" arising from monads being applicative functors. That is, the natural transformation for applicative-application allows us to transform a value of type
(L A B (X→Y) × L A B X) into a value of type (L A B Y). There's an entirely different natural transformation which allows us to transform a value of type (L A B (L B C X)) into a value of type (L A C X). Of course we can combine the two and construct a natural transformation which allows us to take a value of type (L A B (X→Y) × L B C X) into a value of type (L A C Y).
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
Indexed and Parameterized Monads
Date: 2010-04-05 12:40 pm (UTC)From:-Edward Kmett
Re: Indexed and Parameterized Monads
Date: 2010-04-05 11:08 pm (UTC)From:But considering some of the mysticism around "those ineffable monads", I figured it'd be of general interest (ala the link to Dan's other post). There's much more to axiomatizing "computation" than monads, but people get so hung up on unknown terminology. (And welcome to LJ, Ed :)