Re: Typed exceptions

[Neel Krishnaswami <address@hidden>]

Anton van Straaten writes:
>
> Sorry, I did mean "exception" (and I *do* know the difference :)
> This also ties into what I mean by "mandatory exception handling".
> Because of the way static typing integrates with exceptions in
> languages like Java and C++ (probably Ada & Eiffel too?), when a
> method declares that it throws an exception, every one of its
> callers has to take more or less explicit steps to handle that.
> Yes, you can just declare methods as "throws Exception" and ignore
> all that, but I'm talking about systems that do try to do the right
> thing, which most systems that reach production have to do.

I'm designing a language even as we speak, and it's this consideration
that led me to leave out Java-style exception declarations. You pretty
much always end up with a "throws Exception" clause. It's not adequate
as program complexity rises -- you need some kind of parametric
polymorphism for it to be sufficiently flexible to be really
useful. Eg, consider the case of the map function. If we leave out
exception declarations altogether, it will have a type like:
 
  map : (List[a], a -> b) -> List[b]

That is, it takes a list of some type a, a mapping function that takes
a's to b's. and returns a list of b. Now, imagine that we want to add
Java style throws clauses. 'map' can potentially throw any exception
that the mapping function can throw, but the most precise Java-style
type you could write would be:

  map : (List[a], a -> b throws Exception) -> List[b] throws Exception

This isn't actually any more informative than if you left out the
throws clause altogether! What we really want is some parametric
polymorphism, like this:

  map : (List[a], a -> b throws x) -> List[b] throws x

where x is the *set* of exceptions that the mapping function could
throw. Now there's some real information here. The compose function
might have a type like

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

where 'x + y' is the union of x and y. I left this kind of stuff out
of Needle, mostly because I have zero experience with polymorphic
effect systems, and the typechecker was hairy enough as is. Matthias
could likely comment further, because IIRC the PLT MrSpidey tool works
using set-based analyses.

-- 
Neel Krishnaswami
neelk@alum.mit.edu