Follow

A common link I did not expect to find between category theory and Haskell programming is that if your types line up, it's very very unlikely that you're wrong

@socks this also partially applies to Rust, and it's an amazing paradigm to write software under!

@socks wait i thought the whole thing of Haskell was that it was category theory but programming? :0

@alexandria Well, sort of! There is a lot of category stuff involved but you don't need to know actual category theory (as in the branch of mathematics) to do it

And now that I'm studying actual category theory I'm seeing parallels and it's neat

@socks @alexandria uhhhm akchually hask is not a category

(sorry for the shitpost reply i liked the conversation but i just didnt know what to say and im awkward)

@thornAvery Eheh, it's fine. I didn't know that actually, I'm still learning category stuff and have only applied it to topology so far, I haven't seen how it relates to Haskell other than just intuition

Hopefully that will change soon, it's one of the topics I'm thinking about looking into for my master's thesis

@socks ah you’re probably ahead of me, I started Hasklel and since then hav ebeen trying to learn more category theory

the shitpost comes down to (at least in my understanding) that a lot of haskell’s category theory pretends that values cant crash or hang forever because otherwise a lot of assumptions break, so all the category theory holds up but theres a big asterisk for *unless something crashes or hangs forever

@socks I thought the behaviour of monads was dependent on knowledge from category theory, so to use them properly you had to know it <:O

At least that's when i was last looking into it like 5 years ago lol

its what stopped me from learning it, I was like "im going to learn category theory first" and watched some lectures, then that slowly got shunted off my todo lol

@alexandria @socks you should give it a go! i didnt know any category theory before i started, and I love the language.

I do like lisp a lot too though :)

@alexandria In my experience, not at all. You can absolutely use monads in Haskell without knowing what they are in the category theory sense!

@socks @alexandria To add anecdotal evidence to this, I learnt Haskell monads before learning category theory monads. And in one of our courses, we teach monads in functional programming and definitely don't assume category theory. (See lean-forward.github.io/logical)

Basically, the only 2 parts of FP monads you need to understand category theory for, is why they have this name and why people say "a monad is just a monoid in the category of endofunctors, what's the problem?"

@Vierkantor @socks Yea, but five years ago most programmy news outlets were spammed with everyone trying to explain what they thought a monad was, all failing in different ways, and most people saying just go back to the category theory to properly "get" it

@Vierkantor @socks It's cool that the situation hss changed,,, but it was hella confusing back then lol

@alexandria @socks Oh yeah, the "let me explain how a monad is just a burrito" years, the scourge of the FP community.

At least we got a great parody called "Burritos for the hungry mathematician" out of it: emorehouse.wescreates.wesleyan

@Vierkantor @socks I think at that time I actually had the patience (read: being forced into a 30m train journey every day) to read about type theory, set theory, SPJ's book on making programming languages, and category theory

not only did i learn a bunch, but ive already forgotten like 90% of it 😂😂😂

@socks @alexandria By the way, if you're interested in learning dependently-typed programming and/or formal verification, that's basically my job and I'm more than happy to guide you! :D

Sign in to participate in the conversation
social.emisocks.com

Emil Socks' personal instance!