6 ms·

A Path to Enlightenment in Programming Language Theory

155 points by jcurbo 11y ago

psibi 11y ago
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.
- kmicklas 11y ago
  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.
- namanbharadwaj 11y ago
  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.
- mafribe 11y ago
  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/ http://shoup.net/ntb/
  - ihm 11y ago
    > 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.9946 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.9... [2] http://www.researchgate.net/publication/2108154_A_model_category_for_the_homotopy_theory_of_concurrency http://www.researchgate.net/publication/2108154_A_model_cate... [3] https://en.wikipedia.org/wiki/Directed_algebraic_topology https://en.wikipedia.org/wiki/Directed_algebraic_topology
    - mafribe 11y ago
      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.
- tel 11y ago
  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.
- ufo 11y ago
  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.
igravious 11y ago
What is always missing for me in these lists is a tutorial for knocking together a small lambda calculus + dependently typed interpreter in C. Not ML, Not Ocaml, not, Haskell, not any language that has _already_ got lambdas in it! Always when I read these I see, "get your Haskell compiler and..." and I'm like, if I knew Haskell well enough to do that I wouldn't be doing this tutorial in the first place. Case in point, article says "particularly for programming pracitioners who didn’t learn it at school." -- Correct! I taught myself Basic, I taught myself a bit of x86 assembler, most importantly, I taught myself C. My working mental model of a computer is the C machine model. And even now, now that I know Ruby with its lambdas, I know that Ruby is written in C. And the Linux kernel. And Nginx (C++ maybe? Dunno). And on, and on. Show me the tutorial where I can build, _in C_ a bare bones working (tail recursion) implementation of the lambda calculus with type inference and dependent (algebraic?) types and I'll shake your hand and call you a champion. Closest I've seen is Make A Lisp - https://github.com/kanaka/mal https://github.com/kanaka/mal but I don't think it has the sweet types and tail recursion and other good stuff. PS: bonus points if Regexen are native type :) (Open to suggestions (I am))
- mafribe 11y ago
  Show me the tutorial where I can build, _in C_ a bare bones working (tail recursion) implementation of the lambda calculus with type inference and dependent (algebraic?) types Why would you want to do that? Type inference and dependent types don't go well together (already System F doesn't have type-inference), although it depends on the details of what you mean by dependent types. Tail recursion is a concept of compilation and does not show up in an interpreter. Note also that C has higher-order functions (via function pointers). The only relevant difference from lambda-calculus is that C functions must be named, cannot be nested and must exist at compile time. But conceptually these restrictions make little difference to the understanding of what lambda does: it creates a function. Finally writing something like that (to the extent that the requirements make sense) is gonna be really painful in C. If you understand the lambda-calculus well enough to know what dependent types are, the implementation language should not make much of a difference. I think the easiest way to learn the lambda-calculus program in a functional language. The second easiest way is to read the theory, after all the lambda-calculus as a calculus is incredibly simple, and you can hand-wave away the problems of bound-variable renaming. A slow-paced textbook like Hankin's "An Introduction to Lambda Calculi for Computer Scientists", and doing the exercises in the first few chapters should do the job.
panic 11y ago
In practice, most programming languages are not purely or even mostly functional. So why is everything on this list about functional programming?
- innguest 11y ago
  Because 20 years ago everything on every list was about object-oriented programming and I didn't complain (too much).
  - seanmcdirmid 11y ago
    PL theory has never been dominated by OOP, except for those theories specifically related to it. Just take a look at a POPL '95 proceedings. FP starts from math, for OO math had to be shoe horned into successful existing work that didn't care about it that much.
    - NotableAlamode 11y ago
      The semantics of OO languages is really messy and complicated and probably has the least well understood theory of all sequential forms of computing.
      - seanmcdirmid 11y ago
        Not just that, but we still don't really know how to combine subtyping and generics very well. The soundness question when considering variance is still quite open, and it shows in the poor support for type inference in OO languages (in spite of heroic efforts made in languages like Scala). Much of this has to do with the root: most of our PL theory was basically designed for FP, and applying them to OOP has been predictably difficult. Most PL theoreticians are more interested in FP than OOP, so progress is quite slow (though see work done by Ross Tate, Igarashi, etc...for progress).
        NotableAlamode 11y ago
