I’d be interested! No knowledge of topology. I’ve been annoyed several times by watching talks at a programming conference titled “Why Programmers Should Learn Category Theory”, and they never explain why, they only define basic CT ideas and say “These are cool!”. Still overall convinced that there’s interesting things hiding in CT.
Not to steal countedblessings’ thunder, but you may be interested in “Category Theory for Programmers”.
I’m not actually convinced that “programmers” in general should learn category theory. (Though I don’t know it well, myself.) I do think there’s an analogy between programming and category theory which is interesting to think about and can lead to important insights in PL design; but when someone else has had those insights, other people can use them without knowing category theory.
There are a bunch of really great introductions to category theory, and this is definitely one of them. There’s also Youtube videos of his lectures going over the same material.
My plan is to go very slowly, and to assume everything needs to be explained in as much detail as possible. This will make for a tediously long but hopefully very readable series.
For what it’s worth, I tried reading that (I’d seen it recommended elsewhere, and this latest mention reminded me to give it a try).
I haven’t quite given up yet, but it’s not looking good. I found the preface to be thoroughly unconvincing as an argument for why I (a “working programmer”, as Milewski puts it) would want to learn category theory; and the next chapter (the Introduction) seems to be packed with some of the most absurd analogies I have ever seen, anywhere. (One of which is outright insulting—what, so the reason we need static type systems is that programmers are nothing more than monkeys, hitting keys at random, and with static typing, that randomly generated code will not compile if it’s wrong? But I am not a monkey; how does this logic apply to a human being who is capable of thought, and who writes code with a purpose and according to a design? Answer: it doesn’t.)
I will report back when I’ve read more (or finally given up), I suppose…
Immediately after the bit about monkeys there’s this
The usual goal in the typing monkeys thought experiment is the production of the complete works of Shakespeare. Having a spell checker and a grammar checker in the loop would drastically increase the odds. The analog of a type checker would go even further by making sure that, once Romeo is declared a human being, he doesn’t sprout leaves or trap photons in his powerful gravitational field.
which feels like a bit of an own goal to me, because I suspect the analogue of a type checker would actually make sure that once Romeo is declared a Montague it’s a type error for him to have any friendly interactions with a Capulet, thus preventing the entire plot of the play.
That’s an interesting (and amusing) point—I didn’t even think of that when reading it! (I was too busy shaking my head at the basic absurdity of the analogy: what human playwright, when writing a play, would accidentally have one of their main characters turn into a plant or a stellar object or any such thing? If we take the analogy at face value, doesn’t it show that type checking is manifestly unnecessary if your code is being written by humans…?)
Furthermore I don’t get how type checking would help monkeys write code any better. They would just have less code compile (and the same is true of adding a spelling and grammar checker to their Shakespeare plays)
To be clear, I recommend the “teaching category theory to programmers” aspect of it, which I remember being effective at teaching me. I have no particular memories of the “convincing programmers to learn category theory” aspect.
I’d be interested! No knowledge of topology. I’ve been annoyed several times by watching talks at a programming conference titled “Why Programmers Should Learn Category Theory”, and they never explain why, they only define basic CT ideas and say “These are cool!”. Still overall convinced that there’s interesting things hiding in CT.
Not to steal countedblessings’ thunder, but you may be interested in “Category Theory for Programmers”.
I’m not actually convinced that “programmers” in general should learn category theory. (Though I don’t know it well, myself.) I do think there’s an analogy between programming and category theory which is interesting to think about and can lead to important insights in PL design; but when someone else has had those insights, other people can use them without knowing category theory.
https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/
There are a bunch of really great introductions to category theory, and this is definitely one of them. There’s also Youtube videos of his lectures going over the same material.
My plan is to go very slowly, and to assume everything needs to be explained in as much detail as possible. This will make for a tediously long but hopefully very readable series.
For what it’s worth, I tried reading that (I’d seen it recommended elsewhere, and this latest mention reminded me to give it a try).
I haven’t quite given up yet, but it’s not looking good. I found the preface to be thoroughly unconvincing as an argument for why I (a “working programmer”, as Milewski puts it) would want to learn category theory; and the next chapter (the Introduction) seems to be packed with some of the most absurd analogies I have ever seen, anywhere. (One of which is outright insulting—what, so the reason we need static type systems is that programmers are nothing more than monkeys, hitting keys at random, and with static typing, that randomly generated code will not compile if it’s wrong? But I am not a monkey; how does this logic apply to a human being who is capable of thought, and who writes code with a purpose and according to a design? Answer: it doesn’t.)
I will report back when I’ve read more (or finally given up), I suppose…
Immediately after the bit about monkeys there’s this
which feels like a bit of an own goal to me, because I suspect the analogue of a type checker would actually make sure that once Romeo is declared a Montague it’s a type error for him to have any friendly interactions with a Capulet, thus preventing the entire plot of the play.
That’s an interesting (and amusing) point—I didn’t even think of that when reading it! (I was too busy shaking my head at the basic absurdity of the analogy: what human playwright, when writing a play, would accidentally have one of their main characters turn into a plant or a stellar object or any such thing? If we take the analogy at face value, doesn’t it show that type checking is manifestly unnecessary if your code is being written by humans…?)
Furthermore I don’t get how type checking would help monkeys write code any better. They would just have less code compile (and the same is true of adding a spelling and grammar checker to their Shakespeare plays)
To be clear, I recommend the “teaching category theory to programmers” aspect of it, which I remember being effective at teaching me. I have no particular memories of the “convincing programmers to learn category theory” aspect.