"例外は共有の秘密である"

Exceptions are shared secrets | Existential Type の内容が興味深かったので試訳してみました。

It's quite obvious to me that the treatment of exceptions in Haskell is wrong. Setting aside the example I gave before of an outright unsoundness, exceptions in Haskell are nevertheless done improperly, even if they happen to be sound. One reason is that the current formulation is not stable under seemingly mild extensions to Haskell that one might well want to consider, notably any form of parameterized module or any form of shadowing of exception declarations. For me this is enough to declare the whole thing wrong, but as it happens Haskell is too feeble to allow full counterexamples to be formulated, so one may still claim that what is there now is ok … for now.

私から見て、Haskellにおける例外の取り扱いが誤っているのは全く明らかだ。以前例に挙げたあからさまな不健全性の例はともかく、Haskellにおける例外は、仮にそれが健全に発生したとしても、不適切に処理されている。一つの理由は、現在の定式化は、誰でも思い付きそうなマイルドな拡張に対しても安定でないことだ。パラメタライズされたモジュールや、例外の宣言のシャドウイングについては特に。私からすれば、これだけでも「全てが間違っている」と宣言するには十分だ。しかし、あいにくHaskellは全ての反例を定式化しきれない程度に貧弱なため、「今のところは大丈夫じゃないか」と反論することはそれでも可能だった。……今までは。

But I wish to argue that Haskell exceptions are nevertheless poorly designed, because it misses the crucial point that exception values are shared secrets. Let us distinguish two parties, the raiser of the exception, and the handler of it. The fundamental idea of exceptions is to transfer a value from the raiser to the handler without the possibility of interception by another party. While the language of secrecy seems appropriately evocative, I hasten to add that I am not here concerned with “attackers” or suchlike, but merely with the difficulties of ensuring modular composition of programs from components. In such a setting the “attacker” is yourself, who is not malicious, but who is fallible.

しかし、私はそれでもなおHaskellの例外はまずい設計だと述べておきたい。なぜかといえば、例外の値というのは共有の秘密であるという最も重要な視点が抜けおちているからだ。プログラムを二つの関係者に分けて考えてみよう。例外の発生元と、発生した例外の受け取り先だ。例外の基本原理は、ある値を、他のどんな関係者にも傍受されることなく、例外の発生元から、例外の受け取り先へと転送することだ。秘密というといらぬ刺激をかきたててしまいそうだが、ここで言っておかねばならないのは、私が問題にしているのはいわゆる「攻撃者」のようなものではなく、単に、プログラムを複数のコンポーネントに分けてモジュラーに組み合わせられることを保証することの難しさだ。この場合、「攻撃者」というのはあなた自身だ。悪意はないが、誤りを犯しがちな。

By raising an exception the raiser is “contacting” a handler with a message. The raiser wishes to limit which components of a program may intercept that message. More precisely, the raiser wishes to ensure that only certain previously agreed-upon components may handle that exception, perhaps only one. This property should remain stable under extension to the program or composition with any other component. It should not be possible for an innocent third party to accidentally intercept a message that was not intended for it.

例外を発生させることで、例外の発生元は、何らかのメッセージによって例外の受け取り先と「契約を交わす」。例外の発生元は、そのメッセージを傍受しうるプログラムのコンポーネントをなるべく制限したいと考える。もっと正確にいえば、例外の発生元は、前もって確実に同意したコンポーネントにしか例外を受け取らせたくない。そして、そのコンポーネントはおそらく1つだけだろう。この性質はプログラムを拡張した場合や、ほかのどんなコンポーネントを組み合わせた場合にも安定に保たれるべきだ。善意の第三者が、受け取るはずでなかったメッセージを予期せず受け取ってしまうということがあるべきではない。