jcurbo 11y ago
I spotted this on Twitter [0] and it was timely for me because I've been sorta building my own learning path lately. After learning Haskell a few years ago I got really interested in PLT, type theory, and other higher math (like CT) and also things like formal program verification and automated solvers. So I started trying to decide on a good self-study path (as a guy with a day job who's not going to be starting a Ph.D. anytime soon). I ran across this very helpful Reddit thread [1] and so far I'm thinking of the following path. I'm starting with How to Prove It, because I never did a lot of proof solving in college (and that was >10 yrs ago anyway) and it's a good basis for further work. Then I have two branches. The first is for abstract algebra and CT, because I find them interesting and they're useful for understanding Haskell, that currently consists of Pinter's A Book of Abstract Algebra, then Conceptual Mathematics by Lawvere and Schanuel, then Awodey's CT book, which is a path straight out of that Reddit thread. The second is for PLT/type theory, and starts with Software Foundations by Pierce, then Types and Programming Languages by Pierce, then Practical Foundations for Programming Languages by Harper (for completeness, as I have heard pros and cons for both), then maybe moving to Advanced Topics in Types and Programming Languages and such. Mix in some Oregon Programming Language Summer School (OPLSS) [2] videos here and there when they fit. (OPLSS sounds great and I'm glad their videos are online) [0] https://twitter.com/manisha72617183/status/613016587696648192 https://twitter.com/manisha72617183/status/61301658769664819... [1] http://www.reddit.com/r/haskell/comments/29reb7/first_or_second_edition_of_introduction_to/ http://www.reddit.com/r/haskell/comments/29reb7/first_or_sec... [2] http://www.cs.uoregon.edu/research/summerschool/ http://www.cs.uoregon.edu/research/summerschool/
- groovy2shoes 11y ago
  Pinter's A Book of Abstract Algebra is one of the best math books I've ever read. It's short, to the point, and doesn't assume you're an idiot. I learned a lot from it and I can't recommend it enough.
dschiptsov 11y ago
It is only me, or type theory is overrated and oversold?
- tel 11y ago
  I can't say it's only you, but I certainly don't agree.
  - dschiptsov 11y ago
    Donald Knuth might say so too.) The problem, in my opinion, is same as with Category theory. While the math describing behavior of categories as abstractions is probably correct, the categories themselves are mere abstractions. Consider clouds (in the sky). One could try to categorize them, but it is useless, because each cloud is unique. Same goes for companies, people, etc. Categories are useful for crude approximations but they are mere products of the mind. Types are more "concrete" than clouds, of course, but they are not essential. Yes, you could define some "iterable" and "traversable" and "foldable" categories and do scribe a list with it, but the list itself is fundamental abstraction (a basic sequence structure) and it is good-enough. Moreover, after all the type information would be striped off, it will be a "natural" chain of pointers. In other words, decent programming could be done (and has been done) without most of type theory. The notion of a ADT is enough.
    - nbouscal 11y ago
      ... You know that we do have a categorization of clouds, right? I think meteorologists would disagree with you about the utility of that categorization. More to your point: whether you can do something without a tool has no bearing on whether or not it is a useful tool. You can write programs in machine code if you'd like to, but you're highly unlikely to be as productive as someone using a high-level programming language. Similarly, you can program without a type system if you'd like to, but you're highly likely to end up with runtime errors that you wouldn't have had you used a type system.
      - dschiptsov 11y ago
