What does it mean for a monad to be strong?

Ctrl+F “endofunctors”

In mathematics more broadly, the fact that you don't always have the equivalent of the `strength` function is useful because it lets us work with different kinds of products than just tuples. This can even be useful for practical work: we might want to model something like hardware or quantum computations which behave differently than "normal" programs. Requiring all monads in that context to support `strength` would really restrict the sort of things you could useful model as monads.

Let's turn it around. Why is strength for Haskell Monads interesting?

Answer: it enables a nicer do notation, you can use intermediate values:

https://mroman42.github.io/notes/Pieces/Do-notation-for-stro...

I think the article implies it clear enough that it's impossible. Even if your monad has nonsensical (but lawful) semantics like `Proxy t` it's still possible to use it with `strength`. BTW the `strength` function is called `sequence`.

If C is a so-called "closed category", not only is there an actual set Hom(x, y) of morphisms from x to y, but also, there is internal to C a corresponding object x → y.

We say a monad is "strong" if there are morphisms from x → y to M(x) → M(y) [note that these are morphisms in C between objects of C] which suitably correspond to the aforementioned functions from Hom(x, y) to Hom(M(x), M(y)) [note that these are morphisms in Set between objects of Set].

This is the distinction between having an operator external to your programming language that rewrites functions from x to y into functions from M(x) to M(y) (plain monad) vs furthermore having this operator itself represented internal to your programming language by a function from x → y to M(x) → M(y) (strong monad).

(This notion of strength really doesn't have to do with monads specifically, and applies more generally to functors. It's the same as what people call being an "enriched functor".)

The notion of a strong monad on a closed category C goes beyond just the plain notion of a monad on C, because it asks for some structure to exist internal to C which otherwise only has to exist in Set. But if C itself is Set, this is automatic. This is why monads on Set are automatically strong.

This is all muddied in the way people in Haskell world talk about monads and functors, because they never talk about monads on arbitrary categories, or functors between arbitrary categories. They never talk about categories at all because they only ever have one category in mind. They only ever talk about monads on Set, or functors from Set to Set [or rather, "Set" where "sets" are taken to be Haskell types and "functions" are taken to be Haskell functions. But this amounts to about the same thing, if you only ever work internal to "Set"]. This can make for some confusion in translating between how Haskell people use category-theoretic jargon and how category theorists use it.

But there are more categories in the world beyond just the ambient category Set. For a simple example of a closed category and a non-strong monad on it, consider the four-element Boolean algebra with 0 < p, q < 1. We can construe this as a category, where there is a (unique) morphism from any value to any equal or larger value. This category is in fact cartesian closed; we have Boolean negation such that p and q are each other's negations, and more generally, the interpretation of x → y becomes the material implication operation such that x → y = (NOT x) OR y.

If we define on this the operation M which sends 0 to itself but sends all other values to 1, we find that this M is indeed functorial: Whenever x ≤ y, we have M(x) ≤ M(y). And this M is furthermore a monad: It's easy to verify that x ≤ M(x) and M(M(x)) ≤ M(x) for all x. [All the other equations that go into being a monad are trivial in this partial order context where all parallel morphisms are equal]

But this M is NOT a strong monad! Even though it's true from our external perspective that x ≤ y entails M(x) ≤ M(y), that is not visible internal to this category, so to speak, in that we do not in general have that (x → y) ≤ M(x) → M(y). For example, p → 0 = q, but M(p) → M(0) = 0, and we do not have q ≤ 0.

Another example along the same lines is where we take our category C to be Set^2, whose objects are pairs of sets and whose morphisms are pairs of functions, all composing component-wise, and equip it with a monad which sends (empty set, empty set) to itself and sends everything else to (one element set, one element set).

There are also less trivial, more complicated examples, but this should perhaps get the idea across of what a non-strong monad. Of course, it requires thinking about categories in general to begin with.

It says that all monads in the Set category are strong. That would include Haskell monads, at least those expressed in the usual way as type constructors, to the extent that Haskell types model sets.

And you can see that the "strength" operation relies on the existence of tuples behaving like Cartesian products of sets. Such objects might not exist in other categories.

I have no problem reading and writing Haskell code itself. But for some reason most of the articles about it are successful efforts in deliberate complication of otherwise simpler affairs.

The article is saying that by judicious use of a "strength" function, you can in fact write any monadic computation as such a pipeline (or composition of monadic functions).

    a -> b -> c
     \_______^