Skip to content

Types and Programming Languages Chapter 14 Exceptions

Jump to bottom Edit New page
Paul Mucur edited this page Aug 10, 2017 · 13 revisions

Table of Contents

Tom's update

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.

[…]

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

Preamble

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.

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"

Or JavaScript's throw:

throw 'Something went awry!';

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 error evaluates to error, 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 error also evaluates to error, 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 neither of which we have covered yet), 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)

Interestingly, the introduction of this new, non-value error term means that we have to refine our definition of progress:

Suppose t is a closed, well-typed normal form. Then either t is a value or t = error.

We discussed how this wording was unlike our previous definition (with meaning packed into the use of the phrase "normal form") but could be translated like so:

If a closed term t is well-typed, then either it can be evaluated, is a value or is error.

Suitably well-typed, we marched onto the next new feature of our language: exception handlers.

We introduced another brand new bit of syntax:

t ::= …
      try t with t

This is reminiscent of the familiar try catch from languages such as JavaScript and PHP:

try {
  // ...
} catch {
  echo 'Jings crivens, help me boab!';
}

With it came some new evaluation rules:

try v1 with t2 ⟶ v1 (E-TryV)

This first rule shows that if we evaluate a term until the "body" of the try is a value, the next step of evaluation is to use that same value and discard the exception handling part in t2.

try error with t2 ⟶ t2

On the flip side, if the body of the try evaluates to an error, we should return the handler t2.

Finally, we need a congruence rule:

            t1 ⟶ t1'
----------------------------------
try t1 with t2 ⟶ try t1' with t2

This shows that if the body of the try can be evaluated (t1 ⟶ t1') then we do that a single step.

This intuitively matches how you'd expect exception handlers to work: evaluate the body and, if it raises an exception, fire the handler, otherwise return the successful result of the body.

We also have a new (but not unfamiliar) typing rule for try:

Γ ⊢ t1 : T  Γ ⊢ t2 : T
-----------------------
Γ ⊢ try t1 with t2 : T

This shows that try t1 with t2 has a type T if both the body t1 and the handler t2 return the same type T (not dissimilar to how we type-check if).

Finally, we raced through the last new feature: the ability to raise an exception with some value using raise.

t ::= …
      raise t
      try t with t

This replaces error with raise t which allows us to pass some term t when we signal an exception.

The evaluation rules match those we saw for error:

(raise v11) t2 ⟶ raise v11 (E-AppRaise1)
v1 (raise v21) ⟶ raise v21 (E-AppRaise2)

With an added congruence rule for evaluating the term of a raise:

      t1 ⟶ t1'
----------------------
raise t1 ⟶ raise t1'

And a rule to handle exceptions raised when evaluating the term passed to another exception:

raise (raise v11) ⟶ raise v11

We also restate the rules of try to accommodate raise:

try v1 with t2 ⟶ v1

            t1 ⟶ t1'
----------------------------------
try t1 with t2 ⟶ try t1' with t2

We also explain what happens to the term passed to raise:

try raise v11 with t2 ⟶ t2 v11

Namely, that the handler t2 is called with it! This means that the handler t2 should be some sort of function which leads us neatly onto the typing rules:

  Γ ⊢ t1 : Texn
-----------------
Γ ⊢ raise t1 : T

This is similar to the error rule we saw previously in that raise t1 has any type T but it also states that the term passed to raise should be some predefined type Texn. This may well be a Nat (e.g. if you want to use numeric error codes) or perhaps some Exception type but again this all seemed like a tease for subtyping.

Γ ⊢ t1 : T  Γ ⊢ t2 : Texn → T
------------------------------
   Γ ⊢ try t1 with t2 : T

Finally, we refined our typing rule for try such that the handler t2 must now be a function of the exception type Texn to the same T as the body t1.

With that, we were done with exceptions!

As we finished a little early, we had chance to discuss some of the topics raised by @tomstuart in his update about how this chapter demonstrates a programming language design decision and its knock-on effect on our type system.

We also remarked on the surprising existence of this very specific sign in the Geckoboard office:

Retrospective

As we had more time than usual, we took the time to reflect on both the meeting and TAPL in general:

  • We were all pleased to have made it this far into the book particularly as it feels like the end of an important first chunk of the material;
  • We were eager to continue to at least cover subtyping both after so much teasing in this chapter and because the dependency graph at the beginning of the book shows it to be critical to so many other topics;
  • We decided to not pause for an interstitial (as we had one recently) but for the next meeting to be about Chapter 15;
  • @mudge volunteered to organise the next meeting;
  • We discussed whether we'd need to split Chapter 15 into more than one meeting as it seems rather lengthy and dense and decided that a few people would research a sensible plan to be announced before the next meeting;
  • We discussed whether, from this point on, we should pay more attention to the aforementioned dependency graph in the book for choosing "interesting" chapters and then bailing on the book once we reach a consensus;
  • We acknowledged the ever-present issue of the club being difficult to join mid-book and decided this continued pressure should be part of our decision every book meeting whether to press on or switch to a new book.

Pub

Thanks

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.

Add a custom footer
Clone this wiki locally