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".
 A: I think I've found a nice simple example.
Consider a poset of subsets of a topological space, ordered by inclusion. Set intersection induces a monoidal structure. The closure operator $C$ is a monad that does not admit strength, because $X \cap CY$ is not in general a subset of $C(X \cap Y)$.
Please correct me if anything is wrong here.
A: 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/23104[1]
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 M that is similar to the one described in http://opus.bath.ac.uk/23104/[1]. Namely, (a: a0 → a1) maps to a + (0 → a0), with obvious unit and multiplication.
Now this monad is not strong. Suppose it were, then for a: a0 → a1 and b: b0 → b1, the strength a × M[b] → M[a × b] would involve specifying a morphism from a1 to a0 × b0 + a1 × b1. This morphism cannot be a × b1, because in this case it won't be preserving the tensor product's (which is Cartesian in our case) unit. And what if b0 is empty.
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.
A: 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: Any partially ordered set $(X,\le)$ is a category, and on such a category, the product $\times$ boils down to meets (greatest lower bounds) and monads boil down to 'closure operators'.
For example, the well-known transitive (reflexive) closure is such a closure operator where the underlying category is the category $\mathcal{C}$ of graphs for a fixed vertex-set $V$, i.e. the objects of this category are relations $E \subseteq V\times V$ and $E_1\le E_2$ iff $E_1\subseteq E_2$. Then, it's easy to see that taking the transitive closure $TE=E^*$ of a relation is a closure operator, i.e. a monad on this category $T\colon \mathcal{C}\to\mathcal{C}$.
In order to see that this monad is non-strong in general, consider some $V$ with at least three (distinct) elements, $x,y,z\in V$. Let $E = \{(x,y), (y,z)\}$ and $R=\{(x,z)\}$. Then,
$$
R\times E = R\cap E = \emptyset
$$
and so $T(R\times E) = T\emptyset = \{(v,v) \mid v\in V\}$. But on the other hand,
$$
R\times TE = \{(x,z)\}.
$$
and so $R\times TE \not\le T(R\times E)$, which shows that transitive closure is a non-strong monad.
A: 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.
A: 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".
