# Any example of a non-strong monad?

Looking for an example of a monad that is not strong.

The reason being, a strong monad (wrt cartesian product) is an "applicative functor" (in functional programming); an example of a non-strong monad would be useful to see what's breaking in its "applicativity".

-
You will have to look outside the category of sets. –  Andrej Bauer Jan 11 '12 at 11:40
In functional programming, what this amounts to is that you will have to look outside the monads/functors for which one has a function map : (a -> b) -> (m a -> m b). There will in fact be a way (external to the programming language) to take any function of type a -> b and turn it into the corresponding function of type m a -> m b, but there will not be any higher-order function (internal to the programming language) which does this for you. [This is the meaning, in this context, of Finn's statement that strong monads are those which respect the internal hom's enrichment] –  Sridhar Ramesh Jan 11 '12 at 22:26
More to the point, perhaps, depending on how you think about monads in functional programming: for a non-strong monad, one does not have a function bind : m a -> (a -> m b) -> m b in the programming language. Rather, there will be a method of taking any function of type a -> m b and turning it into a function of type m a -> m b, but this method is not carried out by any higher-order function. –  Sridhar Ramesh Jan 11 '12 at 22:29
Something to bear in mind is that strength is not a property of a monad: it's extra structure on a monad. The same monad can admit no strengths, one strength, or many strengths. (At least, I believe this to be the case. I don't know an example.) So "monad that is not strong" is a phrase comparable to "set that is not a group". But maybe you know that. –  Tom Leinster Jan 13 '12 at 17:16

Here is a class of examples different to Tom's: if your underlying monoidal category C is closed, then a strong monad on C is the same as a C-enriched monad, i.e. one that respects the enrichment of C given by its internal hom (this is why every monad on Set is strong, as Andrej points out). So one example would be the monad on Cat (considered as a Set-category) whose algebras are cartesian closed categories -- it is known that this is not a Cat-monad (although it does extend to Cat as a groupoid-enriched category). I would imagine that the same is true for the monad for monoidal closed categories, or in general for categories with any one sort of mixed-variance structure.

-
Here is a very simple example of the same kind suggested by Finn and due to John Power: it is a monad on Cat which cannot be extended to a 2-monad and therefore cannot have a strength. It is the monad T on Cat whose algebras are categories C equipped with a endofunction on the set of objects ob(C) of C. It has value $TC= C + (N \times ob(C))$ where $N$ is the discrete category with set of objects the natural numbers. For the details of why it cannot be extended, see Example 3.1 of Power's "Unicity of enrichment over Cat or Gpd" freely available at opus.bath.ac.uk/23104 –  John Bourke Jan 23 '12 at 15:05

Here's one. Let $\mathbb{D}$ be the monoidal category of finite ordinals. Thus, the objects are the natural numbers (including 0), a map $m \to n$ is an order-preserving function $\{1, \ldots, m\} \to \{1, \ldots, n\}$, and the monoidal structure is addition. The object $1$ is a monoid in $\mathbb{D}$, in a unique way. This makes $T = 1 + (-)$ into a monad on $\mathbb{D}$.

I claim that $T$ admits no strength. A strength on $T$ would consist of a map $$t_{m, n}\colon m + 1 + n \to 1 + m + n$$ for each $m$ and $n$, satisfying some axioms. Readers might wish to stop reading here, because perhaps it's clear that no sensible such $t$ can exist (bearing in mind that maps have to be order-preserving). But ploughing on:

$t_{0, 0}$ must be the identity map on $1$, and the naturality square for the unique maps $0 \to m$ and $0 \to n$ then tells us that $t_{m, n}\colon m + 1 + n \to 1 + m + n$ must send the copy of $1$ in the domain to the copy of $1$ in the codomain.

On the other hand, the unit axiom (i.e. the second triangle on the Wikipedia page) tells us that $t_{m, n}\colon m + 1 + n \to 1 + m + n$ must send each element of $m$ in the domain to the corresponding element of $m$ in the codomain. So, for instance, $t_{1, 0}\colon 1 + 1 \to 1 + 1$ is the non-identity bijection. This is not order-preserving — contradiction.

