A Path to Enlightenment in Programming Language Theory
steshaw.org
steshaw.org
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))
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.
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.
The scoping follows immediately from beta-reduction
(lambda x.M)N --> M[N/x]
And I think implementing a type-inferencer in C is going to be confusing because beauty of e.g. the W type-inference algorithm is drowned by orthogonal issues that C forces on you like memory management. Interpreters are best written in languages with pattern matching. So I prefer to bootstrap one's learning: get the basics of lambda-calculus, then implement a lambda-calculus interpreter and type-inferencer in a modern FP language. (As an aside, that's what SICP also does.)
If you're trying to understand what a closure does, perhaps that's true.
If you're trying to understand how it does it, and you come from an imperative programming background where you know the ABIs for your languages like the back of your hand and are used to the kind of function set-up that always allocates space for local variables on the stack, there is a huge question of how all that lovely, neat theory is actually implemented in practice.
Some of this discussion reminds me of the jokes about professors who prove that a solution to some elegantly expressed problem must exist, but then lead it to the grad students to actually find it...
Indeed, you have put it more succinctly and cogently that I ever could.
I would like an introduction to these advanced topics in the language that I already now. For instance, for a Haskell module I was studying we used a teeny tiny interpreter that had been created just for the task of learning the basics of Haskell. This interpreter was written in Lua. It was small, and I could follow the logic of it. It lacked type inference though, and if I had seen a tutorial _in C_ about how to bolt on a Hindley Milner type inference engine to a lambda calc core I bet I could have made a stab at improving this toy project.
Even with Ruby now I bet I code Ruby as if it were a really dynamic C. I hardly ever use map() or collect(), for instance. I just don't have it in my mental toolbox. I'm not total loser though, I do like my {|o| blocks!}
I need to emphasize this. I am fluent in C, and can think in it. When I open Pierce TaPL and see immediately ML my heart sinks.
When I open Pierce TaPL and see immediately ML my heart sinks.
This is an oft-made statement about OCaml, but it simply isn't true. 0install and Opa are two major projects that use the object system, for instance.
I feel like C fits my brain, know what I mean? I don't even think that it was because I learnt it early on. It's a simple language, I feel.
Why is programming way easier in Ocaml than in C? Setting aside that for me programming is way easier in C than in Ocaml because I know C and don't know Ocaml, what is it about Ocaml that is way easier than C?
Anyway, my original point is that it is _cheating_ to explain how to build a Lisp by saying, "First reach for your nearest functional programming language". Useless car analogy. Today I'm going to learn how to build a car. First, take the engine from my Toyata... oh... um...
Why is programming way easier in Ocaml than in C?
* Garbage collection, removes all memory bugs, avoids tons of ugly and distracting (de)allocation commands and keeps your head free to think about more important stuff.
* Pattern matching, enables you to code up complex decision making code (and most functinality needs this) in a readable and maintainable way.
* higher-order functions allow you to parameterise code with behaviour in a neat way.
(There is one caveat, which is code for extremely high performance, I'd probably write that in C/C++, but this is not an issue concerning a learner.)
As to useless car analogies, I think implementing lambda in C is like saying: Today I'm going to learn how to build a car. First, let's do this while riding a uni-cycle ... oh... um...
On the other hand, C needs a manual with hundreds of pages and has lots of dark corners and undefined behaviour. IMO, if you really want to keep things simple you need to stick to assembly language instead of C.
Oh, and also, which assembler? 68000? x86? ARM? (One of these is not like the others in terms of complexity...)
The thing that I was thinking about was that many operations that are defined in assembly language, such as integer overflow are undefined in C (and this undefined behavior is often abused by optimizing compilers) and C also abstracts over a lot of control flow conventions.
To the extent that the analogy works, it doesn't help your case: nobody these days builds or learns how to build a car from scratch, without access to an existing car. It's not only that you're typically making a modified version of an existing model: you also use a car to get to the factory, you use existing vehicles to transport raw materials and tools to the factory, etc.
In any case, as others have pointed out, it's not like you need to use a full {Lisp, Haskell, ML} compiler to implement (say) tail recursion. It's that you bootstrap: as soon as you have a minimal viable {Lisp, Haskell, ML} compiler, it makes sense to use that instead of C to implement other features.
That being said, this is if you're interested in the theory. If you're interested in building compilers, this list won't help too much.
The lack of side-effects and equational reasoning in functional languages let you get a lot of details out of your way.
Point taken though that it's a bit simpler with global state
The problem with this may be best expressed by Whorf[1]:
"Language shapes the way we think, and determines what we can think about."
A philosophical school of thought concerned with this is known as Linguistic Relativity[2]. But I digress.
Part of internalizing foreign concepts is approaching them with minimal prior prejudices. Trying to relate concepts inexpressible in C to C idioms is extremely difficult, if not impossible, before being able to _translate_ those concepts into what can be represented in C. It's the classic "chicken and egg" problem.
The best thing I can think to recommend is to pick a language which is generally considered capable of supporting the concepts you wish to learn and approach it as if you have never seen a programming language before.
> When I open Pierce TaPL and see immediately ML my heart sinks.
IMHO, this reinforces the fact that tools which you have used before (likely to great success) are influencing your view of those tools which you are not as familiar. IOW, you learned BASIC, x86 assembler, and C... Why not ML?
Best of luck and hopefully the path you walk is fun!
1 - http://www.searchquotes.com/quotation/Language_shapes_the_wa...
Also this was here not long ago https://news.ycombinator.com/item?id=9699065
That's a _bit_ extreme though. Let's start with C, the portable assembly language. Having said that, now that WebAssembly is on the cards (boo, hiss), we'll have many more of these from-the-ground-up affairs.
re: reddit thread: that Kragen, name is familiar...
I agree it's a bit much to answer your question, but the spirit is there. And I agree, although learning lisp in lisp was very valuable on the intellectual level, the ignored primitives (cons, gc, interned symbols, IO) are worth knowing too. I found this book (warning: french) http://www.decitre.fr/livres/la-programmation-applicative-97... at a library, discussing a scheme system up until the io primitives. It was a great read. Sidenote: they called macros doubly-recursive functions :)
If you want to make things really low level, then make a compiler that targets assembly language and then bootstrap it. Coding the first version of the compiler in assembly or C instead of something more suitable for the task is just unnecessary pain.
This wouldn't be any more educational and just plain painful. "Research" programming languages tend to work very well for building compilers, that's why they are used in many toy programming language projects.
Dealing with tree and graph structures in a language like C would be a lot of work, a lot of effort going into memory management which is not at all useful towards the goal of learning how to implement a language.
To give a practical example: last time I was working on a toy compiler using Haskell, I needed to calculate the strongly connected components in a directed graph to perform dependency analysis (rearranging "letrecs") that is required to do type inference. Had I been writing the compiler in C, it would have required a week's worth of engineering to get done. With Haskell, I could grab Data.Graph.SCC and be done in a few hours. Arguably I could have picked up a graph library in C, but then I'd have to spend time understanding how memory management works in the library and so on.
I understand the appeal in using C or just an imperative programming language but quite frankly, that would really hurt the pedagogic aspects of a project like that.
edit: Here's the relevant code if you're interested: https://github.com/rikusalminen/funfun/blob/master/FunFun/De...
Go ahead and search for that particular example. There is almost nothing on the Web about practical, real world techniques for implementing that sort of programming language feature, despite its ubiquity in functional languages and the increasing presence of -- or emphasis on -- higher order functions and related tools in mainstream imperative languages. The same could be said of many other non-trivial language features, say laziness, or various concurrency models.
I think this is regrettable, because it creates a real barrier for anyone who's interested in learning about these features and maybe writing their own languages one day, but who doesn't come from an academic background where this kind of material was taught. It also makes it unnecessarily difficult for someone from an imperative programming background -- which is probably still the overwhelming majority of programmers -- to understand the real costs and performance implications of using these kinds of features.
If you're writing a compiler targeting real hardware and not a high level virtual machine, you'll need to learn how to implement closures regardless of the "host" language you write your compiler in.
But you're correct, when implementing an interpreter, it's so much easier if you have a garbage collector and an object system of some kind at hand. You'll have to implement this yourself if you're working with C.
Right, but a lot of the tutorial material in this area doesn't really consider that issue, even though it's rather fundamental to practical applications. Instead the explanation often settles for some sort of indirect dependency on the implementation language's existing version of a similar feature. I think this is unfortunate, not least because it reduces us to a model where most people implementing these ideas depend on some sort of magic run-time environment instead of learning how to actually write that run-time.
All that said, I kind-of agree with you. It would be nice to have some easy to grasp explanations of how to compile higher-order functions to actual machines, x86, ARM, MIPS ... This material can be found e.g. in Appel's book [2], but I don't think it's available freely (and legally) on the web. I think this is in parts because the compilation process is not so easy: you need to understand the compilation of normal languages, in particular stack layout, and then add more pointers. You also need to think about how to do memory management if a closure lives longer than its creating context. This is quite rich material, and not even usually covered in undergraduate compilers courses.
The situation with concurrency is much worse, but that only reflects the fact that this is far from a solved problem on many levels. To cite a recent paper [3]: "Despite decades of research, we do not have [in 2015] a satisfactory concurrency semantics for any general-purpose programming language that aims to support concurrent systems code [...] Disturbingly, 40+ years after the first relaxed-memory hardware was introduced (the IBM 370/158MP), the field still does not have a credible proposal for the concurrency semantics of any general-purpose high-level language that includes high-performance shared-memory concurrency primitives. This is a major open problem for programming language semantics."
And memory models are but one issue to deal with in concurrency.
[1] http://research.microsoft.com/en-us/um/people/simonpj/papers...
[2] A. Appel, Modern Compiler Implementation in ...
[3] M. Batty et al, The Problem of Programming Language Concurrency Semantics.
Here are some key points from the website which the book addresses:
- How does tail call elimination work?
- How is macro expansion implemented?
- How is arbitrary precision arithmetics implemented?
The CHICKEN website and user manual contain a wealth of info re: theory and implementation of the compiler. The development team has always been friendly and willing to answer questions.
What is normally done is a very simple and stupid, but extensible language bootstrapped with C (or whatever else), and then grown up to a level when it's convenient to implement a functional language compiler (i.e., at least higher order functions and some pattern matching).
I wrote about such a bootstrap some time ago: https://combinatorylogic.wordpress.com/2015/01/14/bootstrapp...
I have also learnt how to write compilers for simple languages (mostly from Appel's book). Through reading the book, I picked up ML. At first it was an uncomfortable transition from C, but I eventually loved writing ML code. Strong typing eliminates a lot of common errors, and the compiler really feels like a friend that's watching over you.
Later on, I decided to pick up Haskell. Frankly it was a lot harder to get used to it (I still can't say I understand Haskell) because of how side effects in Haskell are made much more explicit than either C or ML. But after about a year and a half, I can now code comfortably in Haskell. And if someone let me choose a language that I can only code in for the rest of my life, it might actually just be Haskell.
But ML and Haskell are not without their problems.
C and functional languages like ML/Haskell have different problem domains. Haskell, being (almost) pure, is really good at modeling side-effect free computations.
The compiling process is really a translation process (thus a computation), and it's easier to model it in Haskell. It is quite easy to mess things up in a language like C where side-effects show up everywhere, although if you're disciplined enough you could probably translate a Haskell program into C with some modifications.
But Haskell/ML is definitely not for everything. I would not write a kernel in Haskell (although I do know people who have done it). With the runtime problem aside, it doesn't give me enough control over the bare metal it's running over (or it's probably I just don't know it well enough yet). I can't layout things exactly the way I want with Haskell, but with C, I can build structs, cast integers into pointers (might not be a good idea, but sometimes necessary when you're dealing with a kernel) and so on. With C it feels like you're the creator, taking care of everything, hence, you have much more responsibility on your shoulder. But with Haskell, the compiler takes care a lot of things for you if you're in the right problem domain, and it lets you focus on abstractions and the problem itself.
Anyway, just a little thought. I love Haskell and C equally, and they're both absolutely wonderful languages. But try to keep yourself open and just try a little bit of new things at a time. Pretty soon you might find yourself designing compiler for your own language in Haskell (or C)!
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/61301658769664819...
[1] http://www.reddit.com/r/haskell/comments/29reb7/first_or_sec...
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.
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.
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
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.
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.
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.
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.
As for crude and misleading clasdification - there is no shortage for them, especially in realms of psychology (hypohondric, sangvinic - all that nonsense) or economics and finance. The results of application of flawed economic/financial models based on flawed categories could be seen everywhere. For meteorology, please, ask anyone who lives in monsoon area - there is worse than coin-flipping accuracy when it comes to hill regions.)
My belief about type theory is that it serves, for purposes of PL, as a massively more difficult challenge than merely making a programming language which also happens to spawn programming languages on accident.
This is really important because as we've seen—PL design without some deeper driving purpose or mechanism for making tradeoffs can wind up wherever you want it to be. LOLCODE is a real thing and without Type Theory the only way we can talk about our distaste for it is to say that it's "indecent" for deeply personal reasons.
Type Theory wouldn't accept this because its goal is to be a good foundational system for all logic and mathematics.
It's also important to note that Type Theory doesn't serve this purpose by being aligned to some arbitrary goal. It works because the goal of "being a good foundational system for all logic and mathematics" is not so dissimilar from the goal of a PL which might be "represent all interesting thoughts of a programmer in a computable fashion". If Type Theory happened to stumble across non-computable mechanisms then it would be a poor fit, but because it turns out to be the case that the best foundational system must respect computability... things match up.
And ultimately that's the joy of learning Type Theory and programming with it: things match up. I say this flippantly because I lack the words for the enormity of the "matching up" that occurs.
Before I knew Type Theory I felt that PLs were cute and arbitrary. It was interesting to learn them anthropologically, but frustrating to use them because I was building on foundations of sand. After learning Type Theory I understand where the hard places are, where the foundation exists, and I know how to build things which I feel confident can last hundreds of years.
A: I'm a simple Python programmer. Please tell me why I need types.
B: Types let you catch many bugs that would otherwise cause compile time errors or require compile time checks or testing.
A: But I've seen studies that suggest that static typing does not prevent bugs.
B: When I said static typing, I meant dependently typed languages, which can express almost any constraints at compile time, not just the basic constraints expressed by static typing.
A: Great, you've convinced me. What dependently typed languages can I use in my production system.
B: Errrr
As a mathematical theory, a way to think about programming, and a research project for future languages, type theory is very interesting. But it's not otherwise that useful for the practicing programmer.
... except heterogeneous lists, hash-tables and conditionals.)
I'm not actually looking to debate you, your mind is made up and there's very little chance I'll change it, not that it would matter if I did. I mainly just want to point out for others reading this that your arguments are blatant straw men.
Also just fyi, it's "bait and switch".
If that's your opinion, why did you ignore the fact that I addressed this in my original post? You accuse me of having a straw man argument, and yet you can't even engage with what I've written?
Anyway, you're right that neither of us is likely to convince the other, but I have really seen arguments that go like the one I described, and you're really doing me a disservice by ignoring the details of what I posted.
Meanwhile we have a lot of people who have used both weak type systems and strong type systems who claim that strong type systems make their jobs dramatically easier, and we have a lot of people who have only used weak type systems who claim the opposite. Take a survey of people who have actually done non-trivial work using a language with a good type system, and you'll get very clear results about their view of the benefits. Clearly an RCT would be better, but given that training takes a long time, that just isn't feasible.
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).
soundness question when considering variance
But I thought that was pretty well understood, so I don't know what he thinks is open...
As an example, let's assume that you have two classes, Cat and Dog, both inheriting from Animal, and that you have a covariant mutable List implementation.
Say you have a value of type List[Cat]. Since List is covariant, this value can legally be passed to a function that expects a parameter of type List[Animal].
Now, imagine you have a function that expects a List[Animal] and adds a Dog to it. That's a legal operation: Dog extends Animal and can thus be used this way.
Putting the two together, you have a perfectly legal way of adding a Dog to a List[Cat], which a sound type system should not allow. An example of that is Java's Array, which is both covariant and mutable, and that as a result can yield type errors at runtime.
As we're seeing more and more language features originating from functional programming trickle into mainstream languages, this research hasn't clearly gone to waste even though everyone is not programming in functional programming languages.
imperative programming is not very interesting from a programming language theory point of view.
All that has changed in the last decade or so, but it will take another decade or so before recent research insights into non-functional languages perlocates down to accessible textbooks.
We hope that this cost can be lowered in the future.
The industry tends to lag behind academia by at least a couple decades. In the 90's, lots of research was being devoted to functional programming and the various applications of type systems. Now we see various companies starting to use languages like Haskell and ocaml. Nowadays, it seems like dependent types and program verification are popular in academia, so maybe we'll see some of that by 2030.
First of all, you need to correctly define the specification. Saying "the returned list is sorted" isn't enough because that would also accept lists that have nothing to do with the input, like [1,2,3,4,5]. Also saying that the list only contains elements from the input is also not enough because that would accept a returned list with duplicated or missing elements. To really make a specification that models what you want you need to say that the returned list is a sorted permutation of the input list.
Then, once you manage to get a formal specification that is actually what you want prout invariantving it is also hard. In the bubble sort case you need to figure you need to write down the proofs in detail, down to the point when you use the fact that comparison is a transitive relation.
I don't know, I find GCL and predicate transformer semantics to be quite interesting. Esterel's approach to synchronous reactive systems, too.
I don't see why the research potential in imperative languages couldn't be ripe. The semantic possibilities are large. A ton of PL and OS research from ETH Zurich, Xerox PARC and Bell Labs alike have been from imperative language designs.
If you find that condescending and/or narrow-minded, you're not alone. There are more things in programming language theory than are dreamt of in their philosophy (to steal a line from Shakespeare).