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 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 :)
> knocking together a small lambda calculus + dependently typed interpreter in C. Not ML, Not Ocaml, not, Haskell, not any language that is _already_ got lambdas in it!
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.
The flip side of this is that if you're writing something in C, you actually do have to understand how details like closures are implemented on real hardware. These are not trivial problems, yet many programming language design papers and articles effectively brush the whole issue of actually implementing these things under the carpet.
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.
This is not quite true. There is SPJ's famous "The implementation
of functional programming languages" [1]. Then there is lots of
material on various abstract machines, like the SECD machine, the
CAM, the many variants of the Krivine machine, the G-machine and
plenty of others whose name I forget.
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.
> The flip side of this is that if you're writing something in C, you actually do have to understand how details like closures are implemented on real hardware.
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.
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.
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.
Thats because tutorial material is going to keep things simple. If you really want to implement a garbage collector on your own then you should go looking for an advanced compiler book instead of a tutorial.
Of course. But it's still reasonable to ask how you'd write a compiler that implements such features in a free-standing way, without depending on either the built-in tools of the language you're writing an interpreter in or a black box run-time environment/VM that does all the tricky stuff for you by magic. With a relatively low-level language like C, you don't have any choice but to confront such issues head-on, while many tutorials manage to side-step them using higher-level languages. Of course it's easier to write almost anything in a suitable higher-level language, but for educational purposes that isn't really the point IMHO.
You're confusing levels. If you are compiling to C or assembly, you have to understand how the constructs you are building work. That places no requirement on the language of implementation of the compiler.
Yes, but IME many tutorial presentations on these subjects never get as far as actually building a complete, functional compiler to demonstrate the concepts. Often they use some form of interpreter instead, which means they can use structures in the interpreter's implementation language that somewhat reflect the run-time structure of the implemented language using the analogous language features.
Well, it makes sense for tutorials to use what they can to simplify the bits they're not focusing on, but certainly implementing a construct by mapping it into an identical construct is not going to be terribly informative as to the workings of that construct. That may be totally appropriate if the focus of the tutorial is on the parsing or such, but it sounds like that sort of tutorial (of which there are many, and which are perfectly useful to other purposes) are not what you are looking for.
I'm not sure if it satisfies all your needs,
but Scheme 9 from Empty Space is a full R4RS Scheme implementation written from scratch in pure C (and Scheme).
It has a heavily commented source code and a book, which is supposed to be quite good.
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?
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.
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.
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.
I strongly recommend that you ignore this feeling and learn a modicum of ML coding. If you want to learn TAPL, just learn a bit of Ocaml. You don't need much. If you already speak C, a bit of Haskell and Ruby, you should be able to pick up enough Ocaml in a few hours/days. Programming in Ocaml is way easier than in Haskell or C. The only two things that are a bit difficult in Ocaml are modules and the object system. You can completely ignore objects. Nobody ever uses them, and for TAPL you can also ignore modules (although you occasionally have to open a module, which is trival, something like: open Support.Pervasive).
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...
I've written vast amounts of Ocaml and C/C++, certainly over 100K LoCs in each. Programming in ML dialects is so much easier than C/C++, it's not funny. I'd estimate it takes me about 10 times longer to implement the same functionality in C/C++ than in an ML dialect. The three key features enabling this difference are the following.
* 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...
Are you sure C is simpler then ML? If you really get into the nitty gritty details (which is what you do when interacting with programming language theory), the definition of the lambda calculus fits in a single page and an ML-lite that is powerful enough for real programming is just a little larger than that.
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.
You think that assembly needs less of a manual than C? You think assembly has less dark corners? You think it's going to make things simpler? My mind boggles.
Oh, and also, which assembler? 68000? x86? ARM? (One of these is not like the others in terms of complexity...)
Maybe talking about undefined behavior wasn't the best approach I could take :) But if you stick to simple machine languages then it shouldn't be a big problem. Something that is closer to Knuth's MIX than to x86 won't have much undefined behavior.
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.
> Today I'm going to learn how to build a car. First, take the engine from my Toyata... oh... um...
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.
I agree with you it'd be useful to see how you might implement lambdas in a language like C. But after that first example, implementing other more complicated language constructs in C, instead of learning ML/haskell is going to be more time fighting C, and less time learning anything new. The lack of side-effects and equational reasoning in functional languages let you get a lot of details out of your way.
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.
Actually ... You (kind-of/sort-of) need side effects when implementing a language with higher-order functions. You at least need it for generating fresh variables to avoid free name capture. Yes, I know you can do this with a monad, but this is not going to help a beginner. It's much easier to maintain a global counter that you increment every time you want a fresh variable name.
The way I did it was just recursively pass down an accumulator argument to generate De Bruijn index-like variable names, rather than keeping a global counter
Point taken though that it's a bit simpler with global state
> I would like an introduction to these advanced topics in the language that I already now.
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!
It's actually a lot easier to learn ML and then read/write the interpreter in ML than to read/write the interpreter in C. An interpreter written in C would be too convoluted.
I did point out the nesting and the requirement to name in C.
The scoping follows immediately from beta-reduction
(lambda x.M)N --> M[N/x]
which I find very intuitive. I never had trouble understanding this, but maybe I'm overgeneralising from my own learning process. The real difficulty, or rather the real subtlety, is not nesting but name binding and the automatic renaming of bound variables where necessary. Having taught lambda-calculus to generations of students, that causes confusion with some students.
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.)
The real difficulty, or rather the real subtlety, is not nesting but name binding and the automatic renaming of bound variables where necessary.
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...
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...
That "C is portable assembly language" mantra bugs me a bit. There are lots of things that are dirt simple in real assembly language but impossible to do in (standard) C: tail call optimization, computed gotos, arithmetic overflow detection, SIMD, control over registers and local variable allocations, etc...
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.
I don't know how field-famous he is, but googling his name (he has a ML named after him) was full of fun crazy hacks idea. Like writing binaries under MS-DOS (just the few commands it provides like dir, copy etc) by using codepage keycodes `COPY CON > MY.COM`. And then expanding possibilities.
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 :)
There is no point in doing such things in C, since C is just too low level.
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).
And a great many fine suggestions have been made. To add one more, you might take a look at CHICKEN Scheme. It's written in C, and compiles to C.
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.
The first language I learned was C. I don't claim to be an expert, but I'm comfortable enough with it that I can hack on an OS kernel with C.
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)!
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)
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.
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.
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.
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.
> 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].
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.
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.
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.
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.
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.
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.
"Decent" programming is a wiggle word. I'm of course obliged to agree with you when you define it. In a similar way, decent programming can be done with Turing Machines, punch cards, raw circuitry, brainfuck, what-have-you. Each would require a notion of "decent" in line with the style of the tool, but there is no hard place to push against when defining "decent".
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.
... 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.
Except when the type system restricts you to homogeneous data-structures in inherently heterogeneous world. Herbert Spencer, the philosopher, could tell us a lot about it.
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.)
It is part of the marketing for several "new hotness" languages (however long ago their development started). Back when Java was new, the same marketing talk was directed at OOP, which isn't cool any more.
Especially when we consider how Java crowd have misunderstood OOP and emphasized stupid class hierarchies and static typing (and design patterns as a result) instead of message-passing and message-based polymorphism and protocols as the essence of the original paradigm developed by Smalltalk authors.
It is certainly oversold. There is a typical discussion that goes
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.
I've spent a lot of time hanging out with pretty hardcore type theory people, and have never seen any of them recommend a dependently-typed language to a new programmer. In other words, you're pretty blatantly fighting a straw man.
It's not about how experienced the programmer is. The problem is that people do a bate and switch when it comes to type theory, promising the benefits of dependent types even though there are no production languages that deliver these benefits.
I've similarly never seen anyone promise the benefits of dependent types when talking about simpler type systems. Why would they need to? Much simpler type systems already have more than enough benefits to be worthwhile.
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.
>Much simpler type systems already have more than enough benefits to be worthwhile.
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.
You "addressed" it by referring to "studies" that you didn't cite. There are studies that go both directions on the question, none of which have good enough methodology to be worth more than a tiny update in either direction. Most of the studies are about extremely weak type systems (C, Java, etc.), and therefore don't provide any evidence at all about type systems that are stronger than Java but weaker than dependent types (e.g. Swift, Rust, Haskell, etc).
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.
Because imperative programming is not very interesting from a programming language theory point of view. If this was a list about compiler construction, it would look very different.
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.
I'm afraid I disagree, the opposite is the case. Modern PL theory is mostly about program correctness, and that is much easier for pure functional languages. Until recently, nobody had a handle on program logics for imperative languages, or reasoning techniques for operational semantics. The only available reasoning techniques used to be based on denotational semantics, following Scott's breakthrough domain-theoretic semantics of lambda-calculus. That's why so much theory was developed in a functional programming context, because FP is in some ways much simpler than imperative or concurrent programming (even though compiling FP languages is harder). The available textbooks reflect this state of afairs.
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.
This is the real answer. The restrictions on functional languages that make them (perhaps) harder to use for everyday programming makes them much easier to reason about and prove properties of.
Oh, I agree with this. "Interesting" was a poor choice of words. It's definitely interesting but then again, as you say this changed in the past decade or so. Getting introduced to a new topic by exploring the latest state of the art without going through the basic theory first isn't a good way to learn most subjects.
I know it is possible. But I wonder what stops us from doing it for most programs we write from day to day. And, if proving correctness is indeed important (I believe so), can we do something / what is the next thing to do to enable us proving correctness in our daily job.
What stops us is cost. Formally verifying non-trivial properties (in the sense of CompCert) with current technology is several orders of magnitude more expensive and time-consuming than programming and a bit of testing. And this price is almost never worth it.
We hope that this cost can be lowered in the future.
The commonplace languages in use are difficult to reason about. It would take a serious paradigm shift for most companies to stop what they're doing and develop a tool chain for wholesale program verification. Additionally, it takes a special breed of programmer to be able and willing to write code in such a way that enables verification, then actually take the time to verify it. Functional programming is a jump for most main stream engineers, it is an altogether different matter to recruit or develop a team of engineers familiar with dependent type theory and formal verification.
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.
For an example of what mafibre is talking about: even proving that a BubbleSort implementation is correct is quite tricky.
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.
Because imperative programming is not very interesting from a programming language theory point of view.
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.
In practice, most programming languages are compiled via SSA or even Array SSA, i.e., via a pure functional intermediate representation. And understanding it thoroughly is a huge advantage.
Note the word "enlightenment" in the title. Everything on the list is about functional programming languages because the author believes that, once you are enlightened, of course you're going to use functional programming languages.
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).
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.
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).
I suspect that combining generics with subtyping might always lead you into the land on undecidable type-inference. After all, pure genericity (System F) is already undecidable.
It is possible that he's referring to mutable and covariant types being unsound.
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.
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))