Lambda the Ultimate

The above text has described a pretty complete managed exception model. But there’s one feature that’s conspicuously absent. There’s no way for an API to document the legal set of exceptions that can escape from it. Some languages, like C++, support this feature. Other languages, like Java, mandate it. Of course, you could attach Custom Attributes to your methods to indicate the anticipated exceptions, but the CLR would not enforce this. It would be an opt-in discipline that would be of dubious value without global buy-in and guaranteed enforcement.

This is another of those religious language debates. I don’t want to rehash all the reasons for and against documenting thrown exceptions. I personally don’t believe the discipline is worth it, but I don’t expect to change the minds of any proponents. It doesn’t matter.

What does matter is that disciplines like this must be applied universally to have any value. So we either need to dictate that everyone follow the discipline or we must so weaken it that it is worthless even for proponents of it. And since one of our goals is high productivity, we aren’t going to inflict a discipline on people who don’t believe in it – particularly when that discipline is of debatable value. (It is debatable in the literal sense, since there are many people on both sides of the argument).

Would you consider it uncontroversial for a language in the general spirit of C++/C#/Java to expose exceptions as follows?

- There are two kinds of functions, clearly distinguishable by syntax: imperative functions (which may have side effects and other referentially non-transparent behaviour) and pure functions (referentially transparent).

- Pure functions default to being able to throw no exceptions. To widen the set of exceptions throwable by a pure function, you need to add an extra keyword, like "throws(int,string)", or (in the most general case) "throws(any)".

- Imperative functions default to being able to throw exceptions of all types. To narrow the set of exceptions throwable by an imperative function, you need to add an extra keyword, such as "throws(int,string)" or (in the most narrow case) "throws(none)".

- A type of functions f may only be a subtype of a type of functions g if f throws the a subset of the exceptions of g.

My thinking is that this approach satisfies the largest possible audience, giving you the capability of expressing any possible exception widening/narrowing behaviour, but defaulting to what is typically wanted: pure functions where exception support is narrow and may only be widened explicitly, and imperative functions where exception support is universal and only be narrowed explicitly.

Thoughts?

package mypackage;
class MyException<E> {
    E getCause();
}
class MyApi {
    int someMethod(String foo) throws(MyException<IOException>, MyException<SQLException>) {
        try {
             return baz(bar(foo));
        } catch(SQLException exc) {
             throw new MyException<SQLException>(exc);
        } catch(IOException exc) {
             throw new MyException<IOException>(exc);
        }
    }
}


// client
try {
    new MyApi().someMethod("Hello World!");
} catch (MyException<SQLException> exc) {
    System.out.println("Database error:");
    exc.printStackTrace();
} catch (MyException<Exception> exc) {
    exc.printStackTrace();
}

package mypackage;
union MyException = SQLException | IOException;
class MyApi {
    int someMethod(String foo) throws(MyException) {
         return baz(bar(foo));
    }
}


// client
try {
    new MyApi().someMethod("Hello World!");
} catch (SQLException exc) {
    System.out.println("Database error:");
    exc.printStackTrace();
} catch (MyException exc) {
    exc.printStackTrace();
}

Totally agreed. Type unions especially are an extremely valuable language feature, and aren't too hard to implement. It's amazing how frequently C++/Java/C# programmers create a subclass hierarchy when what they really want to define is a disjoint union, or a type union.

Regarding the distinction between imperative functions and pure functions: programming with local exceptions and local heaps can be done inside a pure function, and the typechecker can assure that no imperative effects can escape out of that pure function. The Haskell State monad provides a good example of how this can be implemented (though there are other ways, and I use an approach that looks more like Pascal/Java/C# syntactically).

The exception handling details are straightforward (i.e. a pure function must be statically provable to catch all possible exceptions its body is capable of throwing before it exits).

The heap details are more complex, and sometimes end up limiting what the compiler can recognize as being locally imperative within a pure function. The most general solution is region typing, but its syntactic overhead is big, so right now I feel OK about accepting the pure/imperative dichotomy and the limitations that go with it.

In general, the set of exceptions throwable by a function, and its heap accessibility (pure or imperative) are things one wants to parameterize over.

For example, you want to be able to write a 'map' function that is pure when its input function is pure, but imperative when its input function is imperative.

This has a nice solution if you embrace the most general subtyping relationship possible (f:a->b <: g:c->d iff b<:d and c<:a and f's set of effects (heap accessibility, set of throwable exceptions) is a subset of g's set of effects. In addition to being able to declare exceptions as "throws(int|string)", you can say "throws(int|f.exceptions)" to say that you can throw integers or any exceptions throwable by f.

Do you think that capability would solve the problems you've pointed out with the pure/impure dichotomy? I haven't run into those myself (yet), but in my work so far I've had somewhat simplistic boundaries between functional and imperative code.

The heap details are more complex, and sometimes end up limiting what the compiler can recognize as being locally imperative within a pure function. The most general solution is region typing, but its syntactic overhead is big, so right now I feel OK about accepting the pure/imperative dichotomy and the limitations that go with it.

In general, the set of exceptions throwable by a function, and its heap accessibility (pure or imperative) are things one wants to parameterize over. For example, you want to be able to write a 'map' function that is pure when its input function is pure, but imperative when its input function is imperative.

In addition to being able to declare exceptions as "throws(int|string)", you can say "throws(int|f.exceptions)" to say that you can throw integers or any exceptions throwable by f.

Do you think that capability would solve the problems you've pointed out with the pure/impure dichotomy? I haven't run into those myself (yet), but in my work so far I've had somewhat simplistic boundaries between functional and imperative code.

fun foo(f : Int -> Int throws a, x Int) {
  try {
    f(x)
  } catch (DivideByZero) {
    0
  }
}

Now you'd want to say foo has type "foo : (Int -> Int throws a, Int) -> Int throws a - {DivideByZero}".

This is nasty because the set difference operation means you don't have any kind of principal typing, and that means that your compiler is going to infer these huge, ugly, unreadable sets for the throws declaration.

No, Needle never had exception declarations. This is because I think you need exception variables to get sufficient precision in the exception typing -- you need to be able to write something like "foo : (Int -> Int throws a, Int) -> Int throws a" so that the information about what the argument can throw doesn't get lost.

o : (b -> c throws x) -> (a -> b throws y) -> (a -> c throws x + y)

Now you'd want to say foo has type "foo : (Int -> Int throws a, Int) -> Int throws a - {DivideByZero}".

This is nasty because the set difference operation means you don't have any kind of principal typing, and that means that your compiler is going to infer these huge, ugly, unreadable sets for the throws declaration.

The lack of such a canonical form is a great big warning sign to the type system designer. It's not a fatal problem, since you can add type declarations (which will presumably be readable!) and check that the inferred type matches the declaration, but it does mean that you've moved up the ladder of complexity, and that perhaps you should rethink the approach.

With your parametric example, after a few methods you'd end up with huge, unwieldy types like

ItDidntWorkException< BoomException< YouReallyDontCareAboutMeException< TheSourceOfAllEvilException > > >

And the union choice would be even worse, as the type would reduce to the recursive union of all exceptions that may be thrown under the method. Use of a union type would just move the list from the throws clause to another location, which does not deal with the problem itself. It is also a step back in that it throws out the chain of exceptions in favour of just propagating the original.

On the other hand I don't see any such problems with the convert and chain idiom. The original causing exception is preserved and can be inspected if desired. Encapsulation is preserved by keeping implementation details from polluting the type interface. The exception explosion is eliminated.

Am I missing something?

what should you do instead? isn't this the appropriate way to scratch that itch in those languages?