# the type system does not tell the whole story due to “exception”

I am wondering whether it is a bad style to use "exception". For example, in Ocaml, the exception does not appear as the .mli file. So it appears to me that "exception" is something that cannot be tracked by a type system.

So my question in general is, is using exception a bad style because it hides information against the type system?

Concretely, I am trying to implement a type checker for an imperative language, say, Pascal. The essential judgment should have been of this signature,

well-typed_1: environment -> statement -> unit


But this seems to be insufficient because the environment would be modified due to a local variable declaration, thus a more reasonable interface for typechecker would be

well-typed_2: environment -> statement -> environment


An alternative would be use the former one, well-typed_1, dealing with local variables declaration through an exception Var_declaration (e : environment) which returns the updated environment to the type checker for its other recursion.

So, my question for this concrete example is , should I use the well-typed_1 + exception for variable declaration, or well-typed_2?

The disadvantage of well-typed_2 seems to be that, for most statement there are no side effect with regard to environment of types, thus that signature of well-typed_2 seems to be a bit redundant. The disadvantage of well_typed_2 + exception seems to reveal a general issue: the the signature of well-typed_1 in does not tell the whole story. (it does not tell the potential exception)

-

There have been numerous type systems dealing with exceptions and other kinds of computational effect, so the reason it doesn't appear in O'Caml is not that it cannot be done. I think there are two reasons why exceptions do not appear in types:

1. The types that programmers have to write become larger.

2. Exception typing interacts poorly with subtyping and higher-order features, such function types. Ultimately, this is because exception declarations will be an over-approximation of the exceptions that will be thrown, so reusable code needs to have very general exception declarations. For example, the exception declarations for a higher-order function need to be general enough to describe all possible functions passed to the higher-order function. Similarly, the exception declarations on a superclass need to anticipate all possible exceptions that can occur in the subclasses. (Subtyping among exception types alleviates this problem somewhat.)

Java is a good example programming language that has exception typing and these two problems.

Here is some of the research done in the area:

Looking at these papers and chasing the references within will give you more details of what has been done in the field.

-
Can you comment about "exception types are contravariant" please? If $E_1$ is a subclass of $E_2$ and $M$ is a computation that may throw an $E_1$ exception, then $M$ is also a computation that may throw an $E_2$ exception. Of course, if you want to raise an $E_2$ exception inside $M$ you may not do so without changing the exception annotation on $M$, but why is that contravariant? –  Ohad Kammar Jul 24 '11 at 11:53
Also, there's a more general story here: type systems inherently under-approximate program behaviour. Research into type-systems, especially dependent types, pushes the boundary of what can be determined statically and what cannot. However, a language designer may choose not to support state-of-the-art type system features for several reasons which roughly fall under your two categories: It may make the implementation difficult (=mistake prone). It may interact poorly with other language features. It will make the programming experience in the language different. –  Ohad Kammar Jul 24 '11 at 12:05