News for hackers. Stuff that matters.
Re:A Path to Enlightenment in Programming Language Theory by psibi on Monday June 22, 2015 @03:40PM (#9760682)
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.
Re:A Path to Enlightenment in Programming Language Theory by mafribe on Monday June 22, 2015 @04:03PM (#9760832)
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.

[1] http://shoup.net/ntb/

Re:A Path to Enlightenment in Programming Language Theory by ihm on Monday June 22, 2015 @06:28PM (#9761611)
> 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].

[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.9...

[2] http://www.researchgate.net/publication/2108154_A_model_cate...

[3] https://en.wikipedia.org/wiki/Directed_algebraic_topology

Re:A Path to Enlightenment in Programming Language Theory by mafribe on Tuesday June 23, 2015 @04:11AM (#9763254)
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.
Re:A Path to Enlightenment in Programming Language Theory by tel on Monday June 22, 2015 @06:31PM (#9761625)
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.

Re:A Path to Enlightenment in Programming Language Theory by ufo on Monday June 22, 2015 @07:41PM (#9761849)
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.

Re:A Path to Enlightenment in Programming Language Theory by namanbharadwaj on Monday June 22, 2015 @03:56PM (#9760794)
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.
Re:A Path to Enlightenment in Programming Language Theory by kmicklas on Monday June 22, 2015 @03:53PM (#9760770)
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.