124

52

almostdeadguy

hackandthink

Andrej Bauer wrote a popular post in 2016 (Hask is not a category):

https://math.andrej.com/2016/08/06/hask-is-not-a-category/

Mathematicians are still thinking about this stuff.

A recent post by Mike Shulman, asking about Agda (Haskell for mathematicians):

https://proofassistants.stackexchange.com/questions/1887/cat...

agentultra

And you definitely don't need to learn category theory or know anything about it to start writing programs in Haskell or to maintain and build large Haskell applications.

A lot of category theory is fun to learn and knowing it will help you in many ways but it is not a necessary requirement. I mention this because a lot of people seem to think it is.

Definitely a nice article for the math-oriented/curious/etc! It's neat seeing what Haskell *isn't* in order to understand better what *it is*.

justinhj

Enjoyed the article as a functional programmer and category theory enthusiast. Haskell does not have to be a strict encoding of Category for it to be useful. We are grown ups and can understand that not everything is perfect and we can overlook some warts in order to benefit from a beautiful set of rules that help us think about composition as a first class citizen in our work.

The first thing mathematicians tell you when talking about categories of, say, sets, we have to do some hand waving to avoid Russel's Paradox. In other words even mathematicians have caveats when talking about different aspects of category theory.

In the case of the Functor, we use fmap and not a "function that lifts functions" because it is much more ergonomic. Yet, it is just as "correct" since it is isomorphic to lifting a function and applying it.

With monads we use bind and flatmap although the most obvious categorical implementation would be a simple compose function. That maps more directly to the "category of endofunctors", but again it is isomorphic to the same code that uses flatMap/bind, and the same laws hold.

A lot of utility has been gotten from analogies with category theory and as long as we hold our noses we can ignore the occasional whiff of in-authenticity.

I don't believe that you need to learn category theory to take advantage of the concepts we have borrowed, but it does make everything become more coherent to dig into it a little. It's also a lot of fun if you like that sort of thing.

xwowsersx

> I recommend Learn You A Haskell.

LYAH is a fun read, but for someone trying to learn the language seriously — by this I just mean more than a casual tour to get an idea of what the language looks and feels like — there are, thankfully, some much better resources and books available these days. No shade to LYAH intended whatsoever, but it's just not what I'd recommend for some undertaking really learning the language. https://haskellbook.com/ is a solid option IMO.

runevault

I'm confused by his argument that Haskell functors are only endofunctors because everything is Hask.

I thought that even if everything is part of one category, if the input is a different category that is a subset of the one category and transformed to another category, even if a subset of the same category, it could still be a regular functor instead of an endofunctor.

For example, lets say you had a function f(x) that takes unsigned ints and returns the signed int inverse (so f(1) = -1). -1 is not part of the unsigned category since it is below the Initial value of an unsigned number (0). I'm a total newbie to category theory so I'm not sure if he's wrong or I'm missing a key detail here.

dan-robertson

Haskell is a pretty fun language to learn and if you’re interested in trying to translate concepts from category theory into programming, it’s probably a good language to use.

Haskell is not category theory in the same sense that arithmetic is not group theory: there’s only really one category. Well sort-of because type constructors let you work in different subcategories.

Category theory is about *different* categories and the nature of the relationships between them. It usually operates at a level of ‘let *C* be a category…’ with concrete categories or functors being examples. Haskell operates at a level even more concrete than single objects in a single category: the objects are types and Haskell operates on the values of those types. Of course Haskell can work at slightly higher levels too, but it never really escapes categories that look a lot like Hask.

Maybe that statement is too strong though. I’d be keen to see some interesting actual-category-theory level things in Haskell. (Maybe I’m being unfair and these do exist but I am considering them to not count as ‘actual category theory’)

I thought that the ‘categorical theory of patches’ thing was a good example of category theory *applied* to programming but note that it didn’t require any kind of general notion of e.g. push-outs in a programming language.

schoen

From my late-beginner Coq student perspective, I'm amused to think that the loop detection in Haskell (which allows you to distinguish divergence from a specific instance of a type) might have made Haskell less sound from a type theory perspective, because it is in some way intervening in the calculation to add or detect distinctions that would otherwise not be a part of the underlying theory!

Well, maybe that's not the best way to put it: but the example of using the <<loop>> detection to distinguish a loop from a concrete instance is something that Haskell added presumably for users' convenience; if it didn't have that feature, you would not, in fact, be able to distinguish the infinite loop from a specific value in finite time, except by manually examining the implementation!

markusde

IMO after the first section the headings in the post are misleading:
- A functor is "not a functor" because not all endofunctors on Hask can be written as Haskell Functors.
- A monad is "not a monad" because you can implement a monad without satisfying all the monad laws.

I don't think either of these statements _really_ evidence the claims the headings make. Good post though, I always find that it's useful to think about the subtleties between mathematical objects and their implementation.

valcron1000

This post is literally the "Ackchyually" meme. There is a reason why "fast and loose reasoning is morally correct".

eBombzor

What are the prereqs for learning category theory? I looked up a definition online and it had a lot of stuff I've never heard before. What exactly is a mapping in this context

mattpallissard

> However, if you are proficient with any functional language, especially if it is a dialect of ML,

The one, true ML.

sr.ht

I definitely don't recommend this. While cute, Learn You A Haskell is lacking a lot of pragmatic advice about how to write software in haskell. It's good for getting you up to the FAM trio of type classes but leaves out a lot of practical advice around things like navigating base (what to use and ditch from it), the available community libraries, topics like monad transformers, and pragmatic advice around things like error handling, testing, and isolating effects from tests that come up very quickly in real world Haskell development.

Haskell Programming From First Principles is a much better book IMO: https://haskellbook.com/

I haven't written Haskell in a while, but there may be even better books today as well.