(Why did I think of this example? Because I wanted to find the most generic possible example of a category equipped with a monad. Well, the initial category equipped with a monad is the empty category, which clearly isn't going to answer your question, so I wanted the free category equipped with a monad and an object. This is exactly $\mathbb{D}$, equipped with the monad $T$ and the object $0$.)

-
A) How can the initial monoidal category equipped with a monad be empty? Surely, it must have an identity object for the monoidal structure. B) This is nice, as a free example with monoidal structure, but the question-asker seemed to want specifically cartesian product structure. –  Sridhar Ramesh Jan 11 '12 at 22:19
Oh, whoops, nevermind A); apparently, it was corrected 5 minutes before I said it. –  Sridhar Ramesh Jan 11 '12 at 22:58
Yeah, sorry about the mistake; wasn't thinking straight. As for the cartesian structure, maybe Finn's answer will be more satisfying on that front. –  Tom Leinster Jan 11 '12 at 23:45

This answer is largely a rendition of Sridhar's comment into lambda calculus. A strong monad $T$ has the following introduction and elimination rules in the lambda calculus.

$$\frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : T(A)}$$ $$\frac{\Gamma \vdash e : T(A) \qquad \Gamma, x : A \vdash e' : T(B)} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : T(B)}$$

You may recognize these rules as typing a variant of the do-notation in Haskell.

Strength is needed to interpret the elimination rule, since the context $\Gamma$ is available in both premises of the elimination rule. Taking $\sigma : \Gamma \times T(A) \to T(\Gamma \times A)$, we can calculate:

$$\begin{array}{lcl} e & : & \Gamma \to T(A) \\\ e' & : & \Gamma \times A \to T(B) \\\ T(e') & : & T(\Gamma \times A) \to T^2(B) \\\ T(e'); \mu & : & T(\Gamma \times A) \to T(B) \\\ \langle id; e\rangle & : & \Gamma \to \Gamma \times T(A)\\\ \langle id; e\rangle; \sigma & : & \Gamma \to T(\Gamma \times A)\\\ \langle id; e\rangle; \sigma; T(e'); \mu & : & \Gamma \to T(B)\\\ \end{array}$$

Without the strength $\sigma$, we could not use the context $\Gamma$ in $e'$. That is, we would get introduction and elimination forms:

$$\frac{\Gamma \vdash e : A} {\Gamma \vdash \mathrm{val}(e) : \Diamond A}$$ $$\frac{\Gamma \vdash e : \Diamond A \qquad x : A \vdash e' : \Diamond B} {\Gamma \vdash \mathrm{let\;val}(x) = e \;\mathrm{in}\; e' : \Diamond B}$$

I changed the notation from $T$ to $\Diamond$, since this is actually the possibility modality of S4 modal logic! These modalities arise in applications like functional languages for distributed programming --- e.g., see Murphy et al's 2004 LICS paper "A Symmetric Modal Lambda Calculus for Distributed Computing".

-
This is a very cool interpretation, thanks a lot! Although it does not exactly answer the question, but it gives a great insight. Actually, it would be great to find a non-strong monad in a CCC. But well, this should be a separate question. –  Vlad Patryshev Jan 13 '12 at 7:20
This interpretation will produce a non-strong monad on a CCC, if you add in all the rest of the rules of the simply-typed lambda calculus with pairs. Indeed, this produces the free monad on a CCC. –  Sridhar Ramesh Jan 13 '12 at 7:29

This should really be a comment to the original question, and/or to Finn Lawler's answer, complementing John Bourke's comment. I apologise for posting as an answer, but I don't yet have comment privileges here.

As Tom believes above, there is a monad with two different enrichments. See Example 4.1 in John Power's "Unicity of enrichment over Cat or Gpd" which John Bourke mentions above.

-

I believe I found a simple sample for a ccc, based on the answers from Tom Leinster, Finn Lawler and John Bourke, and http://opus.bath.ac.uk/231041

I also used the fact I found in Moggi's "Computational lambda-calculus and monads" - that a category should be well-pointed.

Take category 2 (two objects, three arrows), and a topos Set2. This topos is obviously not well-pointed, so we can proceed. Take a monad similar to the one described in http://opus.bath.ac.uk/23104/1. Namely, (a: a0 → a1) maps to a + (0 → a1), with obvious unit and multiplication. Now this monad is obviously not strong.

I believe this kind of topos would be a good testing area for the favorite Haskell constructs. Some of them won't hold, I believe.

Now I wonder... can we prove that if all monads over a topos are strong, then the topos is Boolean? Will post it in another question.

-