Achieving this requires a secrecy mechanism that allows the raiser and the handler(s) to agree upon their cooperation. This is accomplished by dynamic classification, exactly as it is done properly in Standard ML (but not O'Caml). The idea is that the raiser has access to a dynamically generated constructor for exception values, and any handler has access to the corresponding dynamically generated matcher for exception values. This means that the handler, and only the handler, can decode the message sent by the raiser; no other party can do anything with it other than pass it along unexamined. It is “perfectly encrypted” and cannot be deciphered by any unintended component.

これを達成するには、例外の発生元と受け取り先が協力関係に同意するための機密保証の仕組みが必要だ。この仕組みは、dynamic classificationによって正確に達成可能であり、Standard MLでは正しく実装されている(しかしOCamlではそうなっていない)。Dynamic classificationとは、例外の発生元は動的に生成された例外コンストラクタにアクセスでき、例外の受け取り先は、それと対応する動的に生成された例外マッチャにアクセスできるというアイディアだ。これは、例外の受け取り先が、そして受け取り先だけが、発生元が送ったメッセージを復号できるということを意味する。つまり、他の関係者はそれを無検査で通過させることしかできない。このメッセージは「完璧に暗号化され」、受け取ることが意図されていないいかなるコンポーネントによっても復号されることはない。

The usual exception mechanisms, as distinct from exception values, allow for “wild-card handlers”, which means that an exception can be intercepted by a third party. This means that the raiser cannot ensure that the handler actually receives the message, but it can ensure, using dynamic classification, that only a legitimate handler may decipher it. Decades of experience with Standard ML shows that this is a very useful thing indeed, and has application far beyond just the simple example considered here. For full details, see my forthcoming book, for a full discussion of dynamic classification and its role for ensuring integrity and confidentiality in a program. Dynamic classification is not just for “security”, but is rather a good tool for everyday programming.

よくある例外機構は、例外の値は別にして、例外の「ワイルドカード受け取り」を許している。これは、例外が第三者によって横取りされ得ることを意味する。これでは、例外の発生元は例外の受け取り先が確実にメッセージを受信することを保証できないが、dynamic classificationを使えば、正規の受け取り先だけがメッセージの内容を復号できることを保証できる。Standard MLでの長年の経験は、これは実に有用で、ここで考えたようなシンプルな例を遥かに越える応用性があることを示している。詳細については、近々出版予定の私の著書を読んで欲しい。そこでは、dynamic classificationと、それがプログラムにおける一貫性と機密性の保証について果たす役割について詳しく議論している。Dynamic classificationは単に「安全性」のためだけでなく、日々のプログラミングにおける非常によい道具となる。

So why does Haskell not do it this way? Well, I'm not the one to answer that question, but my guess is that doing so conflicts with the monadic separation of effects. To do exceptions properly requires dynamic allocation, and this would force code that is otherwise functional into the IO monad. Alternatively, one would have to use unsafePerformIO --- as in ezyang's implementation --- to “hide” the effects of exception allocation. But this would then be further evidence that the strict monadic separation of effects is untenable.

じゃあ何でHaskellはこの方法を採用しないんだろう？はて、私はこの質問に答える立場にないが、おそらくモナドによる副作用の分離と非常に相性が悪いからではないか、と考えている。例外を正しく扱うには動的なアロケーションが必要で、それが無ければ関数的だったコードを、IOモナドに押し込むことになる。これを避けようとすれば、例外のアロケーションという副作用を「隠蔽」するために、 unsafePerformIO を使わなければならない。 ezyang の実装のように。しかしそうすると、これはモナドによる厳密な副作用の分離は支持できないということの更なる証拠となってしまう。

追記(原文での追記部分)

Update: This account of exceptions also makes clear why the perennial suggestion to put exception-raising information into types makes no sense to me. I will write more about this in a future post, but meanwhile contemplate that a computation may raise an exception that is not even in principle nameable in the type. That is, it is not conservativity that’s at issue, it’s the very idea.

この例外についての議論で、なぜ長年私が、例外発生についての情報を型に記述することに意味がないと述べてきたのかについてもはっきりした。これについては今後の記事でより詳しく述べていくが、同時に、例外を発生させ得る計算が原理的にも型で言い表せないことについても考察していく。(訳注:最後の一文の意味がとれず。)