<p>The question you ask has been widely and acrimoniously discussed under the heading "checked exceptions or unchecked exceptions?". Here "checked exceptions" means the Java model where all possible exceptions a method can throw have to be declared explicitly. I think it's mostly agreed that while checked exceptions might seem a good idea when looked at from the point of view of a conventional type-theorist, they are terrible for large scale software engineering, because simple changes to code in one place may trigger changes in the exception interface of vast amounts of seemingly unrelated code. As Neel points out, with modern typing systems (typically extensions of F<sub>&omega;</sub>), more expressive than Java's, some of these problems can be alleviated, although not always without introducing new problems (such as making type-inference harder). This is the main reason why modern, and otherwise strongly typed languages such as Scala and Ocaml don't have checked exceptions. </p>

<p>In my opinion, the last word on this issue has not been spoken, because with increasing use of logic-based specification and verification techniques, it's increasingly useful to let the type-checker infer as many (basic) program properties  as possible. OTOH, most exception usage is simple (when something goes wrong, throw an exception, and catch it in the outermost loop, printing "sorry, please restart" or some variant thereof), using unchecked exceptions is not that big a software engineering problem in practise.</p>

CC BY-SA 3.0
2011-07-27T13:37:08.370Z
Java has both checked and unchecked exceptions. But, yes, most people use the checked ones and regard the latter as "bad style."
Radu GRIGore
CC BY-SA 3.0
2011-07-28T11:25:07.470Z
Radu, I agree. Java's exception model is a mess. Unchecked exceptions in Java "represent conditions that, generally speaking, reflect errors in your program's logic and cannot be reasonably recovered from at run time." Examples are OutOfMemoryError exceptions. It is debatable whether such exceptions can really be avoided. Java's exceptions were developed before their large-scale software engineering properties were understood. Now we know better.
Martin Berger
CC BY-SA 3.0
2011-07-28T11:53:27.333Z
I meant that one can declare *new* exceptions to be unchecked and throw them without advertising the possibility in the type. There's nothing in the language preventing one from doing so. What you quote is a guideline, not a constraint. Just to be clear, I am merely pointing out it is *possible*, without passing any judgement on whether it is good or bad. The reason I commented is that your answers says "[in] Java [...] all possible exceptions a method can throw have to be declared explicitly," which is false. I am nitpicking.
Radu GRIGore
CC BY-SA 3.0
2011-07-28T12:15:21.293Z
Radu, yes, [you are right](http://java.sun.com/docs/books/jls/third_edition/html/exceptions.html#44278), exceptions that are subtypes of unchecked exceptions classes don't need to show up in the exception specification. I have not programmed in Java for a long time, I had forgotten this detail. Thanks for correcting me.
Martin Berger
CC BY-SA 3.0
2011-07-27T10:23:17.587Z
2011-07-28T11:21:48.190Z
2011-07-28T11:21:48.190Z
Martin Berger
<p>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:</p>

<ol>
<li><p>The types that programmers have to write become larger.</p></li>
<li><p>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.)</p></li>
</ol>

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

<p>Here is some of the research done in the area:</p>

<ul>
<li><a href="http://www.google.com/url?sa=t&amp;source=web&amp;cd=5&amp;ved=0CDQQFjAE&amp;url=http://portal.acm.org/ft_gateway.cfm?id=349230&amp;type=pdf&amp;ei=MQMsTvKiFcmaOrWohIwO&amp;usg=AFQjCNEHl8D0lKUMjgEkU10gAi7zpaGZKQ&amp;sig2=6E4_vDAGsru3LGfD4tBXlg" rel="nofollow">Type-based analysis of Uncaught Exceptions</a> by Xavier Leroy and Francois Pessaux</li>
<li><a href="http://ewce.fmf.uni-lj.si/wp-content/uploads/2011/04/ewce-filinski.pdf" rel="nofollow">Monadic effects</a> by Andrzej Filinski</li>
<li><a href="http://arxiv.org/pdf/0907.2059" rel="nofollow">A type system for call-by-name exceptions</a> by Sylvain Lebresne</li>
<li><a href="http://www.ccs.neu.edu/home/tov/pubs/substructural-control/CtlURAL-bw.pdf" rel="nofollow">A theory of substructural types and control</a> by Jesse A. Tov and Riccardo Pucella</li>
</ul>

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

