A Path to Enlightenment in Programming Language Theory • Hacker News Board

Re: A Path to Enlightenment in Programming Language Theory

#21

Post by Silhouette » Mon, Jun 22, 2015, 9:34 PM UTC

exDM69 wrote: post #17

igravious wrote: post #6

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…

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

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.

Re: A Path to Enlightenment in Programming Language Theory

#22

Post by igravious » Mon, Jun 22, 2015, 9:36 PM UTC

agumonkey wrote: post #8

igravious wrote: post #6

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…

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

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

Re: A Path to Enlightenment in Programming Language Theory

#23

Post by locokoko » Mon, Jun 22, 2015, 9:36 PM UTC

igravious wrote: post #6

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…

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

Re: A Path to Enlightenment in Programming Language Theory

#24

Post by exDM69 » Mon, Jun 22, 2015, 9:39 PM UTC

Silhouette wrote: post #21

exDM69 wrote: post #17

Earlier quoted context omitted.

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

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 We…

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

Re: A Path to Enlightenment in Programming Language Theory

#25

Post by habitue » Mon, Jun 22, 2015, 9:41 PM UTC

mafribe wrote: post #18

exDM69 wrote: post #13

Earlier quoted context omitted.

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 langu…

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 techn…

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.

Re: A Path to Enlightenment in Programming Language Theory

#26

Post by exDM69 » Mon, Jun 22, 2015, 9:42 PM UTC

mafribe wrote: post #18

exDM69 wrote: post #13

Earlier quoted context omitted.

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 langu…

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 techn…

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.

Re: A Path to Enlightenment in Programming Language Theory

#27

Post by vezzy-fnord » Mon, Jun 22, 2015, 9:42 PM UTC

mafribe wrote: post #16

igravious wrote: post #15

Earlier quoted context omitted.

Grandparent here :) 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…

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 a…

You can completely ignore objects. Nobody ever uses them

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.

Re: A Path to Enlightenment in Programming Language Theory

#28

Post by igravious » Mon, Jun 22, 2015, 9:44 PM UTC

mafribe wrote: post #16

igravious wrote: post #15

Earlier quoted context omitted.

Grandparent here :) 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…

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 a…

Really?

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

Re: A Path to Enlightenment in Programming Language Theory

#29

Post by igravious » Mon, Jun 22, 2015, 9:45 PM UTC

locokoko wrote: post #23

igravious wrote: post #6

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…

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 ar…

Thank you!

Re: A Path to Enlightenment in Programming Language Theory

#30

Post by Silhouette » Mon, Jun 22, 2015, 9:46 PM UTC

mafribe wrote: post #14

mkehrt wrote: post #10

Earlier quoted context omitted.

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…

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…

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