Types and Programming Languages Chapter 14 Exceptions
Hi Computation Club,
We’re meeting tomorrow night (Tuesday 8th) to discuss chapter 14 of Types and Programming Languages. Please sign up if you’re planning to join us, so we don’t accidentally bring too few or (god forbid) too many snacks.
The meeting is at 6:30pm at Geckoboard's office on the 3rd floor of 60 Worship St, near Liverpool Street, Old Street, Moorgate and Shoreditch High Street stations. The Geckoboard office is above HelloFresh's: to get in, go around to the side entrance on Vandy St (hopefully there'll be a sign directing you) and a worryingly disinterested man on reception should be able to send you up to the 3rd floor in the lift (just mention Geckoboard). If you have any trouble getting in, drop a message in #general on our Slack team or reply to this message and we'll respond as soon as possible.
It’s been a quiet couple of weeks since our last meeting. Some of this is doubtless due to the soporific effect of this dreamy summer that feels like it’ll never end, smothering our minds with its heat and beauty like warm maple syrup poured over a sentient waffle, transporting us to a half-remembered childhood of lemonade, wildflowers, jumpers for goalposts, bark rubbings, fake bokeh, those funny feet ice lollies you remember the ones, etc. But another factor might be that chapter 14 is quite short, relatively straightforward and about exceptions.
Previous chapters have introduced new and exciting types in order to accommodate new and exciting features in the operational semantics; chapter 14 gives us some new syntax and some new typing rules, but doesn’t affect the syntax of types at all. As with mutable references in chapter 13, we may end up spending the majority of the meeting discussing how the syntax and operational semantics give rise to exception-like behaviour in the lambda calculus, and only briefly touch on the typing rules, which are less complicated and thus a little less educational than last time. Still, it’s an interesting demonstration of how we can add a recognisable language feature while maintaining the safety (= progress + preservation) property that we care about so much.
I like this chapter because it continues to illustrate how much of programming language design is about decisions, tradeoffs and judgement. It’s showing us that we can engineer the evaluation behaviour we want without sacrificing runtime properties we care about (i.e. determinism), but that as a consequence we have to abandon some other important properties (i.e. uniqueness of types) to accommodate this in the type system, and therefore have to do some patching up elsewhere (i.e. redefine progress) to make everything hold together. This interplay between the different parts of the language is incredibly common and strongly informs the way that language designers choose and combine features in the presence of some kind of static type system. It’s cool that we’re getting a feel for that engineering process with such a simple language and in such a superficially mathematical context.
Also! This is the last chapter in part II of the book! What are we going to do after this? Do we barrel straight into 130 pages of subtyping, or take a break and do something else, or call time on the whole adventure? I will TRY to RAISE this tomorrow.
Looking forward to seeing you there.
Cheers,
-Tom
TBC
TBC
TBC
TBC
Thanks to Leo and Geckoboard for hosting and providing beverages (both soft and not), Chris for organising the meeting, all those that brought bread, snacks and dips and to Tom for leading the meeting.