CC BY-SA 3.0
2011-07-24T11:53:31.333Z
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
CC BY-SA 3.0
2011-07-24T12:05:09.923Z
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
CC BY-SA 3.0
2011-07-24T20:37:06.457Z
@Ohad Why don't you write your own answer and earn some upvotes? ;-)
Marc Hamann
CC BY-SA 3.0
2011-07-24T20:39:17.743Z
@marc: I hardly think I deserve them, as Dave's answer is pretty good (modulo the two comments).
Ohad Kammar
CC BY-SA 3.0
2011-07-24T20:48:00.930Z
I replaced the phrase "exception types are contravariant" with two examples illustrating what I meant.
Dave Clarke
CC BY-SA 3.0
2011-07-24T20:57:32.837Z
Cool, thanks! The examples you wrote are true enough, but they equally apply to any subtypes: the return type of any function needs to be general enough to accommodate all possible return types of any subclass. Similarly contravariantly for higher order stuff. I guess what you meant is that allowing exceptions to have subtypes alleviates the problem? The same solutions we could apply to general subtypes are now applicable to exceptions?
Ohad Kammar
CC BY-SA 3.0
2011-07-25T07:35:35.083Z
@Ohad: subtyping isn't strong enough! For higher-order functions to be useful, we need to know that `map pure` is itself pure, and that `map effectful` can raise the same exceptions as `effectful`. If you only had subtyping, `map` would end up with a too-conservative exception spec. (IMO, this is why Java checked exceptions failed: OO is a very higher-order style.) Also, handlers have to be able to mask exceptions too, so types need to quantify over *collections* of exceptions. The relevant keywords to Google for are "row polymorphism" and "Boolean unification".
Neel Krishnaswami
CC BY-SA 3.0
2011-07-25T09:23:14.350Z
@Neel: That's the standard tradeoff between effect-polymorphic systems and subeffecting systems.  If you allow recomputing the effects on     map    for each application, you will be able to type-check all instances of map.  In other words, given a complete program (i.e., closed ground type), you can annotate each sub-term with an effect, and you'll be able to accept all programs. This is **non** -modular, of course.  I have less intuition for effect polymorphism still, but it has its own issues, in particular tractability of effect reconstruction.
Ohad Kammar
CC BY-SA 3.0
2011-07-25T09:32:58.313Z
@Neel: I guess we should also say that this tradeoff mirrors the tradeoff between polymorphism and subtyping.  map can be given a polymorphic type, or instances of map can be typed with subtyping. What I am unsure of is how well we can mirror the HM solution to type inference in polymorphic effects, and I guess that's where your boolean unification reference will come in handy. Thanks!
Ohad Kammar
CC BY-SA 3.0
2011-07-24T11:40:24.250Z
2011-07-28T07:33:24.750Z
2011-07-28T07:33:24.750Z
Dave Clarke
<p>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.</p>

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

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

<pre><code>well-typed_1: environment -&gt; statement -&gt; unit
</code></pre>

<p>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</p>

<pre><code>well-typed_2: environment -&gt; statement -&gt; environment
</code></pre>

<p>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.</p>

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

<p>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)</p>

<pl.programming-languages><type-inference><type-systems>
the type system does not tell the whole story due to "exception"
zell
# the type system does not tell the whole story due to "exception"

(Asked by: username_0 on 2011-07-24)

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)

**Tags:** pl.programming-languages, type-inference, type-systems

---

## 2 answers

### Answer by username_3 on 2011-07-24. Score: 11 | Accepted answer

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:

