5 ms·

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.

• MaxRegret 3y ago
  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.
  • throwaway17_17 3y ago
    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.
    • consilient 3y ago
      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.
  • consilient 3y ago
    > 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.
• bPspGiJT8Y 3y ago
  > 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`.
  • kfixjviv 3y ago
    Haskell's sequence is not the same as strength. Strength specifically involves pairs. 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-laziness/ http://comonad.com/reader/2008/deriving-strength-from-lazine...
• tikhonj 3y ago
  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.
• mkoubaa 3y ago
  "I don't see how this helps anyone" is my gut response to anything related to the m-word
  • mgaunard 3y ago
    Monads are just a way to bind a continuation to an expression. The only reason they sound special is the silly name and the inane Haskell syntax.
    • throwaway17_17 3y ago
      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.
      • ndriscoll 3y ago
        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.
        • throwaway17_17 3y ago
          Can you explain what you mean by producers? 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.
• hackandthink 3y ago
  >What is different about a math monad that makes strength no available, and why is that interesting? 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-strong-monads/ https://mroman42.github.io/notes/Pieces/Do-notation-for-stro...
  • gowld 3y ago
    I can't read that handwriting.
    • phibz 3y ago
      Read yes, understand... that's a different story.
  • trust_bt_verify 3y ago
    Nice handwriting and explanation. Thanks!
• Chinjut 3y ago
  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.