1. 23
  1. 22

    I find that, having written a lot of Haskell and done a lot of pure math, I am less and less interested in using category theory to describe what I am doing. The category theory seems like the implementation detail, and not the thing I care about. The way I have come to think of things like monads is more like model theory: the monad is a theory, and there are models of it. Those models happen to be isomorphic to categorical constructions.

    This text seems to suffer from what every other category theory text does: where are the theorems? There are lot of definitions here, but definitions are cheap. They alter over time to keep theorems true as new corner cases are found. If someone knows of a category theory text that isn’t a giant collection of definitions, I would love a pointer to it.

    1. 16

      I feel that I am in the same boat. I enjoy Haskell and mathematics. It brings me intense joy to use mathematics to gain new insights into other area, so I leapt at the opportunity. Just like your experience, the first few chapters were purely defining terms, but I kept pushing through. Finally, we started getting into some relations.

      Given f : A → (B, C), ∃ g : A → B and h : A → C

      This was treated as some mind-blowing revelation on par with the Euler identity. Pages and pages of exercises were dedicated to showing the applicability of this formula across domains. There was an especially deep interest showing real world examples. That by asking a barber for a Shave and a Haircut, then telling them to skip the shave, I could get just a haircut.

      The next chapter introduced symmetric monoidal categories with the earth-shattering property that I could take a value (B, C) and get a value (C, B). There was a brief mention that there existed braided categories without this property, and that they had deep connections to quantum mechanics (and my thesis!), but that they were outside the scope of this book. What was in scope was a collection of example problems about how, given waffles and chicken, we can construct a meal of chicken and waffles.

      1. 3

        Stellar comment, category theory (at least at my depth) tends to explain the obvious with the obscure.

      2. 6

        It makes sense to me why a theory of associative maps (to put it glibly) might be useful for someone designing high-level abstractions, since it can help to identify what the important invariants of those abstractions should be. What chafes a little for me in Haskell’s aesthetic embrace of category theory is precisely that a lot of its enthusiasts have the opposite inclination from you and seem to want to refer everything about what they’re doing to category theory. This feels deeply silly to me, because the vast majority of the interesting semantic properties of any given program are carried by concrete implementors of those category-theoretic abstractions. It’s nice that they’re there to provide the interfaces and invariants that allow me to productively compose concretions, but the generality that allows them to do that is also what prevents them from having much to say about what my program actually does. At the risk of seeming uncharitable, I wonder if a lot of the fetishism is down to Haskell being the most obvious place to go for people who belatedly realized that they’d have preferred to pursue pure math than be focused on software.

        If someone knows of a category theory text that isn’t a giant collection of definitions, I would love a pointer to it.

        I think Emily Riehl’s Category Theory in Context is one such text. It’s pretty typical of a math text targeted at mathematicians in its very terse Definition -> Theorem -> Worked Proof -> Exercises format, but the balance between those elements seems similar to anything else in the genre.

        1. 3

          I think that there’s computer science and there’s software engineering and Haskell happens to be a good tool for either. As a result you get a lot of writings out of scope for any given person’s interest.

          1. 2

            Absolutely! It’s just been my experience that a lot of the prominent writing about Haskell from the computer science perspective in particular tends to defer overwhelmingly to category theory in a way that feels reductive to me. It’s certainly possible that I’m just working with a non-representative sample.

            1. 2

              FWIW as someone who’s done a decent amount of higher math, I agree.