Even Safer Exceptions

[odersky]

Safer exceptions uses capabilities to express possible throws of checked exceptions. It is currently not completely safe since the capability to throw an exception can escape the scope where it is valid. Example:

def f(x: Int): Int throws E
val xs: List[Int]
try
  xs.iterator.map(f)
catch case ex: E => Nil

This is unsafe since the exception might be thrown only after the try has exited. So the thrown exception might not be caught.

With capture checking we now have a means to detect cases like this, so we can move safer exceptions to the next stage.

The goals of this project are:

• eliminate shortcomings for existing safer exceptions. For instance, we should detect exceptions thrown in Java code.
• combine safe exceptions with capture checking in the research branch cc-experiment.
• develop a range of test cases to demonstrate that the checking works and that unsafe code is rejected.
• maybe port (parts of) an existing application or library to checked exceptions.

The project is for someone who likes working with bleeding edge research prototypes and to push the envelope of what we can do with them. The project could have wider impact as a publishable case study of what we can do with capture checking, and how this approach solves Java's problems with checked exceptions by supporting effect polymorphism better.

[mbovel]

@hamzaremmal will work on this next semester.