7 ms·

A Path to Programming Language Theory

174 points by rspivak 10y ago

Normal_gaussian 10y ago
This is exactly what it says on the tin. A path to enlightenment. I've read a lot on these subjects already, but I am certainly saving this for two reasons: * Including papers and sections of books in my weekly reading * I find it quicker to understand if I can grab a handful of explanations and critique them (often rewriting the confusing parts of several explanations once understood) If you want an easy list, or a minimal list, this isn't it - and I am glad.
deleted 10y ago
[deleted]
infodroid 10y ago
One thing that is sorely missing here is a section on motivation, which is arguably the first step on the journey. Because I can see that learning PLT will be hard. Yet most people are not going to learn PLT just because it is hard. There must be something more that makes it worthwhile. But I struggle to appreciate why any programmer would want to learn PLT.
- Xophmeister 10y ago
  Why does anyone learn anything? An intellectual pay-off is, to many, just as valuable as the practical (and ultimately, presumably, economic) pay-off that comes from learning a new skill. That might be seen by many others to be "learning for learning's sake", but any research could potentially lead to wider benefits. That said, for die-hard-pragmatists, it seems reasonable to assume that learning PLT might make one a better programmer.
krat0sprakhar 10y ago
I've been taking a PLT[0] class in school and while the list above is extremely comprehensive and thorough, I'd argue that you do not need to read up all of it to get a good idea of programming languages. Without even learning all the theory, you can get pretty far ahead (IMHO) in a building your own programming language (if that's the goal). The two resources that I've found invaluable are - the prog lang course[1] by Dan Grossman and PLAI[2] by Shriram. Lastly, there's also a whole bunch of interesting university courses that you can refer to - https://github.com/prakhar1989/awesome-courses#programming-languages--compilers https://github.com/prakhar1989/awesome-courses#programming-l... [0] - http://www.cs.columbia.edu/~sedwards/classes/2016/4115-spring/index.html http://www.cs.columbia.edu/~sedwards/classes/2016/4115-sprin... [1] - https://www.coursera.org/course/proglang https://www.coursera.org/course/proglang [2] - http://cs.brown.edu/courses/cs173/2012/book/ http://cs.brown.edu/courses/cs173/2012/book/
- ianai 10y ago
  I can imagine someone being overwhelmed by all of those at first glance (in OP).
- spriggan3 10y ago
  thanks , your links look way more reasonable than pure theory and mathematics for new comers who just want to implement simple programming languages and compilers.
- tikhonj 10y ago
  There's a difference between learning about programming languages and learning about programming language theory. The class you linked is squarely in the former camp. It's a bit confusing because they use PLT to stand for "Programming Languages and Translators" where I usually see it referring to "Programming Language Theory". Honestly, "programming language theory" is a bit of a misnomer. It's less a theory for programming languages and more a theory of CS from a language perspective. (Where theoretical CS is a theory of CS from a computational point of view.) Programming language theory is interesting in and of itself and is fairly distinct from the sorts of things you'd learn in a normal programming languages course or by implementing your own language. I'm not saying either of those is useless—I'm a big fan of doing both!—just that they accomplish fundamentally different things. Your advice is good if you just want to implement a programming language; the linked repository is good if you want to explore PL theory. PL theory shares a lot with formal logic and the foundations of mathematics. The main areas are things like type theory (a special approach to formal logic) and semantics (akin to proof theory or model theory). What you'll learn by reading the books linked above is almost completely disjoint from what the class you linked covers.
mpweiher 10y ago
This seems very one-sided, skewing towards type-theory and functional programming. Is that what is taught these days? No wonder people think that's all there is. :-(
- munin 10y ago
  any book list that starts with "first you should read TAPL and PFPL, then move on to SF and CPDT and read HOTT and of course these three category theory textbooks" is really out of touch IMO. mostly because i don't think there's anyone alive that has simultaneously read all of those works, not even the authors of each individual work!
  - madgar 10y ago
    I'm 27 and while I'm only about halfway through HOTT - it's tough - I've read all the other named books. TAPL was tough too but invaluable to wrap my head around as an undergraduate.
  - fmap 10y ago
    You're seriously underestimating the amount of work that goes into a phd, or into writing a textbook...
    - munin 10y ago
      I'm a current PhD student in programming languages, I don't think I am...
      - fmap 10y ago
        Let's talk again in a few years. :) In all seriousness, though, I'm also just speaking from personal experience. That said, if you are working in type theory, chances are that you will end up skimming almost everything on this list...
        munin 10y ago
paxcoder 10y ago
I (and I'm sure others) would appreciate references to the minimal set of things necessary to absorb to easily participate in the PLT discussion. This is the opposite of that.
gravypod 10y ago
I know this might be a stupid question for some, but I have to ask anyway because this will drive me crazy trying to figure this out on my own. Why is this a 'theory', what makes this different from a documentation different design patterns in programming languages?
- rntz 10y ago
  It's basically a certain kind of documentation of design patterns in programming languages. PLT emphasizes the use of formal logic and mathematics. It focuses on systems that can be rigorously defined, and theorems that can be proven about them; as opposed to software engineering, which focuses on the issues and patterns that crop up in the practice of developing software, or HCI, which focuses on human factors. Of course, all of these are overly broad generalizations, and it's not as if there aren't points of intersection between these different ways of looking at programming languages. But the kind of stuff you'll see in a book like Types and Programming Languages is super-different in approach from the kind of stuff you'd see in, say, the Gang of Four book, both of which are different again from Bret Victor's approach.
  - gravypod 10y ago
    Are there any benefits or contributions made by this method that couldn't be simply done by "doing" it. IE: Implement a language and use that as an example and improve it.
    - mathetic 10y ago
      No, it is a completely egotistical and futile exercise used to produce public funding consuming academics. This method of doing things offers a sound approach to developing things rather than ad-hoc implementations. It allows properties about the method to be proved with absolute certainty. In hindsight after you have "done" it, everything seems they were doable. Monads for example proved to be very useful in functional languages, and as Phil Wadler puts it "it is doubtful that the structuring methods presented here would have been discovered without the insight afforded by category theory. But once discovered they are easily expressed without any reference to things categorical. No knowledge of category theory is required to read these notes." in his now famous paper [0]. But maybe monads are too exotic to provide a good example. Let's talk about higher-order functions instead. Closures are very common to all programming languages these days and they existed long long before we had the first computer thanks to the lambda calculus. It would be nice then we look at lambda calculus to understand use and ramifications of such constructs. What they are good for, if they have limitations, etc. More importantly, there seems to be a correspondent logic to useful type theories we come up with (or perhaps discover). One famous example is Curry-Howard correspondence [1]. So it might be useful if we understood what has come decades, sometimes centuries before, rather than reinventing the wheel. [0] http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/ba... [1] https://en.wikipedia.org/wiki/Curry–Howard_correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence
cousin_it 10y ago
I've spent a lot of time on learning these ideas. They are interesting in themselves, but also because they come with a tantalizing promise of usefulness. For me, that promise was never fulfilled. I suspect that's not just bad luck. Creating programming languages is mostly a practical problem, not a research problem. For example, type theory will never tell you that garbage collection is a good idea, or which kind you should use. My advice to younger folks looking at this field would be to turn back and instead solve some practical problem by creative programming. Git or BitTorrent would be good examples to emulate. Even a smaller project could have more impact than the whole field of PL research combined.
Smaug123 10y ago
I was struck by the category theory section, which starts with two fairly easy books (Cheng and Awodey), a book I've never heard of, and then Mac Lane. Mac Lane is a fearsome book, which takes a lot of concerted effort and study for me to read. I have had four years of the Cambridge Maths Tripos, so I am (ahem) probably quite a bit more highly trained in mathematics than most readers of this list, and Mac Lane is just barely on the edge of things I can read. It should come with a health warning for its extreme difficulty and abstraction; there's a reason it's in the "Graduate Texts" series.
- thechao 10y ago
  I had the same feeling when Ben Pierce's introductory text was tossed casually into the same list as HOTT. I mean... more power to you, but a few lines of text are casually glossing over probably a decade of study for the reader.

174 points by rspivak 10y ago

This is exactly what it says on the tin. A path to enlightenment. I've read a lot on these subjects already, but I am certainly saving this for two reasons: * Including papers and sections of books in my weekly reading * I find it quicker to understand if I can grab a handful of explanations and critique them (often rewriting the confusing parts of several explanations once understood) If you want an easy list, or a minimal list, this isn't it - and I am glad.

deleted 10y ago

[deleted]

infodroid 10y ago

One thing that is sorely missing here is a section on motivation, which is arguably the first step on the journey. Because I can see that learning PLT will be hard. Yet most people are not going to learn PLT just because it is hard. There must be something more that makes it worthwhile. But I struggle to appreciate why any programmer would want to learn PLT.

Xophmeister 10y ago
Why does anyone learn anything? An intellectual pay-off is, to many, just as valuable as the practical (and ultimately, presumably, economic) pay-off that comes from learning a new skill. That might be seen by many others to be "learning for learning's sake", but any research could potentially lead to wider benefits. That said, for die-hard-pragmatists, it seems reasonable to assume that learning PLT might make one a better programmer.

krat0sprakhar 10y ago

I've been taking a PLT[0] class in school and while the list above is extremely comprehensive and thorough, I'd argue that you do not need to read up all of it to get a good idea of programming languages. Without even learning all the theory, you can get pretty far ahead (IMHO) in a building your own programming language (if that's the goal). The two resources that I've found invaluable are - the prog lang course[1] by Dan Grossman and PLAI[2] by Shriram. Lastly, there's also a whole bunch of interesting university courses that you can refer to - https://github.com/prakhar1989/awesome-courses#programming-languages--compilers https://github.com/prakhar1989/awesome-courses#programming-l... [0] - http://www.cs.columbia.edu/~sedwards/classes/2016/4115-spring/index.html http://www.cs.columbia.edu/~sedwards/classes/2016/4115-sprin... [1] - https://www.coursera.org/course/proglang https://www.coursera.org/course/proglang [2] - http://cs.brown.edu/courses/cs173/2012/book/ http://cs.brown.edu/courses/cs173/2012/book/

ianai 10y ago
I can imagine someone being overwhelmed by all of those at first glance (in OP).
spriggan3 10y ago
thanks , your links look way more reasonable than pure theory and mathematics for new comers who just want to implement simple programming languages and compilers.
tikhonj 10y ago
There's a difference between learning about programming languages and learning about programming language theory. The class you linked is squarely in the former camp. It's a bit confusing because they use PLT to stand for "Programming Languages and Translators" where I usually see it referring to "Programming Language Theory". Honestly, "programming language theory" is a bit of a misnomer. It's less a theory for programming languages and more a theory of CS from a language perspective. (Where theoretical CS is a theory of CS from a computational point of view.) Programming language theory is interesting in and of itself and is fairly distinct from the sorts of things you'd learn in a normal programming languages course or by implementing your own language. I'm not saying either of those is useless—I'm a big fan of doing both!—just that they accomplish fundamentally different things. Your advice is good if you just want to implement a programming language; the linked repository is good if you want to explore PL theory. PL theory shares a lot with formal logic and the foundations of mathematics. The main areas are things like type theory (a special approach to formal logic) and semantics (akin to proof theory or model theory). What you'll learn by reading the books linked above is almost completely disjoint from what the class you linked covers.

mpweiher 10y ago

This seems very one-sided, skewing towards type-theory and functional programming. Is that what is taught these days? No wonder people think that's all there is. :-(

munin 10y ago
any book list that starts with "first you should read TAPL and PFPL, then move on to SF and CPDT and read HOTT and of course these three category theory textbooks" is really out of touch IMO. mostly because i don't think there's anyone alive that has simultaneously read all of those works, not even the authors of each individual work!
- madgar 10y ago
  I'm 27 and while I'm only about halfway through HOTT - it's tough - I've read all the other named books. TAPL was tough too but invaluable to wrap my head around as an undergraduate.
- fmap 10y ago
  You're seriously underestimating the amount of work that goes into a phd, or into writing a textbook...
  - munin 10y ago
    I'm a current PhD student in programming languages, I don't think I am...
    - fmap 10y ago
      Let's talk again in a few years. :) In all seriousness, though, I'm also just speaking from personal experience. That said, if you are working in type theory, chances are that you will end up skimming almost everything on this list...
      - munin 10y ago

paxcoder 10y ago

I (and I'm sure others) would appreciate references to the minimal set of things necessary to absorb to easily participate in the PLT discussion. This is the opposite of that.

gravypod 10y ago

I know this might be a stupid question for some, but I have to ask anyway because this will drive me crazy trying to figure this out on my own. Why is this a 'theory', what makes this different from a documentation different design patterns in programming languages?

rntz 10y ago
It's basically a certain kind of documentation of design patterns in programming languages. PLT emphasizes the use of formal logic and mathematics. It focuses on systems that can be rigorously defined, and theorems that can be proven about them; as opposed to software engineering, which focuses on the issues and patterns that crop up in the practice of developing software, or HCI, which focuses on human factors. Of course, all of these are overly broad generalizations, and it's not as if there aren't points of intersection between these different ways of looking at programming languages. But the kind of stuff you'll see in a book like Types and Programming Languages is super-different in approach from the kind of stuff you'd see in, say, the Gang of Four book, both of which are different again from Bret Victor's approach.
- gravypod 10y ago
  Are there any benefits or contributions made by this method that couldn't be simply done by "doing" it. IE: Implement a language and use that as an example and improve it.
  - mathetic 10y ago
    No, it is a completely egotistical and futile exercise used to produce public funding consuming academics. This method of doing things offers a sound approach to developing things rather than ad-hoc implementations. It allows properties about the method to be proved with absolute certainty. In hindsight after you have "done" it, everything seems they were doable. Monads for example proved to be very useful in functional languages, and as Phil Wadler puts it "it is doubtful that the structuring methods presented here would have been discovered without the insight afforded by category theory. But once discovered they are easily expressed without any reference to things categorical. No knowledge of category theory is required to read these notes." in his now famous paper [0]. But maybe monads are too exotic to provide a good example. Let's talk about higher-order functions instead. Closures are very common to all programming languages these days and they existed long long before we had the first computer thanks to the lambda calculus. It would be nice then we look at lambda calculus to understand use and ramifications of such constructs. What they are good for, if they have limitations, etc. More importantly, there seems to be a correspondent logic to useful type theories we come up with (or perhaps discover). One famous example is Curry-Howard correspondence [1]. So it might be useful if we understood what has come decades, sometimes centuries before, rather than reinventing the wheel. [0] http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/ba... [1] https://en.wikipedia.org/wiki/Curry–Howard_correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence

cousin_it 10y ago

I've spent a lot of time on learning these ideas. They are interesting in themselves, but also because they come with a tantalizing promise of usefulness. For me, that promise was never fulfilled. I suspect that's not just bad luck. Creating programming languages is mostly a practical problem, not a research problem. For example, type theory will never tell you that garbage collection is a good idea, or which kind you should use. My advice to younger folks looking at this field would be to turn back and instead solve some practical problem by creative programming. Git or BitTorrent would be good examples to emulate. Even a smaller project could have more impact than the whole field of PL research combined.

Smaug123 10y ago

I was struck by the category theory section, which starts with two fairly easy books (Cheng and Awodey), a book I've never heard of, and then Mac Lane. Mac Lane is a fearsome book, which takes a lot of concerted effort and study for me to read. I have had four years of the Cambridge Maths Tripos, so I am (ahem) probably quite a bit more highly trained in mathematics than most readers of this list, and Mac Lane is just barely on the edge of things I can read. It should come with a health warning for its extreme difficulty and abstraction; there's a reason it's in the "Graduate Texts" series.

thechao 10y ago
I had the same feeling when Ben Pierce's introductory text was tossed casually into the same list as HOTT. I mean... more power to you, but a few lines of text are casually glossing over probably a decade of study for the reader.