A Path to Enlightenment in Programming Language Theory
1–10 of 99 posts
Re: A Path to Enlightenment in Programming Language Theory
#2How 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
#3How 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 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.
Re: A Path to Enlightenment in Programming Language Theory
#4How 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.
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
#5How 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.
Re: A Path to Enlightenment in Programming Language Theory
#6What 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 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))
Re: A Path to Enlightenment in Programming Language Theory
#7What 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…
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
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.
Re: A Path to Enlightenment in Programming Language Theory
#8What 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…
Here's a famous reddit comment about bootstrapping a language: http://www.reddit.com/r/programming/comments/9x15g/programmi...
Also this was here not long ago https://news.ycombinator.com/item?id=9699065
Re: A Path to Enlightenment in Programming Language Theory
#9In practice, most programming languages are not purely or even mostly functional. So why is everything on this list about functional programming?
Re: A Path to Enlightenment in Programming Language Theory
#10What 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…
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 comp…
I don't think the grandparent wants all of these features at once necessarily in a single tutorial, but an introduction to them in a language that they already know.
Also, the things you say that function pointers don't have are exactly the things that make lambdas interesting. Lambdas are anonymous and, crucially, can be nested. It's the very nesting that is what makes them difficult to get right, as they close over their containing scope. Variables mentioned in lambda bodies that are not parameters get their values from the definition scope, not the scope where they are used. In C function pointers, this issue doesn't even come up.