Haven't watched the video, but it's clearly being marketed for people who are sick and tired of being told they have to learn about category theory just to do things that other programming languages let you do without any fuss or pedantry.

It's inevitable that people will take things originally developed in a theoretical context and try to filter out some of the original abstract machinery as people learn informal and more intuitive ways to describe them to a wider audience.

Look at which avatar Haskell gets.

I feel like it's not different from anything else: I can imagine a freshman programming student saying "who cares about all the jargony words like signed or unsigned? it's all the same in practice". The point being, yes, you don't need category theory to do functional programming, but if you don't and try programming long enough, your lack of understanding will hinder you.

The difference is, you can teach the concepts in an accessible and open way, that's good. What's not good is the dismissive attitude.

I actually think it won't hurt you too much. Programming is unique compared to other forms of learning, because you get to represent formal ideas tacitly just by having written a program. There's nothing you can say in category theory that can't be imagined and represented in Lisp.

That said, an appreciation for formal types can help you compose program components faster before you've written any code at all, and more importantly, it can avoid mistakes: a slogan of Haskell is that one ought to use the type system to make incorrect programs unrepresentable.

Should we all be using Haskell rather than Lisp / Python / Ruby / Javascript / C / Go? Perhaps. But should people learn about category theory before they learn Haskell? I doubt it.

I'm not making the assertion that people should learn category theory before Haskell, I'm making the assertion that knowing it is beneficial. It's clearly not all or none, and people making extreme statements in either direction should be ignored, really.

Incidentally, what I find rather funny is that both my reaction to some of the things Wadler is complaining about Lisp, and my ******* behavior on this board both bring to mind the Lisp avatar in that matrix. Lol, I'm him. I haven't even showered today.

Edit: Just to be clear, since I used the word Matrix, I'm not saying I'm Neo. I'm saying I'm the ******* with the funny shirt.

Yeah, I definitely think it's wrong to bash math. What's most important is that they don't think it's harder than it really is, because usually it's not.

Ideally, a very small amount of math gets introduced in the beginning, but then one has to know when to stop.

Edit: And most people who know enough math to be dangerous don't know when to shut up and just end up scaring people. You do NOT want to learn Haskell from somebody who thinks they are right in forcing you to do anything but a minimal amount of work learning something like category theory. And EVERY single abstract thing should have a concrete justification showing why it was introduced. A teacher who can't do this but still has a boner for math is worse than nothing and is hurting the student.

..wouldn't that just depend on what your goal is? If you're just learning some functional programming for a few specific applications, then sure, category theory is too much, but I can't see how it would be bad to do some in depth studying for all people in all contexts.

Programmers reject computer science at least as much as they bash math. In my experience it's more about insecurities than genuine distaste.

Probably true, given actual CS is basically mathematical. "Who cares about big-O anyway? The algorithm works. If it doesn't scale then I'll update it then, so what?"

yup.

see also: make everything a hash map.

It wouldn't at all be a bad idea for a smart and curious person to learn category theory to try and better understand programming languages.

What would be a very bad idea would be to do so without first asking: "Why learn about category theory at all in the context of programming languages?", simply because the answer to that question can save you from thinking about these concepts in the wrong order and learning them in a way that you can't efficiently make use of that knowledge in a meaningful way (but hey, welcome to the typically bad expository material academic writing makes for).

In particular, it doesn't make sense to learn about category theory for programming languages if you don't realize that by doing so, you should understand that you are effectively studying type theory. But hey, looking at that answer, we see that we can already become better programmers just by reasoning about these things and asking these questions, since the concepts being illuminated are quite basic. From that answer, we see that category theory helps us appreciate functions in a rigorous and clear way, and just like set theory was a boon for mathematics, we could expect category theory to be a boon for understanding functional programming.

Finally, it also might be a good idea to keep in mind that I've seen programming language semantics researchers express misgivings about the slippery character of Haskell's type system: it might not be all that very well defined the way languages like ML are, and actually doesn't really map to category theory in the way that mathematicians understand category theory. Haskell types, from what I've read (I'm not a Haskell programmer) are sort of their own "category theory inspired" thing, but you might not want to simply assume that they "are" categories that work like the ones you might have seen in mathematics.

Now, if I wanted to learn about Haskell and category theory, rather than go all academic and learn about types and categories, I'd probably take a read of this paper, which makes use of category theory to solve problems in computer science, but introduces all the category theory needed in a self-contained way, so that it isn't a distraction from the real problem being solved.

But I mean, to really appreciate that paper, you should already know about functional programming idioms. So I still say don't learn category first (well, in that particular path).

Supposedly a book that really founds mathematics and types from the ground up in a way that is directly applicable to programming languages, but is an elegant mathematical work in its own right, is Paul Taylor's Practical Foundations of Mathematics. Of course this book is just as much about type theory as it is about categories (it's about both!).

