1. 28

  2. 6

    The author’s explanations are incomplete and likely to confuse.

    The “imprecise definition” at the top cannot tell between a functor and a monad; it isn’t rich enough. For example, this Haskell type has a Functor instance but no Monad:

    data Const b a = C b deriving (Functor)

    Const clearly is a type wrapper with no direct way to get at values of type a, satisfying the imprecise definition.

    The container examples ignore a massive caveat that manifests in every monad-bearing language. Because of the order of evaluation, along with the fact that monoidal structures stack and interact with each other (the Eckmann-Hilton argument, sometimes known as the slogan “monoids in categories of monoids are commutative”), the typical container forms a cromulent functor, but not necessarily a monad. In Haskell, the classic example is ListT and how it can fail to be a monad transformer.

    Indeed, many containers have technical nits in their APIs which prevent monadic behavior. In Haskell, the classic example is the family of data structures in Data.Set; these sets cannot provide Monads due to weaknesses in Haskell’s type system.

    The author briefly touches on continuations, but misses the important connections. A continuation type doesn’t just provide a monad, but a family of monads, via the “mother of all monads” construction. For each continuation type, there is an interesting collection of behaviors, and all of the other different monads can be implemented in terms of the “mother” continuation monad. Constructing a list monad, or another container-shaped monad, on top of continuations is very instructive; the amount of non-determinism in the list monad varies with the number of times and places that the continuations can be called.

    I’m not sure what’s scary about mathematical presentations of category-theoretic concepts. If the author grokked categories of endofunctors, then they would more clearly understand how monads aren’t containers. Alongside their reading recommendations, I’d recommend Seven Sketches.

    As a closing note, why are programmers afraid of maths?

    1. 15

      As a closing note, why are programmers afraid of maths?

      Maybe because they’re told they need to “grok categories of endofunctors” and then linked to a 350 page book on an advanced math topic.

      Look, I love math. I made my career teaching temporal logic to programmers, and it’s awesome. You know what the first major stumbling block for programmers is, though? false => true. That breaks people. Telling them they’re wrong about monads and throwing them in the deep end is a terrible way to get people to like using math.

      1. 4

        I personally feel that the word “implies” is too strong and may have been created by a lack of words for an inability to disprove. “Does not disprove” is probably closer to how most think about it. A false statement can’t be used as evidence against any statement. To actually meaningfully prove something your claims must survive evidence against, so it makes sense to have a term that represents surviving attacks however weak. I’m sure this also captures a little bit of Boole’s biases around what something failing to be disproved means, after all he was intensely religious. Still the operation is pretty useful, and will likely continue to be.

        1. 2

          Sure. I don’t care whether people like using math; math is still an essential part of existence, and in particular of writing code. One does not have to enjoy a task to not fear it. My coworkers react to matrix multiplication like they would to snakes or spiders, and I think that that is ridiculous.

          I will readily admit that I am broken, and further that I believe that it’s not possible to think like a computer without breaking oneself. But the reward of the study of maths is that there is a deep reason why false -> true and false => true show up. If one has already sacrificed their sanity in order to understand how to write code, one might as well take in the beauty of the works of mathematicians, since it is only with this other-than-sane viewpoint that the beauty is visible.

          1. 4

            I mean breaks them as in “it’s really, really hard to get them to understand it”. I lie awake at nights trying to find better ways to explain it. And most programmers don’t need to know that to write code. People who want to write formal specifications of code need to know it. Not everybody needs to do that either.

            But the reward of the study of maths is that there is a deep reason why false -> true and false => true show up [link to (-1)-categories]

            That is a terrible explanation. Here’s a much better one (which still, admittedly, isn’t that great):

            “If x > 5 then x > 0, right? So x > 5 => x > 0. But now let’s pick x = 3. [now] 3 < 5 and 3 > 0, so we have false => true. So you see, intuitively you’re already comfortable with F => T, it’s just that it looks weird when we formalize it.”

            Do you see why that’s a better explanation?

            (edit, added a spacer)

            1. 3

              One reason this is a better explanation is that you sort-of described what the symbol => means though context. I still don’t know specifically what it means though in this context, though. Is this a Haskell symbol or a temporal logic symbol?

              You lost me on “x = 3. 3 < 5 and 3 > 0”, because it’s not immediately obvious that the . denotes the end of the sentence (I had to read it multiple times before I realized you had written x = 3. 3 < 5 and not x = 3.3 < 5. It’s also confusing that two more symbols F and T are introduced at the end, this time with no context clues to infer their meaning.

              1. 1

                Oh to clarify this would be in the broader context of teaching someone propositional logic, so they’d know => means implication. P => Q means that if P is true, then Q is also true. As @voronoipotato said, it’s technically closer to “is at least as strong as”. At this point I’d also have introduced the shorthand for T and F.

                1. 1

                  Thanks for the clarification. I initially tried reading it as “implies”, then as a Haskell fat arrow, and neither made sense to me. Reading it as “is at least as strong as” makes a lot more sense.

                2. 1

                  FWIW => is a pretty standard asciification of ⇒, and -> of →. Both of these symbols are used to mean material implication in mathematical writing. If you see them both in the same place, you’re probably looking at formal logic of some kind, and there’s likely an important technical difference between the two. I won’t get into Haskell or TLA+ syntax here, or even constructive vs classical logic, but yeah there are more subtle distinctions to be confused by here.

                  When I have to explain ->, I just say P -> Q means (not P) or Q. Maybe write down a truth table. In my experience, even programmers can usually figure that out.

          2. 5

            As a closing note, why are programmers afraid of maths?

            My university mathematics ended after the third semester of calculus – a requirement that only existed because, where I went to school, computer science was part of the engineering department. Most working programmers with CS degrees got them from places that didn’t require them to go beyond one semester of calculus. A lot of working programmers don’t have degrees at all.

            Haskell evangelists make the claim that monads provide specific utility to everyday development tasks. Devs who want to determine whether or not this claim is true. Even if they knew it to be undoubtedly true, they would not generally be willing to go back to school & attend four semesters of mathematics courses in order to get incremental gains in reliability or productivity. (Working programmers have a tendency to ignore or avoid techniques that provide much more substantial gains in reliability & productivity because of much smaller initial learning curves than group & category theory.)

            One way to thread this needle is to stop claiming that the benefits of monads are accessible to developers who do not also have a graduate degree in mathematics. (This would probably kill some of the momentum behind the adoption of functional programming techniques – which, though hype-driven, is long overdue & is liable, if it continues, to substantially improve the general quality of software & make software that takes advantage of multiple cores a lot more common.) The other is to write explanations that, while wrong, are less wrong than what your average code monkey already believes about monads while being accessible to said code monkey. (This annoys everybody who knows more than the author, but provides some utility, since readers gain the confidence to actually use monads without fully understanding them.)

            1. 1

              (This annoys everybody who knows more than the author, but provides some utility, since readers gain the confidence to actually use monads without fully understanding them.)

              I wanna add that this is not even necessarily the case. Leaving information out and skewing details are very well known teaching methods. Take continuous functions as an example. In school they’re “functions that you can draw without taking the pen off the paper”. For a mathematician a more fitting explanation is “small changes in inputs cause relatively small changes in outputs”, since even continuous functions can have holes.

              1. 2

                Yup, ‘lies for children’ are almost unavoidable. It’s still annoying to read something when you’re not part of the target audience, though, which seems to be the complaint here – somebody with a strong background in category theory being irritated at the reminder that introductory materials exist.

            2. 5

              Programmers are afraid of math because they never learned it, obviously. We often only have one or two classes on proofs as a prerequisite for programming, and they are introduced near the end of our education. Mathematics without proofs is like painting by number. It’s no wonder most people feel alienated by it, they are asked to trust the conclusions of others without meaningful evidence. Most of these claims are often not readily available to the intuition. People who simply do as they are told and follow instructions perform quite well at “mathematics” as it is taught. The rest, those who are capable of questioning, would perform quite well at actually proving things are weeded out long before they would ever have any opportunity.

              1. 1

                I don’t think most programmers end up studying proofs in university at all. I only did because I took math electives, & most CS degree programmes are much less mathematical than the one I had.

              2. 4

                Writing clearly and concisely in a manner appropriate to the audience is a skill. The author managed this and I’m grateful.

                It would be good to see corrections in the same language (a mix of plain English and commonly-understood programming language).

                Explaining maths in maths doesn’t work very well when the audience aren’t necessarily mathematicians.

                It’s the same problem as programmers explaining programming concepts to non-programmers. Using plain English for this is a hard skill - harder than learning to program.

                1. 2

                  There is no such thing as plain English. (If you still disagree, I respectfully invite you to formally define it.)

                  I do not want the author to correct their monad tutorial; I would like the author to not write monad tutorials. Monad tutorials are deeply harmful. They do violence not only to the concept of monads, but to the audience’s ability to internalize concepts with their own personalized schemata and experiences.

                  By analogy, I’d like to consider another concept which appears in many programming languages and which many people develop an intuition for: Numbers. Imagine if programmers were required to build up a working concept of what numbers are and how they work. Do you suppose that people would write number tutorials? Would they explain how numbers work by analogy? It’s easy enough for me to imagine that the author would write some copy along those lines:

                  Imprecise definition: A number is a type that counts an object of another type. There is no direct way to get each of the ‘inside’ objects. Instead you ask arithmetic to act on the number for you. Numeric classes are a lot like classes implementing the composite pattern, but numbers are capable of returning something composed with another number.

                  Would you really excuse them if they later tried to explain, formally:

                  The concept of numbers comes from arithmetic.

                  A number tutorial would be a folly precisely because we hope that folks will build a robust and flexible concept of numbers which can stretch beyond the integers or other familiar domains. Similarly, monad-tutorial-oriented teaching leaves students without a concept of what monads generally are, once we leave the computer and explore the wider world. How will folks learn about the monoidal behavior of monads without understanding that a monad is a certain sort of monoid? Category theory is the most generic formalism yet for discussing reality at large.

                  Every programmer is a mathematician, as a matter of necessary practice. I studied music, not maths, but I nonetheless am not excused from mathematical thinking when writing code.

                  1. 2

                    You’ve never seen a tutorial about how to start with the everyday concept of counting numbers, and then build up more and more complicated notions of “number” from these until you reach octonions? (Or go down and define natural numbers in terms of ZFC?)

                    1. 1

                      I find it telling that you did not link to any sources. I can produce the evidence, but of course it will favor my position, as I am biased. We’ll look at constructing the reals from the naturals, the octonions from the reals, and natural numbers in ZFC.

                      First, construction of real numbers. Let’s compare some sources. Wikipedia starts from the perspective that there are many different constructions, and that they all involve rational numbers. Wikibooks emphasizes the need to ground the reals in axiomatic foundations, and not to assume that they exist. In both cases, some prior knowledge is assumed; the construction isn’t from-scratch on a single page.

                      Second, construction of octonions. Wikipedia mentions each step of the construction, including the familiar example of complex numbers. Baez is, to me, an extremely casual and friendly approach to the topic, but note that they do not drop formalities:

                      It would be nice to have a construction of the normed division algebras ℝ, ℂ, ℍ, 𝕆 that explained why each one fits neatly inside the next. It would be nice if this construction made it clear why ℍ is noncommutative and 𝕆 is nonassociative. It would be even better if this construction gave an infinite sequence of algebras, doubling in dimension each time, with the normed division algebras as the first four. In fact, there is such a construction: it’s called the Cayley-Dickson construction.

                      And, finally, natural numbers in ZFC. Wikipedia has answers and examples. In particular, Wikipedia contains an important note as its first line:

                      Several ways have been proposed to construct the natural numbers using set theory.

              3. 1

                Why won’t the functional programming cabal just admit that monads are like burritos?!

                Jokes aside, I think you need to first write some stateful programs in Haskell to appreciate how The Monad takes the pain away. By just studying examples it can be hard to see what the fuss is all about.

                1. 1

                  Thanks! This saves me another explanation to juniors about 3 to 4 times per year.