Add support for exceptions in TML programs

[jstolarek]

I implemented support for exceptions. What works:

• Throwing and catching exceptions

• Nested exceptions:

  let n = ref 0 in
  try
    n:=17;;(raise (raise n));;n:=42;;(!n)
  with (x : ref int) => !x

  The innermost exception takes priority, so the above program is equivalent to:

  let n = ref 0 in
  try
    n:=17;;(raise n);;n:=42;;(!n)
  with (x : ref int) => !x

• Type-checking of exceptions. If you say:

  let n = ref 0 in
  try
    (raise (if false then (raise true) else (raise 42))) ;; n:=1 ;; !n
  with (x : int) => !x

  this will be rejected because in the with block expression x inside exception is declared as int but in the then branch of if a bool is thrown.

• Both the try and with blocks are required to have the same type.

What does not work:

• exceptions inside case scrutinee are not supported. Doing this would require writing a type inference algorithm that figures out what type are we matching on without knowing the type of scrutinee.

• Expressions inside uncaught exceptions are not pretty printed. So if I say:

  let n = ref 0 in
  raise n

  This is printed as Uncaught exception: VStoreLoc 0 instead of something more sensible like Uncaught exception: <ref>. I can fix this if we think this is problematic. The reason I didn't do it is that it causes module cycles.

What needs attention:

• typechecking got more complicated because raise can inhabit every type and so we now have an ExnTy that is equal to every other type. Everything seems to be implemented correctly but it is possible that I made a mistake somewhere.

• Implementation of exception catching is tricky as it requires careful manipulation of scope and reference store. It seems to work correctly but yell if you any unexpected behaviours.

See Note [Evaluation of exceptions] for more details

[jamescheney]

Thanks, but I don't think it's necessary (and may not be correct) to try to track the types of thrown exceptions. I will try to explain more clearly what the type system for exceptions should be like in the paper, but you can see what I had in mind here:

http://www.inf.ed.ac.uk/teaching/courses/epl/2016/lectures/lec16.pdf

(I think there is a similar discussion in TAPL but think you have my copy.)

[jstolarek]

I should have made sure we discussed how the type system for exceptions works in ML-like languages.

Yes, I was aware that what I'm implementing is different from presentation in TAPL. The reason I allowed raising arbitrary expressions as exceptions values was that this is what the rules in our paper say. Secondary reason was that we don't really have a proper support for data types and pattern matching. So I would either have to rewrite these parts of the interpreter or come up with some sort of hack to allow defining new values of error data type. Again, something that can be done but will take time.

I'm also nor sure the proposed type system is correct, for example if you call a function in an expression it may raise an exception that has a different type than expected

Sorry, I don't follow. Could you give an example?

[jamescheney]

The reason I allowed raising arbitrary expressions as exceptions values was that this is what the rules in our paper say.

We didn't give typing rules, though. I would suggest that we pick a specific type (say, string) for exceptions for now, since the issue of defining extensible exception types and slicing for general pattern matching is somewhat orthogonal to the control-flow issues of exception handling, which are our focus here.

Sorry, I don't follow. Could you give an example?

Consider "map". It takes a function as an argument. So we can do this:

let foo (f,g) = (map f [1,2,3], map g [1,2,3])
let bar (x) = raise "abc"
in try (foo(bar,\x -> raise 123)) with x -> x + 1

I believe something like this will be well typed according to your rules, because the raise inside "try" raises an int and the handler handles an int. But the actual exception that gets raised will be of type string. The types of f and g do not tell us anything about what kinds of exceptions they (may) raise. Dealing with this correctly would require some kind of effect annotations on the functions/types to characterize what exceptions they might raise (as in Java).

[jstolarek]

We didn't give typing rules, though.

True - I had to come up with an ad-hoc solution. And indeed, your example will derail my type system.

For now I will assume that strings are the only allowed values of exceptions and keep the hack with ExnTy. Fix coming. I'll start separate tickets to track further improvements to the exceptions mechanism.

[jstolarek]

Updated - please review.

[jamescheney]

Thanks, looks fine.