or maybe start with https://www.cis.upenn.edu/~bcpierce/tapl/


On the subject of type systems, I don't know how to segue this better, but C++'s type system is getting a type system and I'm irrationally excited for it and also amused by the idea.

Actually what I said about category theory / types / Haskell is a little silly. From what I understand, Haskell more or less is its type system. Well, there's a lot more there, but it's probably its defining feature.

So if understanding Haskell's type system means learning a bit of category theory, then yeah, it probably makes sense to bite the bullet and understand it in full detail right away. Some practical applications thrown in wouldn't (edit) hurt, though. Actually there was a cottage industry of books for a while basically with the single goal of disabusing people of the idea that Haskell was just useless and theoretical, with titles like Real World Haskell.

If we're talking about functional programming in general, though, you don't need types or categories. That's what Scheme gives you: a functional programming language that's a lisp, which is based on the untyped lambda calculus. You get to keep track of everything yourself and if your program fails it's your fault (but at least it won't be a memory fault).

Edit: oops, meant to say wouldn't HURT, not wouldn't "help". Dur.

I am equally amused that C++ seems to continue to grow without bound. It's sort of changing my understanding of what a programming language can be. Will C++ in 2030 look anything like it does today? Will we be seeing C++ with Quantum Computing extensions?

2030? only if nobody cares enough about quantum computing to have an opinion about it.

lol

