TAPL update 2017-03-13

[Tom Stuart]

Hi Computation Club,

We met last Wednesday to discuss chapter 5 of Types and Programming Languages. Here are some photos and notes.

Our next meeting is on Tuesday 21st March. Please sign up if you intend to come along. Two weeks after that we’ll have a non-TAPL meeting to cleanse our palates.

We’re going to try to continue our rhythm of having a practical, implementation-centric meeting to follow the more theoretical one we just had. Chapters 6 & 7 are about how to implement the untyped lambda calculus from chapter 5, so again we’ll see if we can use some of the meeting time to do some hands-on work in that direction. Maybe we’ll have enough time to fully implement the lambda calculus; maybe we’ll just focus on some interesting part of it. Maybe we’ll all feel a bit funny and have to have a lie down.

A couple of club members have already begun their own implementations:

• @leocassarani’s Haskell implementation
• @jcoglan’s Haskell implementation

As before, I really encourage you to try implementing some or all of chapter 5 if you have the time and the energy. It is the best possible way to navigate a narrow path of understanding through the forest of largely incidental mathematical detail. Hopefully we can have a show & tell, and even more hopefully there will be at least one implementation that isn’t in Haskell.

If you do try to implement it, note that there will be some fiddly bits around how to implement substitution without accidentally capturing variables, so there’s a risk of getting stuck on that even though it’s not particularly interesting. I have two separate tips for dealing with the problem:

1. chapter 6 (which is short) is all about a particular trick for representing lambda calculus expressions without using variable names at all, so read that if you want to remove the problem entirely; or
2. if you only want to implement call-by-value evaluation on closed terms (i.e. no evaluating under lambda abstractions, no free variables), you don’t need to worry about variable capture because there’s no way for it to happen, so you can probably get away with ignoring it. please don’t tell the maths police

Join us in #tapl on Slack if you’d like to talk about any of this, and particularly if you’d some concrete help (or moral/emotional support) with understanding or implementing anything between now and the next meeting. We’re all in this together!

Cheers,

-Tom