|
|
Пишет Journal de Chaource (![[info]](http://lj.rossia.org/img/syndicated.gif){kind=small} lj_chaource)@ 2020-04-05 07:07:00 |
 |
|
 |
|
|
|
|
|
|
 |
|
 |
Monad transformers are pointed functors in the category of monads
I have a new picture of monad transformers (as they are used in functional programming): they are pointed functors in the category of monads.
Programmers work in a Cartesian closed category whose objects are types (available in a chosen programming language) and whose morphisms are functions from one type to another.
Monads are endofunctors M in that category, with properties that there must exist a natural transformation eta: Id -> M and a natural transformation mu: M ◦ M -> M, and suitable laws of identity and associativity must hold, making mu a monoidal operation in a suitable sense.
In programming, monads are used to express various patterns of so called "effects" in computation, such as nested iteration, error handling, message logging, updating of global state, sequencing of concurrent operations, and many other things. These "effects" are represented by different monads, but the laws of all monads are the same. In category theory, we only look at the patterns of laws, since we are not able to talk about specific programs.
So, the first step is to consider the category of monads.
The category of monads is defined by its objects being various monads M, N, ..., and morphisms being natural transformations M -> N such that additional laws hold: the monad morphisms must preserve the monad methods eta and mu, in a suitable sense.
So, what is a monad transformer? It is a functor in the category of monads, which must be pointed and (optionally) co-pointed.
This concise formulation encompasses 18 different laws of monad transformers and defines everything in one phrase.
A functor T is pointed if there exists a natural transformation p: Id -> T. (Here Id is the identity functor.)
A functor T is pointed and co-pointed if there exists a natural transformation e: T -> Id such that the composition e ◦ p is equal to the identity transformation (Id -> Id).
Apply this construction to the category of monads, and assume that somebody gives us a functor T (in the category of monads) that is at the same time pointed and co-pointed. We then obtain the following:
1. By definition, the functor T maps monads M to new monads T(M), and it also maps monad morphisms f: M -> N to new monad morphisms T(f): T(M) -> T(N). This map T(.) is called the "runner". In programming, a runner is used to interpret operations of one monad in another. This construction lifts runners to the context of monad transformers.
2. The image of the identity monad under T is a certain monad T(Id), which is called the "base monad" of the transformer. Call this monad B = T(Id).
The monad T(M) is interpreted as a monad that describes the effects of B and also the effects of M. For example, if B is a monad that describes the error handling effect, then T(M) is a monad that describes whatever effects M is doing, plus error handling. Programmers expect to be able to work with the effects of B and M within T, as needed.
3. If, for some monad M, there exists a monad morphism M -> Id, we can lift it to T(M) -> T(Id) = T(M) -> B. This morphism, called "foreign runner", runs the effects of the monad M within the monad T(M), leaving just the effects of B.
4. Each monad M has eta: Id -> M (a natural transformation in the category of types, not in the category of monads). This natural transformation turns out to be also a monad morphism Id -> M in the category of monads. Lifting eta to T, we get T(eta): T(Id) -> T(M). This gives a monad morphism B -> T(M) called the "base lift". This embeds the effects of the base monad B into T.
5. The natural transformation p: Id -> T (in the category of monads) means that we have components p[M] for every monad M. The component at M is a monad morphism p[M]: M -> T(M). This morphism is called the "foreign lift". It embeds the effects of the "foreign monad" M into T.
6. The natural transformation e: T -> Id (in the category of monads) means that we have components e[M] for every monad M. The component at M is the monad morphism e[M]: T(M) -> M. This runs the effects of the base monad B within T, leaving just the effects of M.
7. Given two monad transformers T1 and T2, we can compute their functor composition T1 ◦ T2, which will be a new functor with exactly the same properties. (Monads don't compose, but monad transformers do, because they are functors in the category of monads.)
8. Since functor composition is associative, we may define a composition of any number of monad transformers, T1 ◦ T2 ◦ T3 etc. This composition is called a "monad stack".
The functions we derived (foreign lift, base lift, base runner, foreign runner, and their analogs in monad stacks) are important for practical use of monad transformers in programming. All their properties and laws follow directly from the assumption that T is a pointed and co-pointed functor in the category of monads.
According to this definition, however, the continuation monad has no transformer: The standard Haskell formula `ContT m r a = (a -> m r) -> m r` does not give a functor in the category of monads, because it is not covariant in the parameter m (the foreign monad). As a consequence, it is impossible to lift `Cont r a -> ContT m r a` for arbitrary monads m. The continuation monad is somewhat pathological also in that there are no monad morphisms Cont r -> Id that don't have side effects, violating the assumptions of purely functional code.
There are other perfectly good monads M without any monad morphisms M -> Id; it is not a problem by itself, as long as there are some other monad morphisms M -> N for suitable "simple enough" monads N. But I'm not sure that the continuation monad has any nontrivial morphisms at all to other monads.
Similarly, it would not be a problem if T were only a pointed functor and not co-pointed, as long as there are natural transformations T -> T' for some suitable "simple enough" functors T'.
Apart from the continuation monad, all known monads have transformers described by this construction.
The ordinary definition of monad transformers (say https://en.wikipedia.org/wiki/Monad_tran
I have a new picture of monad transformers (as they are used in functional programming): they are pointed functors in the category of monads.
Programmers work in a Cartesian closed category whose objects are types (available in a chosen programming language) and whose morphisms are functions from one type to another.
Monads are endofunctors M in that category, with properties that there must exist a natural transformation eta: Id -> M and a natural transformation mu: M ◦ M -> M, and suitable laws of identity and associativity must hold, making mu a monoidal operation in a suitable sense.
In programming, monads are used to express various patterns of so called "effects" in computation, such as nested iteration, error handling, message logging, updating of global state, sequencing of concurrent operations, and many other things. These "effects" are represented by different monads, but the laws of all monads are the same. In category theory, we only look at the patterns of laws, since we are not able to talk about specific programs.
So, the first step is to consider the category of monads.
The category of monads is defined by its objects being various monads M, N, ..., and morphisms being natural transformations M -> N such that additional laws hold: the monad morphisms must preserve the monad methods eta and mu, in a suitable sense.
So, what is a monad transformer? It is a functor in the category of monads, which must be pointed and (optionally) co-pointed.
This concise formulation encompasses 18 different laws of monad transformers and defines everything in one phrase.
A functor T is pointed if there exists a natural transformation p: Id -> T. (Here Id is the identity functor.)
A functor T is pointed and co-pointed if there exists a natural transformation e: T -> Id such that the composition e ◦ p is equal to the identity transformation (Id -> Id).
Apply this construction to the category of monads, and assume that somebody gives us a functor T (in the category of monads) that is at the same time pointed and co-pointed. We then obtain the following:
1. By definition, the functor T maps monads M to new monads T(M), and it also maps monad morphisms f: M -> N to new monad morphisms T(f): T(M) -> T(N). This map T(.) is called the "runner". In programming, a runner is used to interpret operations of one monad in another. This construction lifts runners to the context of monad transformers.
2. The image of the identity monad under T is a certain monad T(Id), which is called the "base monad" of the transformer. Call this monad B = T(Id).
The monad T(M) is interpreted as a monad that describes the effects of B and also the effects of M. For example, if B is a monad that describes the error handling effect, then T(M) is a monad that describes whatever effects M is doing, plus error handling. Programmers expect to be able to work with the effects of B and M within T, as needed.
3. If, for some monad M, there exists a monad morphism M -> Id, we can lift it to T(M) -> T(Id) = T(M) -> B. This morphism, called "foreign runner", runs the effects of the monad M within the monad T(M), leaving just the effects of B.
4. Each monad M has eta: Id -> M (a natural transformation in the category of types, not in the category of monads). This natural transformation turns out to be also a monad morphism Id -> M in the category of monads. Lifting eta to T, we get T(eta): T(Id) -> T(M). This gives a monad morphism B -> T(M) called the "base lift". This embeds the effects of the base monad B into T.
5. The natural transformation p: Id -> T (in the category of monads) means that we have components p[M] for every monad M. The component at M is a monad morphism p[M]: M -> T(M). This morphism is called the "foreign lift". It embeds the effects of the "foreign monad" M into T.
6. The natural transformation e: T -> Id (in the category of monads) means that we have components e[M] for every monad M. The component at M is the monad morphism e[M]: T(M) -> M. This runs the effects of the base monad B within T, leaving just the effects of M.
7. Given two monad transformers T1 and T2, we can compute their functor composition T1 ◦ T2, which will be a new functor with exactly the same properties. (Monads don't compose, but monad transformers do, because they are functors in the category of monads.)
8. Since functor composition is associative, we may define a composition of any number of monad transformers, T1 ◦ T2 ◦ T3 etc. This composition is called a "monad stack".
The functions we derived (foreign lift, base lift, base runner, foreign runner, and their analogs in monad stacks) are important for practical use of monad transformers in programming. All their properties and laws follow directly from the assumption that T is a pointed and co-pointed functor in the category of monads.
According to this definition, however, the continuation monad has no transformer: The standard Haskell formula `ContT m r a = (a -> m r) -> m r` does not give a functor in the category of monads, because it is not covariant in the parameter m (the foreign monad). As a consequence, it is impossible to lift `Cont r a -> ContT m r a` for arbitrary monads m. The continuation monad is somewhat pathological also in that there are no monad morphisms Cont r -> Id that don't have side effects, violating the assumptions of purely functional code.
There are other perfectly good monads M without any monad morphisms M -> Id; it is not a problem by itself, as long as there are some other monad morphisms M -> N for suitable "simple enough" monads N. But I'm not sure that the continuation monad has any nontrivial morphisms at all to other monads.
Similarly, it would not be a problem if T were only a pointed functor and not co-pointed, as long as there are natural transformations T -> T' for some suitable "simple enough" functors T'.
Apart from the continuation monad, all known monads have transformers described by this construction.
The ordinary definition of monad transformers (say https://en.wikipedia.org/wiki/Monad_tran
