4.11. Exceptions🔗

Mainstream languages use exceptions to signal that an operation cannot complete normally, and to transfer control from the point of failure to the code prepared to handle it. Laurel models this directly: a procedure declares what it may throw with throws, a throw statement raises a value, and try / catch / finally handles it. Modelling exceptions here means each frontend does not have to re-implement them.

Laurel imposes no root exception type, and does not require a thrown value to belong to any particular hierarchy — a procedure may declare throws int and throw 3. What Laurel provides instead is subtype-aware typing of the catch binding, so each frontend uses its own hierarchy directly: Java's Throwable, Python's BaseException, or JavaScript's convention of throwing an Error.

What a throwing procedure promises its callers — which inputs force a throw, and what may change on the way out — is a contract, and is covered under Verification - Continued.

4.11.1. Declaring and throwing🔗

throws T in a procedure's signature says the procedure may finish by throwing a T. In the body, throw e raises e and abandons the rest of the procedure.

composite Exception {}
composite ArithmeticException extends Exception {}

procedure div(a: int, b: int) returns (r: int)
  throws (e: Exception)
  opaque
{
  if b == 0 then {
    var ae: ArithmeticException := new ArithmeticException;
    throw ae
  };
  r := a / b
};

throws is part of the signature — it changes what callers have to deal with — so it sits with returns, before opaque.

4.11.2. Catch or declare🔗

Laurel enforces catch-or-declare, the discipline Java applies to its checked exceptions. A procedure that declares no throws may not let an exception escape, whether thrown directly or propagated from a callee, and a procedure declaring throws T may only let exceptions escape whose type is a subtype of T.

composite ArithError {}
composite ParseError {}

procedure wrongThrows()
  throws (e: ArithError)
  opaque
{
  var e: ParseError := new ParseError;
  throw e
  // error: procedure 'wrongThrows' may throw 'ParseError', which is not a
  // subtype of its declared `throws` type 'ArithError'
};

The check is about the program as you wrote it rather than about how it lowers, so it runs during resolution and reports at the offending throw or call. Whether the source language requires catch-or-declare is a separate question: procedures coming from Python or JavaScript carry a throws clause too, even though neither language has that surface construct.

4.11.3. Handling: try, catch, finally🔗

catch dispatches on a predicate rather than on a type, written catch e when <condition on e>. Type-based dispatch is one such predicate: catch e when e is NotFound. Clauses are ordered and first-match-wins, and a clause with no when guard is a catch-all. finally runs on the way out of the try.

composite Exception {}
composite NotFound extends Exception {}
composite Invalid extends Exception {}

procedure handle(fail: int) returns (r: int)
  opaque
{
  r := 0;
  try {
    if fail == 1 then {
      var e: NotFound := new NotFound;
      throw e
    };
    if fail == 2 then {
      var i: Invalid := new Invalid;
      throw i
    }
  } catch e when e is NotFound {
    r := 1
  } catch e {
    r := 2
  } finally {
    assert r >= 0
  }
};

finally runs after a normal completion, after a caught exception, on the way out with an uncaught one, and when a handler itself throws or returns. A return or an exit that leaves the try runs it too, and nested finally arms chain outward.

One rule decides the rest: if the finally arm itself completes abruptly — it returns, throws, or exits — that completion wins, and whatever was pending is discarded. This is Java's rule (JLS 14.20.2), so try { throw e } finally { return } returns normally and the exception is gone.

4.11.4. The type of a catch binding🔗

A catch binding is typed at the least common ancestor of the exception types that can reach it: the types thrown directly in the try body, and the declared throws types of the procedures the body calls. When those share a common ancestor T, the binding has type T, and reading a field of e needs no downcast.

composite Exception {
  var message: string
}
composite NotFound extends Exception {}
composite Invalid extends Exception {}

procedure logFailure(which: int) returns (out: string)
  opaque
{
  out := "";
  try {
    if which == 1 then {
      var f: NotFound := new NotFound;
      f#message := "missing";
      throw f
    };
    var i: Invalid := new Invalid;
    i#message := "invalid";
    throw i
  } catch e {
    // `NotFound` and `Invalid` join at `Exception`, so `e` is an `Exception` and
    // the inherited field is readable without a cast.
    out := e#message
  }
};

If the types reaching a catch share no common ancestor, Laurel reports an error rather than leaving the binding untyped. If the body throws nothing determinable, no exception can reach the clauses, and they are dropped as unreachable.

A frontend that needs to catch values with no useful common ancestor — unrelated types, or JavaScript's arbitrary thrown values — can box them: wrap the value in a composite field when throwing, and unwrap it in the handler.

4.11.5. Not yet supported🔗

Two shapes are rejected during resolution with a not yet supported diagnostic rather than lowered, because the alternatives would be an internal error or a silent miscompile:

a call to a procedure that throws in a nested expression position. Only a whole statement or a whole assignment right-hand side is handled, so s := f() is fine while s := 1 + f() is rejected;
a catch handler that re-declares its own exception binding, because the substitution that rewrites the binding matches by name and is not scope-aware.