チェック例外の特徴を整理する

Java を勉強していてエキゾチックだと感じるのはやはりチェック例外だ。このチェック例外という仕組みは、便利か邪魔か、ということはひとまず置くとしてやはり非常に興味深いものだと思う。そんな Java のチェック例外を自分なりに理解しやすいように整理・言い換えをしてみた。（これも前回と同様にかなり雑な内容だと思いますがとりあえずあきらめて記事にしてしまいます）

まずメソッドの throws 節に書かれる例外クラスを戻り値の型と比べてみよう。戻り値の型は実際に return される型と不整合があるとコンパイルエラーになる。同様に throws 節の例外クラスと実際にメソッドから投げられうる例外との間に不整合があるとコンパイルエラーになる。

いずれもメソッドのクライアントに対する契約の一部をなしているから、宣言された型より小さい型を実際に返す/投げる分には構わないが逆は不可である。例えば Object m() throws Exception {} は String を返したり IOException を投げたりできるが、String m() throws IOException は Object を返したり Exception を投げたりできない。（なお、この記事では継承関係にあってサブクラスに向かうほど小さい、逆を大きいと呼ぶ。≦と≧に対応する不等号として <: と >: を使う）

また、メソッドがサブクラスでオーバーライドされるとき、オーバーライドするメソッドの throws 節にはオーバーライドされたメソッドの throws 節と同じか、それよりも小さい型を指定しなければならない。例えば throws Exception を throws IOException でオーバーライドできるが、逆は不可である。これは Java1.5 からは戻り値についても同じである (covariant overriding)。逆に言うと例外には昔から covariant overriding があったともいえる。

戻り値とチェック例外の類似点は一応ここまでである。チェック例外は戻り値とは異なり互いに継承関係にない複数の型を指定することができる。

throws IOException, ClassNotFoundException

という宣言は IOException か ClassNotFoundException を投げるかもしれないが、例えば（同様に Exception の直接のサブクラスである）InterruptedException は投げないという約束になる。一方で戻り値の型は1つだけだ。

ちなみに「互いに継承関係にない」と断り書きをつけたのはもし継承関係にあればその大きいほうのクラスに包摂できるからで throws Exception, IOException というのは throws Exception というのと同じことである。

「一応ここまで」と書いたのは、次のように捉えなおすことで例外と戻り値の型とのアナロジーを引き続き維持しようという企みからである。

戻り値の型とは別に、そして例外クラス（とその階層）とも別物として、メソッドの「チェック例外に関する型」（およびその階層）を考える。これを仮に「throws の型」と呼ぶことにする。「throws の型」は単に継承関係にない例外クラスの集合として表現される型である。{IOException, ClassNotFoundException} のように表記することにする。

throws の型は次のような規則で階層をなす。

(1) 2つの throws の型が包含関係にあるとき、部分集合のほうの型のほうが小さい。したがって throws IOException, ClassNotFoundException を throws IOException でオーバーライドできる。

(2) また、throws の型の要素の一部を例外クラス階層においてより小さいものに置き換えるとより小さい型になる。したがって throws IOException, ClassNotFoundException を throws FileNotFoundException, ClassNotFoundException でオーバーライドできる。

例外クラスの階層と throws の型の階層の間の関係をいくつか例をあげて示す。

チェック例外のクラスが A, B, C の3つしかなく、以下の継承関係にあるとき、

throws の型の階層は以下のようになる。

例外の階層が以下だったら、

こうなる。

例外のクラスが A, B, C, D の4つで以下の継承関係にあるとき、

throws の型の階層は以下のようになる。(*)

例外の階層が以下だったら、

こうなる。

これらは全部プログラムで出力しているのできちんと変換方法を定義できるが、大雑把にいうとまず例外クラスをメンバとする全ての集合の包含関係で階層を作り、それを例外クラスの階層に基づいて正規化すると throws の型階層ができる。（TODO: throws の型階層が必ず lattice であることを示したい）

あらゆる throws の型に対して下にくる (bottom) のが空集合からなる型である。つまりどんなメソッドでも throws を書かないメソッドでオーバーライドできる（勿論 final でなければ）。あらゆる throws の型に対して上に来る型 (top) は例外クラスのルート一つだけからなる集合として構成できる（上の例ではすべて {A}）。これは例外クラスがツリー階層をなす（top を持つ）ということからくる効用である。

このように throws の型を定義するとオーバーライドについて先ほどと同じ言い方を維持できる。オーバーライドするメソッドの throws 節にはオーバーライドされたメソッドの throws 節と同じか、それよりも小さい型を指定しなければならない。

