This was the third and final lunch in my series about ideal monads. I talked about how to define ideal monads correctly. My talk was based on a discussion with Tarmo Uustalu.
One bad and one good definition
There is a common definition of ideal monads, which is used, for example, in the paper Coproducts of Ideal Monads by Neil Ghani and Tarmo. This definition basically says that a pair as introduced in the previous lunch is an ideal monad, if the derived triple is a monad.
Definition 1 Let be a category with coproducts, and assume that , , , , and . The pair is an ideal monad if and only if is a monad.
Unfortunately, this definition does not give us an equation that constrains the choice of . So we develop another definition, which contains such an equation.
Definition 2 Let be a category with coproducts, and assume that , , , , and . The pair is an ideal monad if and only if
It is easy to show that an ideal monad according to Definition 2 is also an ideal monad according to Definition 1. It is not so obvious whether the converse is also true. Let us check. We assume that is an ideal monad according to Definition 1. This means that the derived triple is a monad, that is, the three monad equations for and hold. We have the following situation:
tells us nothing that we would not already know, since
follows from the coproduct definition.
is more interesting. We have
So the above monad equation is equivalent to
From this, we can derive the desired equation
if is a monomorphism. Unfortunately, this is not the case in general.
Let us finally look at the equation
So the above monad equation is equivalent to
If is a monomorphism, we can derive the desired equation
So if is monic, Definition 1 guarantees that the desired equations for hold, but in general, this guarantee cannot be derived from Definition 1. So I consider Definition 1 inappropriate and regard Definition 2 as a correct definition of ideal monads. Tarmo shares this view.
A third definition
There is yet another definition of ideal monads, which is used by Stefan Milius in his paper On Iteratable Endofunctors. This definition is equivalent to Definition 1, except that it requires to be a subfunctor of .
Definition 3 An ideal monad is a pair that is an ideal monad according to Definition 1 and for which is a subfunctor of .
By definition, is a subfunctor of if and only if for every , is monic. If this is the case, then also the natural transformation is monic. Therefore, an ideal monad according to Definition 3 is also an ideal monad according to Definition 2. The converse is not true, since we cannot expect to be a subfunctor for every that is an ideal monad according to Definition 2.
In as well as in , all injections are monic. So Definition 3 might still seem to be okay. However, Definition 3 does not lead to a good definition of ideal comonads, which are the duals of ideal monads. The duals of injections are projections, and the duals of monomorphisms are epimorphisms. So a definition of ideal comonads that is analog to Definition 3 would require the relevant projections to be epic. In the case of , the epimorphisms are the surjective functions. However, projections are not surjective for .
Mistakes in my MFPS ’12 paper
I have to admit that I used Definition 1 instead of Definition 2 in my paper Towards a Common Categorical Semantics for Linear-Time Temporal Logic and Functional Reactive Programming. And I made a few further mistakes, which are similar:
I defined ideal comonads analogously to Definition 1 instead of Definition 2.
I made an analogous mistake in the definition of -strong ideal monads. An ideal monad should be called strong with respect to an ideal cartesian comonad if and only if there is a natural transformation with
for which certain equations hold. However, I did not require these equations to hold, but required that the monad induced by and a certain natural transformation induced by together form a -strong monad, where is the cartesian comonad induced by .
I made a similar mistake in the definition of temporal categories, which are models of an intuitionistic temporal logic and a flavor of FRP. A temporal category covers an ideal monad , from which we can infer a monad . To ensure that time is linear, I required that if we define and by the equations
then is a product in the Kleisli category of with projections and . This is equivalent to requiring that
is an isomorphism. However, we actually want the existence of an isomorphism
with a definition similar to the above one, from which the above isomorphism property can be deduced.
I intend to present a corrected definition of temporal categories and the constructs they are based upon in a future paper.