Any example of a non-strong monad?

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$.)


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.


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".