How much does algebra contribute to learning Type theory ? I'm currently working on the How to prove it book. I thought, I would jump to TAPL after finishing that.
I also don't think studying algebra helps you directly with programming language theory. However algebra is of indirect help if you want to learn category theory, because the latter is a direct generalisation of the former. It is rather difficult for a non-mathematician to pick up category theory from scratch without having first seen the the algebra that category theory abstracts from. Universal properties, category theory's most important concept, appears bizarre and disconnected from reality, unless you have seen it working in the much simpler settings of groups, rings, modules etc.
To that caveat, I'd like to add that neither Rotman nor Birkhoff/MacLane are ideal places to start learning algebra. There are plenty of gentler, more modern books. In terms of tomes that are available online, I can recommend Shoup's "A Computational Introduction to Number Theory and Algebra" [1].
As an aside, note that category theory is used only in the part of programming language research that is about (pure) functional programming. In other sub-fields (e.g. OO, logic programming and concurrency), category theory has not so far proven terribly useful.
> In other sub-fields (e.g. OO, logic programming and concurrency), category theory has not so far proven terribly useful.
I wouldn't say that. I don't know about OO and logic programming, but there's a good amount of categorical/homotopical structure lurking around concurrency. See for example [1], [2] or [3].
You mean Goubault-style homotopy stuff. I don't this this is very categorical, e.g. [2] produces a single category, so I wouldn't call this an example of categorical structure.
The Gunawardena paper [1] doesn't exhibit categorical structure either.
It's not a direct dependency in the sense that algebra is a direct dependency of, say, algebraic topology.
Instead it's more like a guiding friend. A lot of PL theorists are well-versed in algebra and use it at least stylistically to do their work. If you are familiar with algebra you'll recognize it all over.
But you can definitely get by without it for a while.
The only downside is that you may go a little more slowly due to a general lack of analogies and you may have a difficult time finding resources which don't use algebraic examples.
But honestly, a lot of PL (in fact, TAPL) don't really depend upon abstract algebra much at all.
Type theory is closer to logic than it is to algebra. But for things like TAPL that don't get into really deep type theory you don't need lots of previous knowledge.
Knowing how to prove things and express your self rigorously is very helpful though, but its generally helpful for any part of computer science, not just programming languages.
Studying algebra from a categorical perspective is probably significantly more relevant. Other than that, learning algebra is probably useful primarily to acquire the mathematical maturity and abstract thinking that is involved in PL theory.
I don't think algebra is super useful in itself for standard PL stuff or for, say, writing verified code in Coq. However (perhaps unfortunately?) it is a common source of examples for texts on type theory, and you'll definitely need it to understand the more categorical approaches, and especially HoTT.
