Types and Programming Languages Chapter 14 Exceptions
Before the meeting, @tomstuart sent the following update to the club mailing list:
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
We began the meeting with the traditional decanting of babas ganoush and hummus and @tuzz boldly took to slicing up various breads including one containing cranberries brought by @jcoglan which was much remarked upon.
Suitably loaded with carbohydrates, we kicked off discussion of the chapter.
We began by discussing the "big picture" of the chapter: the introduction of a new feature in our language to allow users to signal errors at any point (and later handle them). We (and the chapter) discussed how this is a design choice: we could not introduce errors with new syntax but instead rely on variant/sum types as introduced in Types and Programming Languages Chapter 11 Simple Extensions.
We briefly highlighted examples of "real" programming languages that make similar design choices, e.g. Ruby's raise:
raise "Some error"As opposed to Rust's explicit error handling through a Result type:
let f = File::open("hello.txt");
let mut f = match f {
Ok(file) => file,
Err(e) => return Err(e),
};Satisfied that we were familiar with the general concept of exceptions, we marched on to introduce some new syntax:
t := ...
error
This introduces a new term in our simply-typed Lambda Calculus, error, which is used to signal an error/exception in our program.
The evaluation rules for this new term were as follows:
error t2 -> error (E-AppErr1)
v1 error -> error (E-AppErr2)
This means a few things:
- Trying to evaluate an application where the left-hand side (typically where you'd find an abstraction) is
errorevaluates toerror, discarding the right-hand term; - Trying to evaluate an application where the left-hand side is a value (e.g. an abstraction) and the right-hand side is
erroralso evaluates toerror, discarding the left-hand term.
One subtle thing to note is that error is not a value otherwise it would introduce ambiguity into our evaluation rules.
We decided to work through some examples on the board to firm up our understanding of these rules:
@tomstuart wrote up the following example on the whiteboard and we stepped through its evaluation:
let decrement = λn:Nat . if iszero n then error else pred n
in iszero (decrement 0)
(Note that this chapter builds on the simply-typed Lambda Calculus, not the simple extensions but we felt it was OK to cheat a bit here to make a more interesting example.)
First, we desugared the let:
iszero ((λn:Nat . if iszero n then error else pred n) 0)
Then we began to evaluate the term being applied by evaluating its application:
iszero (if iszero 0 then error else pred 0)
Then we evaluated the condition of the if:
iszero (if true then error else pred 0)
Then, as the condition was true, we could evaluate the if by replacing it with its consequent:
iszero error
And this allowed us to use our new evaluation rule E-AppErr2 (assuming we can treat iszero as a value as it is effectively an abstraction):
error
So far, so straightforward. @mudge tried to jazz this up a bit:
((λx.Nat→Nat . x) (λy:Nat . 0)) error
We first evaluate the left-hand side (as it is not yet a term):
(λy:Nat . 0) error
Then we can apply E-AppErr2 as the left-hand side is now a value (as it is an abstraction):
error
@jcoglan then stepped up to give an example that exercised our other evaluation rule, E-AppErr1:
((λy:Nat . 0) error) ((λy:Nat . y) 0)
Again, we evaluate the left-hand side and find that it matches E-AppErr2:
error ((λy:Nat . y) 0)
This now matches E-AppErr1 as, even though the right-hand side is not yet a value, our evaluation rule tells us to abandon it:
error
Confident in our ability to evaluate errors, we then moved on discussing its rather plain-looking typing rule:
-------------
Γ ⊢ error : T
In order to remain well-typed, we learnt how error can have any type, a concept we haven't yet seen in the book.
For example, type checking the following application:
(λy:Nat . y) error
Would result in error having type Nat.
We discussed alternatives to having error be of any type (the chapter explaining that we could achieve this with subtyping or parametric polymorphism which we haven't yet covered), with @leocassarani proposing that we could have evaluation use information from the type checker to populate an ascription automatically:
The chapter provides an example of a well-typed term using ascription on error that would break the preservation property of our type system:
(λx:Nat . x) ((λy:Nat . 5) (error as Bool))
As this would evaluate in one step to an ill-typed term:
(λx:Nat . x) (error as Bool)
TBC
TBC
Thanks to @leocassarani and Geckoboard for hosting and providing beverages (both soft and not), @tuzz for organising the meeting, all those that brought bread, snacks and dips and to @tomstuart for leading the meeting.