javajosh 11y ago
I'd like to find a jargon-free path. There's too much gravitas, and hence ego, in the words. It's kind of like astronomy - you can (and should) start with looking up, and notice that the stars rotate around the north star. Terms like right ascension, azimuth, celestial spheres, plane of the ecliptic, etc...these are impressive and important sounding and they really get in the way of understanding. It's not arbitrary picking astronomy as my example, because in the end computers are physical systems. They are quite unique because they are capable of actions that look like violations of the second law - e.g. you can quite easily reverse a program that simulates gas diffusion, and simulate putting that gas back in a jar - that is, you can define an incredibly delicate system, and reset it for nothing, like being able to use a kitchen for anything and then clean it instantly, for free. More generally, all of a computers negentropy can be recovered for little or no cost after arbitrary disorder! They are also unique because they can rapidly and accurately and repeatedly traverse very specific state spaces, which is unlike anything in the universe, including the human brain. As a physical system, a computer extends through time, and it's state is in general time dependent. Coupling signals across time is, I believe, what programming is about. We have special names (jargon!) for different signals - we call signals that come earlier "programming" and signals that come later "runtime input". But only useful distinction is between signals that arise from outside the system, and those which arise inside (that is, programming and input are the same; but input arising from results of a function call are profoundly different). It's useful because only the latter can recurse, which is both a source of error, but also the only possible way "intelligence" (or any really complicated behavior) could possibly express. The only other thing that matters is the shape of the system state - which constrains, in some ways, the kinds of states the system can achieve (or, because it's a universal machine, it constrains the general patterns of state traversal in some hand-wavy sense). I built something that demonstrates these ideas, if anyone's interested.

155 points by jcurbo 11y ago

psibi 11y ago

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.

kmicklas 11y ago
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.
namanbharadwaj 11y ago
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.
mafribe 11y ago
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/ http://shoup.net/ntb/
- ihm 11y ago
  > 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.9946 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.9... [2] http://www.researchgate.net/publication/2108154_A_model_category_for_the_homotopy_theory_of_concurrency http://www.researchgate.net/publication/2108154_A_model_cate... [3] https://en.wikipedia.org/wiki/Directed_algebraic_topology https://en.wikipedia.org/wiki/Directed_algebraic_topology
  - mafribe 11y ago
    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.
tel 11y ago
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.
ufo 11y ago
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.

igravious 11y ago

What is always missing for me in these lists is a tutorial for knocking together a small lambda calculus + dependently typed interpreter in C. Not ML, Not Ocaml, not, Haskell, not any language that has _already_ got lambdas in it! Always when I read these I see, "get your Haskell compiler and..." and I'm like, if I knew Haskell well enough to do that I wouldn't be doing this tutorial in the first place. Case in point, article says "particularly for programming pracitioners who didn’t learn it at school." -- Correct! I taught myself Basic, I taught myself a bit of x86 assembler, most importantly, I taught myself C. My working mental model of a computer is the C machine model. And even now, now that I know Ruby with its lambdas, I know that Ruby is written in C. And the Linux kernel. And Nginx (C++ maybe? Dunno). And on, and on. Show me the tutorial where I can build, _in C_ a bare bones working (tail recursion) implementation of the lambda calculus with type inference and dependent (algebraic?) types and I'll shake your hand and call you a champion. Closest I've seen is Make A Lisp - https://github.com/kanaka/mal https://github.com/kanaka/mal but I don't think it has the sweet types and tail recursion and other good stuff. PS: bonus points if Regexen are native type :) (Open to suggestions (I am))

mafribe 11y ago
Show me the tutorial where I can build, _in C_ a bare bones working (tail recursion) implementation of the lambda calculus with type inference and dependent (algebraic?) types Why would you want to do that? Type inference and dependent types don't go well together (already System F doesn't have type-inference), although it depends on the details of what you mean by dependent types. Tail recursion is a concept of compilation and does not show up in an interpreter. Note also that C has higher-order functions (via function pointers). The only relevant difference from lambda-calculus is that C functions must be named, cannot be nested and must exist at compile time. But conceptually these restrictions make little difference to the understanding of what lambda does: it creates a function. Finally writing something like that (to the extent that the requirements make sense) is gonna be really painful in C. If you understand the lambda-calculus well enough to know what dependent types are, the implementation language should not make much of a difference. I think the easiest way to learn the lambda-calculus program in a functional language. The second easiest way is to read the theory, after all the lambda-calculus as a calculus is incredibly simple, and you can hand-wave away the problems of bound-variable renaming. A slow-paced textbook like Hankin's "An Introduction to Lambda Calculi for Computer Scientists", and doing the exercises in the first few chapters should do the job.

panic 11y ago

In practice, most programming languages are not purely or even mostly functional. So why is everything on this list about functional programming?

innguest 11y ago
Because 20 years ago everything on every list was about object-oriented programming and I didn't complain (too much).
- seanmcdirmid 11y ago
  PL theory has never been dominated by OOP, except for those theories specifically related to it. Just take a look at a POPL '95 proceedings. FP starts from math, for OO math had to be shoe horned into successful existing work that didn't care about it that much.
  - NotableAlamode 11y ago
    The semantics of OO languages is really messy and complicated and probably has the least well understood theory of all sequential forms of computing.
    - seanmcdirmid 11y ago
      Not just that, but we still don't really know how to combine subtyping and generics very well. The soundness question when considering variance is still quite open, and it shows in the poor support for type inference in OO languages (in spite of heroic efforts made in languages like Scala). Much of this has to do with the root: most of our PL theory was basically designed for FP, and applying them to OOP has been predictably difficult. Most PL theoreticians are more interested in FP than OOP, so progress is quite slow (though see work done by Ross Tate, Igarashi, etc...for progress).
      - NotableAlamode 11y ago

jcurbo 11y ago

