Lambdas > Lembas?

By Scott

Hey everyone, Part 2 of PFPL, oh my! Friday night we covered chapter 8 where we start adding functions to our language E, this was in short, awesome!

Next week we will move on to chapter 9 where we meet System T and I am really excited to hear more about Pete’s implementation, https://github.com/pbevin/systemt . We meet as usual at 6:30 pm at Bento Miso on Friday night.

Before discussing chapter 8, I wanted to talk briefly about Ben’s implementation of E which he shared with us a couple of weeks back and I have been remiss in recapping. Seeing this really brought out the concrete applicability of the ideas expressed in PFPL and gave life to the sometimes (always?) terse and concise mathematics used in PFPL. Not sure about others, but I really want to have a go at doing that myself, it seemed like an exercise that would be very rewarding.

Onto chapter 8; in 8.1 the language ED is introduced which extends E with function definition and application but no lambdas. It’s kind of a funny extension, I think it is intended to introduce some concepts rather than be useful in its own right. We spent some time going through the different judgements and equations,and then wrote out an example of how to write a function of two arguments in this language.

In 8.2 we meet EF a more fleshed out extension to E, which promotes functions to first class citizens, i.e. lambdas. We walked through the code example for function k which I personally found quite helpful and then took a look at the preservation and progress theorems. Dann pointed out that preservation is proved by using the dynamics of the language while progress is proved using the statics; the why of this remained unclear to me though Ben had some ideas.

Section 8.3 introduces the concept of definitional equality which on my first reading seemed like a technical detail and I suggested maybe we skip the section, but I am really glad my idea was ignored :). This was perhaps the most interesting part for me once Pete and Ben started discussing the nuances of the definition. I’m going to take a stab at writing down my take away understanding, if it’s wrong let me know and I will edit this.

Definitional equality is a construct introduced in order to identify when different ABTs are in fact equivalent to one another in some potentially useful way to us as language designers. At one end of the spectrum we might say that an ABT is only equivalent to another if every node is equal, but this is too strict since by that reckoning x+1+1 is completely different then x+2. At the other end of the spectrum we might say it only matters what an ABT evaluates to once all free variables have been replaced, but this is too hard to use since often we want to work with trees containing unassigned variables. Definitional equality lands somewhere in the middle and tries to let us make as many equivalencies as possible without compromising the integrity of our language. Though in this aspect it is still a best effort attempt rather than a precise definition. Harper brings up an example showing this in Chapter five, where he shows that commutativity of the nat type can not be proved true in general though it can be shown true for every instance.

We didn’t have too much time for 8.4 but dynamic binding today doesn’t seem nearly attractive as it must once have, though I found it interesting how placing it into the ABT description used in PFPL makes it clear that dynamic binding requires that you give up a lot of the structures we have built up over the last 8 chapters, which hardly seems worthwhile.

Ok that got a bit longer than usual, see you all next week, Scott