Looking at that book by Pierce (I'd seen it before but it looked dense to me at the time) and skimming it on Amazon, the contents look pretty nice. It's probably much better than the book I suggested for people who might want to understand different programming languages through the lens of types.

I've looked at the book by Harper on types and programming languages, but that book seems more sweeping, and is more encyclopedic and concise.

Actually, rather than just read the book by Pierce, if one really wants to understand types, nowadays one can read and work out a book (same principal author) that is itself a giant coq script. This looks very tempting.

Edit: coq bonus points:



https://ncatlab.org/nlab/show/Coq#applications

The book by Pierce is the standard CS textbook. I'm just sayin', while we're debating the pedagogy of type systems to programmers, there are entire university departments already thinking about that.

You are right.

I looked a bit more at the coq book, and Pierce et al (like I said, same principal author) do introduce type systems somewhere in the second volume (and the older, more in-depth book on types by Pierce gets a citation (very bottom)), but before you even get here you are forced to go through all of volume 1, which introduces coq and goes on to use it in various ways.

I wouldn't know if the use of coq is helpful in this context, but I imagine it would be a bad idea to burden the student into simultaneously trying to learn about types, while also forcing him/her to also make use of a dependent type system system (coq) to also show the correctness of the type system being studied.

(Both books claim to have no prerequisites beyond mathematical maturity.)

I should probably try to better appreciate why a course which seeks to formally proving correctness will make for a completely different topic.

Looking through the coq book, one doesn't get very far at all, and only the simplest type systems are verified.

It's like how in quantum mechanics they tell you how to completely specify the hydrogen atom. And then, well, guess what: for almost everything too much bigger than a hydrogen atom, it is completely intractable to write down the wave function.

Going back to functional programming, there seem to be abstract approaches that use category theory but don't seem to have to try too hard to reason about correctness. I haven't looked into this enough to see if this is because the kind of program that such a style is capable of expressing is vastly restricted to some very abstract dialect of functional programming, or if the emphasis is simply on the abstraction and correctness isn't even attempted.

For example, one can organize functional programming using category theory around optimization:

I find that first link totally imcomprehensible, I don't know enough programming to make heads or tails of what it's saying, lol. I also know almost nothing about type theory so I'm really useless there.

However, I know one of the professors here does some stuff in homotopy type theory. I'm barely getting into the higher homotopy theory, but I might end up learning type theory stuff coming up so, I should probably bookmark a few of these links.

Don't worry about those slides, that was just something I found after Googling the name of the book they are based on (The Algebra of Programming). I linked to that book in the second link pair of links, along with a discussion of it. I haven't read the book, but it is fairly well regarded in the Haskell community as a rather beautiful application of category theory that also uses equational reasoning. I'm afraid I don't know much about what equational reasoning is, except to say that it makes use of algebra in logic, and goes back to Boole. Haskell is well suited for equational reasoning, though, and Bird also has a more recent book on writing equational programs in Haskell, but this time he took out almost all the math and just used Haskell programs to demonstrate the idea.

As for homotopy type theory... this thing looks really cool. And interestingly enough, it seems to be closely connected to coq, which is a piece of software for writing verifiable specifications as a sort of game, using things called 'tactics' that can help you write programs that it turns into proofs of correctness. Most people who have used coq find it to be a major pain in the ass, though. It is not the only way one can verify software specifications, and indeed from what I can tell it is a rather low level one. Higher level modelling tools include things like TLA+ and Alloy, but these are much more geared toward industrial use (though they have a sound mathematical foundation of their own).

Jon suggested a book on type theory, which would certainly be the best one to start with if you just care about type theory. I think it is geared toward people who care mostly about programming languages.

On the other hand, if you really care about homotopy type theory, you might want to check out coq at some point, since the underlying theory between the two things seems to overlap. I posted a link in my previous posts to another book where Benjamin Pierce appears as an author, which is much broader than his book on types which Jon`C posted. This book uses coq to verify a bunch of things, not just types, though it has you verify a primitive type system in the second volume. Of course, if you just care about Homotopy Type Theory, you could just see what those people have to say about learning coq as soon as possible. It also might be worth investigating just what a dependent type system is. I wouldn't know, but it sounds like the answer might be interesting.

As it happens, Vladimir Voevodsky (RIP) was adamant about convincing mathematicians to write their proofs in something like coq, and homotopy type theory largely promises to subsume mathematics into something that can be verified, hopefully without too much trouble (although don't quote me on this, since I am sure those aren't its only motivations... actually, see the link at the end of my post for a good story on the topic's roots). As it stands today, though, most mathematicians don't want to write their proofs in something like coq, and I think most people agree that it's a still a pain to do so as of today. From what I've read there is considerable ramp up required in encoding all the tricks you've learned to rely on but may not realize it. That said, one of Voevodsky's motivations for caring about verification of proofs was that a major result of his turned out to have a critical bug in it, and he only discovered this 20 years later!

I think you should definitely check out the Paul Taylor book if you want a general background on all this. It should be available from your university library. n-Lab and the n-category cafe are also great places to look for discussions about these things. Read about Cartesian Closed Categories in Paul Taylor's book, or in something John Baez has written, or somebody else in the n-sites I mentioned.

Actually, that book says it includes material on dependent type theory, which I imagine would be important if you care about coq.

Sadly, it looks like the HTML version of Paul Taylor's book is pretty ****ed up in my browser: none of the math is rendering. Anyway, the book is beautiful in print, but I'd never read this ****ty online version.

Brutal snippet from Taylor's site:

Also on the topic of formalizing some intuitive use of set theory, here's an awesome (and easy!) book by a pioneer in the topic: https://www.amazon.com/Sets-Mathematics-F-William-Lawvere/dp/0521010608/

Understandable even by undergraduates.

Top notch proofwriting from only the finest.

Did Stephen Smale send that to you?

Looks like algebraic and / or geometric topology with the formal definitions factored out.

If I wasn't such an idiot who is ignorant of basic definitions about subjects I supposedly took classes in I would have phrased that last attempted witticism in the proper terminology fitting of the topology joke that it's trying to be

yup algebraic topology with the formal definition factored out

i needed to argue why the degree of the homology classes wasn't weird, and it's intuitive to see why, so i just kinda drew why the degrees line up how they do

it's honestly more rigor that the professor gives so it should be fine

Interesting. Coq/theorem proving software certainly sounds neat. I'm guessing the checker works back the whole way down to theorems it's checked before, starting from whatever axioms you start from? That certainly seems powerful, but from what you've said it sounds more like it's difficult to implement and that's holding it back more.

I don't think anyone here is much involved with Coq style stuff, but I'll ask around after spring break.

Also grad school pickles your brain. I just spent 20 hours straight studying. I'm exhausted and my brain is short circuiting from the caffeine.

Also having to run every day + eat healthy to maintain an unhealthy caffeine usage is time consuming.

Also, my parents bought me a genetics test kit for Christmas. The only genetic markers I have: I have genes correlated with a tendency to sleep deeply, to consume excess caffeine and to be underweight. All of which describe me, except not so much underweight as thin for a person who ate as much trash as I did in my early 20s.

Moral of the story: the snake lemma rules, and I was able to smash a problem using it in a cool way.

I really feel like running right now but it's 30 degrees out. Guess I'll have to bundle up. See y'all in a few miles.

ok KOOBS


only keeeeeding

I just ran a half marathon... second one in two weeks! *flexes quads*