I spotted this on Twitter [0] and it was timely for me because I've been sorta building my own learning path lately. After learning Haskell a few years ago I got really interested in PLT, type theory, and other higher math (like CT) and also things like formal program verification and automated solvers. So I started trying to decide on a good self-study path (as a guy with a day job who's not going to be starting a Ph.D. anytime soon). I ran across this very helpful Reddit thread [1] and so far I'm thinking of the following path. I'm starting with How to Prove It, because I never did a lot of proof solving in college (and that was >10 yrs ago anyway) and it's a good basis for further work. Then I have two branches. The first is for abstract algebra and CT, because I find them interesting and they're useful for understanding Haskell, that currently consists of Pinter's A Book of Abstract Algebra, then Conceptual Mathematics by Lawvere and Schanuel, then Awodey's CT book, which is a path straight out of that Reddit thread. The second is for PLT/type theory, and starts with Software Foundations by Pierce, then Types and Programming Languages by Pierce, then Practical Foundations for Programming Languages by Harper (for completeness, as I have heard pros and cons for both), then maybe moving to Advanced Topics in Types and Programming Languages and such. Mix in some Oregon Programming Language Summer School (OPLSS) [2] videos here and there when they fit. (OPLSS sounds great and I'm glad their videos are online) [0] https://twitter.com/manisha72617183/status/613016587696648192 https://twitter.com/manisha72617183/status/61301658769664819... [1] http://www.reddit.com/r/haskell/comments/29reb7/first_or_second_edition_of_introduction_to/ http://www.reddit.com/r/haskell/comments/29reb7/first_or_sec... [2] http://www.cs.uoregon.edu/research/summerschool/ http://www.cs.uoregon.edu/research/summerschool/

groovy2shoes 11y ago
Pinter's A Book of Abstract Algebra is one of the best math books I've ever read. It's short, to the point, and doesn't assume you're an idiot. I learned a lot from it and I can't recommend it enough.

dschiptsov 11y ago

It is only me, or type theory is overrated and oversold?

tel 11y ago
I can't say it's only you, but I certainly don't agree.
- dschiptsov 11y ago
  Donald Knuth might say so too.) The problem, in my opinion, is same as with Category theory. While the math describing behavior of categories as abstractions is probably correct, the categories themselves are mere abstractions. Consider clouds (in the sky). One could try to categorize them, but it is useless, because each cloud is unique. Same goes for companies, people, etc. Categories are useful for crude approximations but they are mere products of the mind. Types are more "concrete" than clouds, of course, but they are not essential. Yes, you could define some "iterable" and "traversable" and "foldable" categories and do scribe a list with it, but the list itself is fundamental abstraction (a basic sequence structure) and it is good-enough. Moreover, after all the type information would be striped off, it will be a "natural" chain of pointers. In other words, decent programming could be done (and has been done) without most of type theory. The notion of a ADT is enough.
  - nbouscal 11y ago
    ... You know that we do have a categorization of clouds, right? I think meteorologists would disagree with you about the utility of that categorization. More to your point: whether you can do something without a tool has no bearing on whether or not it is a useful tool. You can write programs in machine code if you'd like to, but you're highly unlikely to be as productive as someone using a high-level programming language. Similarly, you can program without a type system if you'd like to, but you're highly likely to end up with runtime errors that you wouldn't have had you used a type system.
    - dschiptsov 11y ago

javajosh 11y ago

I'd like to find a jargon-free path. There's too much gravitas, and hence ego, in the words. It's kind of like astronomy - you can (and should) start with looking up, and notice that the stars rotate around the north star. Terms like right ascension, azimuth, celestial spheres, plane of the ecliptic, etc...these are impressive and important sounding and they really get in the way of understanding. It's not arbitrary picking astronomy as my example, because in the end computers are physical systems. They are quite unique because they are capable of actions that look like violations of the second law - e.g. you can quite easily reverse a program that simulates gas diffusion, and simulate putting that gas back in a jar - that is, you can define an incredibly delicate system, and reset it for nothing, like being able to use a kitchen for anything and then clean it instantly, for free. More generally, all of a computers negentropy can be recovered for little or no cost after arbitrary disorder! They are also unique because they can rapidly and accurately and repeatedly traverse very specific state spaces, which is unlike anything in the universe, including the human brain. As a physical system, a computer extends through time, and it's state is in general time dependent. Coupling signals across time is, I believe, what programming is about. We have special names (jargon!) for different signals - we call signals that come earlier "programming" and signals that come later "runtime input". But only useful distinction is between signals that arise from outside the system, and those which arise inside (that is, programming and input are the same; but input arising from results of a function call are profoundly different). It's useful because only the latter can recurse, which is both a source of error, but also the only possible way "intelligence" (or any really complicated behavior) could possibly express. The only other thing that matters is the shape of the system state - which constrains, in some ways, the kinds of states the system can achieve (or, because it's a universal machine, it constrains the general patterns of state traversal in some hand-wavy sense). I built something that demonstrates these ideas, if anyone's interested.