«A neighborhood of infinity» was one of the blogs which inspired me as a young person, and definitely put me on the path to do research. I would spend hours reading the posts, testing the code and trying to use the stuff in my own programs. The kind of insights it showed off are still what I spend my time searching for.
So, strength is the ability to write a monad-related function you can define if you need to, like any other function you might write that had a monad argument. But you can't not in math monads, for reasons not explained.
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.
As a wild guess, this same construct might not always work with linear types—if we had to use x exactly once, we wouldn't always be able to write `return (x, y)`. I haven't really used them, but linear types are supported in Haskell, and you can generalize the Monad class to be able to handle them. This would conceptually correspond to x being some sort of limited resource that we can't copy arbitrarily, which is more than a purely mathematical curio.
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.
> How would you create a non-strong monad in Haskell, and why might you want to, or is it impossible?
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`.
Given a monad M on a category C, it is among other things a functor from C to C, which means that we have functions from Hom(c, d) to Hom(M(c), M(d)) for each pair of objects c and d in C. [Here, by Hom(x, y), I mean the set of morphisms from x to y in C.]
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.
I agree that it would be interesting to learn what non-strong monads look like. But the blog post does (implicitly) answer some of your questions:
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 agree that it would be interesting to learn what non-strong monads look like.
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 don’t think ‘strength’ requires a Cartesian product. I was under the expression that any tensor product was sufficient, some of which lack Cartesian structure.
You need it to be symmetric if you want strength as such instead of left-strength and right-strength, but otherwise yes, it makes sense to talk about strength relative to any monoidal product.
I find this to be an odd take. Monads, even when restricted to programming language usage, do not fundamentally have anything to do with continuations. There is a Continuation Monad in Haskell, but that is just one implementation of one example of a monad.
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.
I think the grandparent means it offers a way to bind a function `a -> m b` to an expression of type `m a`, to make an expression of type `m b`, but they left out the important part, which is the types!
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.
Generally, from what I've seen, for all of the practical programming examples, an `F[A]` (for F covariant) can be considered to be a type that produces zero-or-more `A`s. Thought of properly, F maps types of values to some type of producer of values, and morphisms to postcomposition of the underlying function. F contravariant maps types to some type of consumer for that type and morphisms to precomposition.
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 don’t know that I agree with the producer of values analogy, but this is really the crux of my problem. I have trouble defining or describing abstract algebraic structures as anything other than what they are and the continual usage in programming discussions just perplexes me.
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.
> 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.
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.
> Monads, even when restricted to programming language usage, do not fundamentally have anything to do with continuations.
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`.
I feel like an idiot when reading _about_ Haskell.
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.
I think the article is an attempt to make your idea more precise. What if monad 3 could use the result of monad 1, not just monad 2? Then you couldn't write that computation using your pipeline metaphor.
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).
If my example of pipeline is a limited metaphor, couldn't it be expanded?
I love this subject but it's traditionally over-complex, so I appreciate the correction and explaination.
How could "strength" be applied generically to programs outside of Haskell? Could the concept of pipelines be extended? Is programming too 1 dimensional? There must be ways to do this.
I think the user-friendly way to make programming less one-dimensional is what we usually do, outside of shell pipelines; give names to intermediate values:
do x <- computation1
y <- computation2 x
computation3 x y
...turning a one-dimensional sequence of operations into a data-flow graph represented textually.
But, and perhaps this is an academic question, what if you're stuck in a context where you can only create computations by composing functions in a sequence, without giving names to intermediate results? Shell pipelines, for example, without using temporary files or other tricks.
Then, using this idea of strong and weak monads, and if you were used to thinking of computations as elements of a monad type, you might realize that all you need to add is a "strength" operator, and you would regain the full expressivity of data flow graphs. This operator would take a computation and bundle it with value, producing a new computation that does the same computation, but bundles its result with the extra value you supplied. So you've given every computation a side-channel that ferries any data you like through it, unchanged. Computations further down the chain can access both values.
I lack the imagination to see how this example works out in shell, because there we don't have the luxury of multiple input and output values (just single pipes of data). But it's nice to know that just the strength operation is enough to express arbitrary computation graphs, with names being given to inputs and outputs.
So how do you generalize this idea to programs and functions? My framing is "incorrect" I think but it feels far easier to reason about.
Couldn't this same idea be applied generically to all computer programs? Could its valuable situational properties ever be done in a way that is language neutral with arbitrary program monads?
Caveat emptor, though. A lot of that page is erroneous.
A few years ago I fixed up the definition for F#, which is perhaps the closest thing to a language for ordinary Joes in which true monadic style can be defined/achieved.
Monads are a concept in types and a specific theory but if you throw the rigid definition away can't they be done anywhere? For example, if I have three RaspberryPi's, isn't there a way I could compose them as monads?
That is what I mean - it isn't a fair thing for me to say - but I feel like they would be so much more tangible if we could think about them as literal Things like this. Which is why my original example was composition of Programs instead of composition in a specific Programming Language.
Each Raspberry Pi could perform a function that was notionally passed to the monadic bind operator, but really a monad is the rules under which the Raspberry Pis would be connected.
From Wadler's paper "The Essence of Functional Programming":
"2.1 What is a monad?
For our purposes, a monad is a triple
(M,unitM,bindM) consisting of a type constructor M and a pair of polymorphic functions.
unitM :: a-> M a
bindM :: M a-> (a-> M b)-> M b
These functions must satisfy three laws, which are discussed in Section 2.10."
So the monad is a functor plus a few operations and laws. It is an algebraic structure, not a type of object or function.
It's important to me because if the pattern was actually useful then we should be able to use it anywhere and talk about it. It seems obvious that the pipe "workflow" pattern as they call it isn't the end-all for program composition - so how can we fix and expand it? It seems fixable.
Another context question: How would you define a monad in Microsoft Excel? For context, that is my favorite programming language. It seems perfectly capable at doing strong monad composition better than a Linux shell.
I just want monads be real and tangible! Examples in reality instead of Math.
What on earth makes you convinced that a monad can be implemented in Excel? You don't understand what a monad is, so you can't know whether Excel is "perfectly capable" of it or not.
Read a bunch of monad tutorials, learn Haskell, hey, even develop some "mathematical maturity" if you can get over your disdain for math. That is the way to make progress.
It's not helpful to want monads to be tangible objects. It doesn't matter how much you want it. The world doesn't work like that.
> What on earth makes you convinced that a monad can be implemented in Excel
True monads can't even be implemented in Haskell. But if we're being practical, you can totally implement monad-like things in Excel. It's almost impossible not to implement monad-like things when building anything non-trivial.
I don't think making this claim is helpful. Monads aren't found everywhere in code. Solving a problem which could be solved by monads doesn't automatically lead to code that works in a monad-like way, not in any meaningful sense.
I completely disagree... The distinction is simply that they're usually ad-hoc and not formalized, mainly because the author didn't know what they were writing and was reinventing the wheel.
What I mean is, they can easily be used as monads - and in fact every Excel user might do so without even knowing what a monad is. Like 41 is used in commutative expressions all the time by people who don't even know what communitivity or associativity mathematically is and that is a good thing! It means its useful and intuitive!
That's why I wish we could throw out the Math, if we can't even use Monads without mathematically knowing they are Monads then no one is ever going to be using them. There must be a way that these patterns can become so intuitive, like Pipes (weak) and Excel (strong) that they speak for themselves and become tangible.
> if we can't even use Monads without mathematically knowing they are Monads then no one is ever going to be using them.
You don't need to know what a monad is to use one. Everyone who has ever written a computer program has used one. Knowing that you're using a monad, and what that means about your program structure, is the entire value proposition here - actually applying particular monad operations is utterly trivial. "Monad" belongs in the same category as "data structure", not "tree".
> It is an algebraic structure, not a type of object or function.
Also therefore it is not that "monads can be composed with monads". Only Functions can, bhe composed. Especially functions which are the unitM() or bindM of some monad.
You're right, there's no right-associativity actually involved, but the article probably used the term because the code kinda looks right-associative if you squint. The point is that the rightmost >>= is evaluated first, which lets the y lambda capture x. The article put the parens like this:
which to a non-Haskeller like me does make it look more right-associative than it actually is – and as the article showed, you can actually make it "left-associative" in the obvious way, which would indeed compile fine and be equivalent to the "right-associative" way if the y lambda didn't refer to x.