* [Type-based analysis of Uncaught Exceptions](http://www.google.com/url?sa=t&source=web&cd=5&ved=0CDQQFjAE&url=http://portal.acm.org/ft_gateway.cfm?id=349230&type=pdf&ei=MQMsTvKiFcmaOrWohIwO&usg=AFQjCNEHl8D0lKUMjgEkU10gAi7zpaGZKQ&sig2=6E4_vDAGsru3LGfD4tBXlg) by Xavier Leroy and Francois Pessaux
* [Monadic effects](http://ewce.fmf.uni-lj.si/wp-content/uploads/2011/04/ewce-filinski.pdf) by Andrzej Filinski
* [A type system for call-by-name exceptions](http://arxiv.org/pdf/0907.2059) by Sylvain Lebresne
* [A theory of substructural types and control](http://www.ccs.neu.edu/home/tov/pubs/substructural-control/CtlURAL-bw.pdf) by Jesse A. Tov and Riccardo Pucella

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

> **Comments:**
> **username_4**: 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?  
> **username_4**: 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.  
> **username_5**: @Ohad Why don't you write your own answer and earn some upvotes? ;-)  
> **username_4**: @marc: I hardly think I deserve them, as Dave's answer is pretty good (modulo the two comments).  
> **username_3**: I replaced the phrase "exception types are contravariant" with two examples illustrating what I meant.  
> **username_4**: Cool, thanks! The examples you wrote are true enough, but they equally apply to any subtypes: the return type of any function needs to be general enough to accommodate all possible return types of any subclass. Similarly contravariantly for higher order stuff. I guess what you meant is that allowing exceptions to have subtypes alleviates the problem? The same solutions we could apply to general subtypes are now applicable to exceptions?  
> **username_6**: @Ohad: subtyping isn't strong enough! For higher-order functions to be useful, we need to know that `map pure` is itself pure, and that `map effectful` can raise the same exceptions as `effectful`. If you only had subtyping, `map` would end up with a too-conservative exception spec. (IMO, this is why Java checked exceptions failed: OO is a very higher-order style.) Also, handlers have to be able to mask exceptions too, so types need to quantify over *collections* of exceptions. The relevant keywords to Google for are "row polymorphism" and "Boolean unification".  
> **username_4**: @Neel: That's the standard tradeoff between effect-polymorphic systems and subeffecting systems.  If you allow recomputing the effects on     map    for each application, you will be able to type-check all instances of map.  In other words, given a complete program (i.e., closed ground type), you can annotate each sub-term with an effect, and you'll be able to accept all programs. This is **non** -modular, of course.  I have less intuition for effect polymorphism still, but it has its own issues, in particular tractability of effect reconstruction.  
> **username_4**: @Neel: I guess we should also say that this tradeoff mirrors the tradeoff between polymorphism and subtyping.  map can be given a polymorphic type, or instances of map can be typed with subtyping. What I am unsure of is how well we can mirror the HM solution to type inference in polymorphic effects, and I guess that's where your boolean unification reference will come in handy. Thanks!  

---

### Answer by username_1 on 2011-07-27. Score: 4

The question you ask has been widely and acrimoniously discussed under the heading "checked exceptions or unchecked exceptions?". Here "checked exceptions" means the Java model where all possible exceptions a method can throw have to be declared explicitly. I think it's mostly agreed that while checked exceptions might seem a good idea when looked at from the point of view of a conventional type-theorist, they are terrible for large scale software engineering, because simple changes to code in one place may trigger changes in the exception interface of vast amounts of seemingly unrelated code. As Neel points out, with modern typing systems (typically extensions of Fω), more expressive than Java's, some of these problems can be alleviated, although not always without introducing new problems (such as making type-inference harder). This is the main reason why modern, and otherwise strongly typed languages such as Scala and Ocaml don't have checked exceptions.

In my opinion, the last word on this issue has not been spoken, because with increasing use of logic-based specification and verification techniques, it's increasingly useful to let the type-checker infer as many (basic) program properties as possible. OTOH, most exception usage is simple (when something goes wrong, throw an exception, and catch it in the outermost loop, printing "sorry, please restart" or some variant thereof), using unchecked exceptions is not that big a software engineering problem in practise.

> **Comments:**
> **username_2**: Java has both checked and unchecked exceptions. But, yes, most people use the checked ones and regard the latter as "bad style."  
> **username_1**: Radu, I agree. Java's exception model is a mess. Unchecked exceptions in Java "represent conditions that, generally speaking, reflect errors in your program's logic and cannot be reasonably recovered from at run time." Examples are OutOfMemoryError exceptions. It is debatable whether such exceptions can really be avoided. Java's exceptions were developed before their large-scale software engineering properties were understood. Now we know better.  
> **username_2**: I meant that one can declare *new* exceptions to be unchecked and throw them without advertising the possibility in the type. There's nothing in the language preventing one from doing so. What you quote is a guideline, not a constraint. Just to be clear, I am merely pointing out it is *possible*, without passing any judgement on whether it is good or bad. The reason I commented is that your answers says "[in] Java [...] all possible exceptions a method can throw have to be declared explicitly," which is false. I am nitpicking.  
> **username_1**: Radu, yes, [you are right](http://java.sun.com/docs/books/jls/third_edition/html/exceptions.html#44278), exceptions that are subtypes of unchecked exceptions classes don't need to show up in the exception specification. I have not programmed in Java for a long time, I had forgotten this detail. Thanks for correcting me.  

---

