A Path to Enlightenment in Programming Language Theory

by jcurbo • 11 years ago

155 97 11 years ago

psibi• 11 years 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• 11 years 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• 11 years 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.

mafribe8• 11 years 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/

ihm• 11 years 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.9...

[2] http://www.researchgate.net/publication/2108154_A_model_cate...

[3] https://en.wikipedia.org/wiki/Directed_algebraic_topology

tel4• 11 years 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.

ufo6• 11 years 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.

igravious9• 11 years 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 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))

mafribe8• 11 years 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.

mkehrt• 11 years ago

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.

agumonkey2• 11 years ago

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

igravious9• 11 years ago

Ha, I remember that from not long ago.

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...

exDM694• 11 years ago

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.

edit: Here's the relevant code if you're interested: https://github.com/rikusalminen/funfun/blob/master/FunFun/De...

Silhouette5• 11 years ago

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.

locokoko• 11 years ago

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?

Enjoy! http://t3x.org/s9book/index.html

igravious9• 11 years ago

Thank you!

jrapdx3• 11 years ago

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.

See http://www.call-cc.org/

igravious9• 11 years ago

Another fine suggestion, thanks!

swah• 11 years ago

That's something I liked about jonesforth (https://raw.githubusercontent.com/AlexandreAbreu/jonesforth/...) ! but its not a lambda calculus interpreter I guess.

igravious9• 11 years ago

Not what I had in mind but intriguing nonetheless.

tel4• 11 years ago

If LLVM is good enough for you... http://www.stephendiehl.com/llvm/ and http://dev.stephendiehl.com/fun/ (in progress)

igravious9• 11 years ago

Thank you, indeed it is :)

sklogic3• 11 years ago

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).

I wrote about such a bootstrap some time ago: https://combinatorylogic.wordpress.com/2015/01/14/bootstrapp...

igravious9• 11 years ago

That's a bit defeatist, we don't know until we try!

chewie123• 11 years ago

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)!

panic• 11 years ago

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

innguest• 11 years ago

Because 20 years ago everything on every list was about object-oriented programming and I didn't complain (too much).

seanmcdirmid3• 11 years 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.

exDM694• 11 years ago

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.

mafribe8• 11 years ago

    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.

vezzy-fnord2• 11 years ago

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.

AnimalMuppet3• 11 years ago

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).

sklogic3• 11 years ago

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.

jcurbo• 11 years 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/61301658769664819...

[1] http://www.reddit.com/r/haskell/comments/29reb7/first_or_sec...

[2] http://www.cs.uoregon.edu/research/summerschool/

groovy2shoes• 11 years 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.

dschiptsov5• 11 years ago

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

tel4• 11 years ago

I can't say it's only you, but I certainly don't agree.

dschiptsov5• 11 years 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.

pekk• 11 years ago

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.

dschiptsov5• 11 years ago

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.

JesperRavn3• 11 years ago

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.

dschiptsov5• 11 years ago

which can express almost any constraints at compile time

... except heterogeneous lists, hash-tables and conditionals.)

nbouscal5• 11 years ago

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.

javajosh• 11 years 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.

A Path to Enlightenment in Programming Language Theory

Related Stories