話はここで終わりではない。インターフェイスが関与する場合は複数のメソッドをオーバーライドするということがありうるので、それら全ての throws の型に対して下に来るような型でなければならない。さっきの (*) を付けた図でいうと throws C と throws B, D をオーバーライドするメソッドは throws D か例外を投げないメソッドでなければならない。

throws の型の階層では2つの要素から下に辿ったときに最初に出会う地点が1つだけ決まる (meet) ので「この型と同じか、それより小さい型」という風に単一の型を使って表現できる。今の例だと「{D} か、それより小さい型」だ。

次に、throws 節に指定する型はメソッド本体の定義からも制約を受ける。メソッド本体はその実装から「こういう例外を投げうる」ということを求めることができる。Java の仕様書では "possible result" とか "can throw ..." （...は例外クラス）とかいう言葉で表現されているが、やや見通しの悪い書き方になっているので throws の型の観点から再構成してみよう。

メソッドがどんな例外を投げうるかを定式化することを考える。関数型言語などでは式の型は（日本語で書くと）以下のような規則（ML 風文法を想定）を定義して型を推論したり検査したりする。

・式 a が型αで式 b が 型βのとき、式 a; b の型はβ
・式 f が型α→βで式 a が型αのとき、式 (f a) の型はβ
・式 c が型 bool で式 t と式 f がともに型αのとき、式 if c then t else f の型はα

このやり方を throws の型に適用すると以下のようになるだろう。なお、以下でα∨βは「αとβから上に辿っていって最初に出会うところ」(join) を意味するものとする（throws の型については「和集合をとって正規化」にだいたい対応）。

・文 a が型αで文 b が型βのとき、ブロック {a; b} の型はα∨β
・式 a が型αでメソッド b が型βで式 C が型γのとき、式 a.b(c) の型はα∨β∨γ
・式 a が型αでブロック b が型βでブロック C が型γのとき、文 if (a) {b} else {c} の型はα∨β∨γ
などなど。

以上から throws の型の特徴として次のようなことが観察できる。先ほどの ML 風文法のための規則は式の組み合わせ方について型の制約を追加で課していた。これに対して throws の型は統語的な組み合わせにはまったく影響を与えない。

たったいま述べた観察に対する唯一の例外は try/catch である。（finally と catch 節複数の場合は省略）

・ブロック a が型αでブロック b が型βのとき、文 try {a} catch (E id) {b} の型は γ∨β。ただしγは{E}>:αのとき{}、それ以外のときγ∨{E}={E}∨αとなるような最小の型で、γ=αとなるときエラー

「ただし」以降は結構考えた末にこうなったけどまだ考慮漏れがあるかもしれない。「γ=αとなるときエラー」が「投げられるはずがない例外をキャッチしてはいけない」に対応している。[2008-10-28追記]もうちょっと良く考えてみると{E}>:αのとき「γ∨{E}={E}∨αとなるような最小のγ」は「γ∨{E}={E}となる最小のγ」で {} だ。だから場合わけは不要だった。こうなってみるとこの定義は Java の仕様書よりもずっといい感じだ。

こうした規則に基づいてメソッド本体の throws の型（「こういう例外を投げうる」）が求まる。メソッドの throws 節にはこうして求まった型と同じかそれより大きい型を書かなければならない。

というわけで「throws の型」という概念を導入したことによりメソッドの throws 節に書くことが許される型 T について、

「T は U 以下で L 以上のものである（ただし U はオーバーライドされる型全ての meet で、L はメソッド本体の型）」

という言い方で述べることができるようになった。

さて、throws 節に書いていい型の範囲はわかった。ところで実際にメソッドのオーバーライドをして、そのメソッド本体の throws の型がオーバーライドされるメソッドの型より小さいとき、どちらを選択する（まあ中間という選択肢はないだろうから）のが慣習として好ましいのだろう。

例えば void m() throws Exception というメソッドをオーバーライドして、メソッド本体は実際には FileNotFoundException しか投げえない場合、オーバーライドする側のメソッドには throws FileNotFoundException と書くべきだろうか、それとも throws Exception と書くべきだろうか。

サブクラスを利用するクライアントに対してより informative なのは前者のほうである。しかしこのクラスをさらに継承する側の実装者に対してより高い自由度を与えるのは後者である。こういうケースには定説があるのだろうか（例えば Effective Java みたいな本に書いてあるとか）。