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.
A monad is strong if:
- its underlying functor is strong
- the strength commutes with the monad unit `return :: a -> m a`, i.e. `return (x,y) === strength x (return y)`
- the strength commutes with the monad multiplication `join :: m (m a) -> m a`, i.e. `strength x (join mmy) === join (map strength (strength x mmy))`
So a non-strong monad is one for which at least one of these conditions is false.
Non-strong functors are easy to find examples of: take any container type with multiple "slots" (e.g. lists, arrays, n>1-tuples) and put it in a language with linear types. You can't implement `strength` for these types because you can't necessarily copy the `x` value.
Off the top of my head, I can't think of any non-contrived way to violate the latter two conditions without also breaking the monad laws or the requirements of a monoidal product, but presumably they're out there.
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`.
Nobody seems to know where "strength" got its opaque name from. Like, nobody, not even the guy who first published the term.
There is another article on the topic here:
http://comonad.com/reader/2008/deriving-strength-from-lazine...
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.
The only reason they sound special is the silly name and the inane Haskell syntax.
I’m not particularly sold on the Ur-importance of monads in programming, but I don’t get using such a specific implementation to deride the concept. Monads are an algebraic structure, application in programming languages is akin to using sum types to form enumerated data.
After all, a functor is just a way to "bind a continuation to an expression", but this time the function you're binding is of type `a -> b`.
A better way to characterize monads is that they're generic types such that you can compose functions `A -> M[B]` with functions `B -> M[C]`. On first glance, the types don't work for basic function composition. Monads are more-or-less types `M` where a reasonable compose operation exists (for all A,B,C).
Covariant functors in programming are basically producers (I don't know of any counterexamples), so monads are essentially producers where production composes.
A covariant functor takes morphisms from object A to object B in some category to morphisms from A to B in some other category. I don’t know what such a functor would produce except some other morphism (or function as would be the common case for programming).
Also, I think, based on the general impression of snark GP’s comment seemed to contain, I am not unwarranted in reading his use of the term continuation in a literal sense and not to stretch it to say he was describing some (particularly odd) general idea of composition or application of functions.
I've seen people make analogies for covariant functors as containers (typical programming jargon using "functor" to mean the values of the types F[A]), but that's not quite right because of things like Future and IO. But containers are producers (they can produce the values they contain), so that characterization seems to work.
It's possible that what I mean can be turned into a statement like "all functors used in programming are representable", but I'm not sure.
I absolutely agree with the seeming consensus that Categorical constructions can be used to find and then abstract over common patterns in programming languages and implementations. However, it’s conversations like this one that lead me to believe people have confused the implementation of a specific example of some structure with what that structure is. I doubt the co-opting of Categorical vocabulary is that big of a deal, it’s just early and I haven’t had coffee yet.
No, this is much stronger and definitely false. Any variable-size data structure is not going to be representable: e.g. `Maybe`, `List`, `BinaryTree`.
Most data structures are sums of representable functors (i.e. are `Traversable`), but not all. Hash sets () are the classic counterexample: you can't walk them in a consistent order because the internal structure depends on the hashes, and you need to recompute hashes when you transform values.
This is a little too strong, I think. If your category is sufficiently nice (complete closed symmetric monoidal, I think) then every monad arises as a codensity monad `Codensity_F x = \int_{y} (x -> Fy) => Fy` (with `->` and `=>` as the respective homs), which is clearly continuationy in character.
There are so far as I know no programming languages that correspond to genuinely complete categories, but Haskell at least is close enough that this construction still works. The main obstacle there to "`Monad`s are just continuations" isn't mathematical, it's the lack of language support for talking about categories other than `Hask`.
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...
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, because they never talk about monads on arbitrary categories. They only ever talk about monads on Set [or rather, they only ever talk about monads on "Set" where "sets" are taken to be Haskell types and "functions" are taken to be Haskell functions].
But there are more categories in the world than just the 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.
I don't see how this helps anyone.
What is different about a math monad that makes strength no available, and why is that interesting?
How would you create a non-strong monad in Haskell, and why might you want to, or is it impossible?
Seems to lean to much on a sort of false connection between Haskell and math, where two similar but different things have the same name.