Exceptions are shared secrets


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.

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.

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.

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.

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.

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.

Update: Reworked last paragraph to clarify the point I am making; the previous formulation appears to have invited misinterpretation.

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.

About these ads

35 Responses to Exceptions are shared secrets

  1. It seems you’re making a switcheroo halfway through the post: First you say it’s important that an exception can’t be intercepted, then you downgrade to that it’s important that the exception can’t be deciphered by illegitimate handlers, and that it’s perfectly OK for an exception to be intercepted. I’d say wildcard handlers are plenty sufficient for breaking compositionality.

    • I’m merely separating separable issues, and careful to point out the distinction between the positive requirement to reach the intended handler versus the non-negative condition of not reaching an unintended handler. The dishonest thing would have been to neglect or hide it, rather than point it out, so I don’t see why you would imply the opposite.

      Wildcard handlers preclude the positive condition, but they are not the only reason. An exception-valued variable does the same. I don’t see how you avoid the problem, though, because one can pass exceptions within exceptions, and must therefore admit variables ranging over exceptions. This is why I stressed the non-negative condition.

    • I did not mean to imply that you neglected or hid anything, merely that I don’t follow your argument. I agree with the reasoning in your comment, so it seems the conclusion is that wildcard handlers break compositionality. Once that is lost, I don’t understand why “not reaching an unintended handler” still buys you much.

      I’d characterize exceptions differently: Exceptions form a communication protocol. For this, the “shared” is much more important than the “secret”. I don’t find a compelling rationale for the “secret” either in your post or in the Book.

    • (A “switcheroo” is a swindle.)

      The reason for secrecy is compositionality. Say I’m a higher order function. I don’t want to accidentally intercept an exception from the function I call just because I happen to use the same name as one used by the (black box) called function. Hence the need for secrecy.

    • Sorry about “switcheroo”: My knowledge of the semantics of that word is mostly from Gödel, Escher, Bach (and Wikipedia).

      I agree that compositionality would be nice: But the problem is that the wildcard handlers already destroy the compositionality – or at least those aspects of it I care about. It just doesn’t seem that what’s left is important enough to focus on the secrecy.

      Moreover, more often than not, at least in my code, exceptions aren’t a communication channel between two places in the code that share a binding, but rather a broadcast from one place in the code that ends up in another piece of code that was developed separately and without knowledge of the other. Providing a protocol for communication in that setting is more important than secrecy. Unfortunately, SML’s exceptions make providing a rich, shared protocol pretty difficult.

  2. Ganesh Sittampalam says:

    If you don’t have modules, what’s the difference between dynamic and static classification?

    • It’s simplest if I refer you to PFPL, rather than make a lengthy reply here.

    • Ganesh Sittampalam says:

      I read chapters 28 and 34 before posting, but I still couldn’t see the difference. In particular 28.3 mentions “the initialization of the module generates new classes at run-time that are
      guaranteed to be distinct from all other classes previously or subsequently generated.” – but if you don’t have ML-style modules then what’s the difference between generating all the classes at compile-time?

    • In 28.3 I am using the term “module” loosely; the point has nothing whatsoever to do with “ML-style modules”. Dynamic classification is required to ensure compositionality, so that when a system is composed of modules (in the informal sense) over which you have no control, you will not run into accidental conflicts.

    • Ganesh Sittampalam says:

      Can you give a concrete example? I can see there might be issues with the same module being used twice, but I can’t get from that to a real problem case.

    • If you fix your components once and for all in advance you can get away with one global static declaration of all classes, but as soon as you want to allow components to be added and swapped, you need dynamic classes to ensure there are no conflicts and no need for a global recompile.

  3. unsafePerformIO is so rarely used in real Haskell code that I find Harper’s fascination with it very strange.

    “Benign effects” (those that are pure from the outside) can be put in reusable libraries (e.g: memoization) that use unsafePerformIO once. Also, if they are only about destructive updates, they can be hidden via the (ST s) monad.

    In any case, I don’t find that I have much need for “benign effects” beyond the few already hanled cases in standard libraries.

    Considering purity (or laziness as in other posts) to be a “language defect” is silly. I think it reveals lack of actual use of the language.

    • Try to implement a splay tree as a pure functional mapping. Try to use global state to profile your code. Try to use memoization transparently in pure code. Try to configure your functional program based on a .init file. I could go on.

      In any case the point of my post is not to complain about unsafePerformIO, it is to say that exceptions cannot be done properly without it.

  4. Andrej Bauer says:

    You can decouple dynamic generation from exceptions (and other agebraic effects), they way it is done in Eff with the “new” construct that generates new instances of effects (so SML exception is just a single instance of Eff exception, which takes a (dyamically generated) name as a parameter). This seems more orthogonal to me. Then you can have both, exceptions that can be intercepted but not deciphered, as well as exceptions which cannot even be intercepted. There are cases when the latter are handy, for example if you want to use exceptions to realize Brouwerian continuity principles (but I am sure there are also more worldly cases to be considered).

  5. gasche says:

    I believe it is actually a *good* design choices to design escape hatches out of sound but incomplete type systems (or generally static analysis). Coq programs couldn’t be extracted to ML without a way to unsafely cast what the Coq type system proved to be sound but ML type systems cannot accept.

    I am therefore not fond of criticizing a system because such hatches exist. You want to control their use, have principled ways to ensure they’re not used somewhere, and maybe you can comment on how often they’re used in idiomatic code, etc. But the argument “an escape hatch exists therefore this static control is a bad idea” does not hold.

  6. Ok, I got you — you want new exception types to be generated at runtime.

  7. Could you explain why the usual abstraction mechanism does not suffice here? https://gist.github.com/4202071

  8. Ashley Yakeley says:

    Of course you can have effects (benign or any other kind) in Haskell without a kludge: all you need to do is give them the correct type. That’s what IO is for.

    • You misunderstand the established terminology.

    • Ashley Yakeley says:

      Is there any established understanding of whether an effect is benign?

      In any case, one can always put all effects in IO. Then one is at least no worse off than ML, which also has a type for functions-with-effects.

    • Yes.

      A function of type a -> IO b does not have any effects. Neither does an expression of type IO a.

      There is no way in Haskell to engender an effect without either using unsafePerformIO or the equivalent kludge at top level.

      The way to do this properly is described in PFPL. You don’t want a monad, you want a modality.

    • Ashley Yakeley says:

      I would imagine the notion of “effect” is relative the definition of “function”? All you need to do is consider the type a -> IO b as an “IO-function” from a to b. These IO-functions are perfectly reasonable programming language functions, and they support effects without kludges. Haskell programs use IO-functions extensively, but occasionally one can use “pure-functions” (a -> b) instead. Indeed ML’s notion of “function” seem closer to IO-functions than to pure-functions.

  9. ezyang says:

    This is actually a bit of a problem for Safe Haskell, for which the “attacker” really could be malicious code! But no one in Haskell seems to use exceptions in this manner, so it’s a bit hard to notice on our side.

    But at the same time, why is there no Safe ML? I’ve wondered about this a bit, and it seems one of the biggest obstacles is ML’s lack of purity. But wait, side effects are exactly what we need for dynamic classification. Perhaps the moral of the story here is: not all side effects are created equal…

  10. Ashley Yakeley says:

    When one actually uses the language, the monadic separation of effects in Haskell turns out to be so helpful, one cannot imagine wanting to use a language without it. As for unsafePerformIO, it is available in the GHC distribution but isn’t part of the Haskell standard. Exactly like, hmm, Unsafe.cast in SML/NJ (surely evidence that ML as a language is unsafe?).

    Anyway, you are right about the ugliness of exceptions in Haskell. What is needed is type-witnesses:

    data W a — wrapper around Integer

    data EqT a b where
    refl :: EqT t t

    matchW :: W a -> W b -> Maybe (EqT a b)

    …and a language feature to declare them at top level:

    myWitness :: W Int <- getWitness

    Now we can create an exception type like this:

    data Exn where
    MkExn :: W a -> a -> Exn

    Exn makes a box you can put stuff in of any type, and retrieve only if you have the key (in this case, myWitness). This is how exceptions should have been done in Haskell. Instead, we have the horror of the Typeable class, which attempts to reify types rather than merely provide witnesses to them, and needs special handling because writing instances of it is unsafe.

  11. Ashley Yakeley says:

    When one actually uses the language, the monadic separation of effects in Haskell turns out to be so helpful, one cannot imagine wanting to use a language without it. As for unsafePerformIO, it is available in the GHC distribution but isn’t part of the Haskell standard. Exactly like, hmm, Unsafe.cast in SML/NJ (surely evidence that ML as a language is unsafe?).

    Anyway, you are right about the ugliness of exceptions in Haskell. What is needed is type-witnesses:

    data W a — wrapper around Integer

    data EqT a b where
    refl :: EqT t t

    matchW :: W a -> W b -> Maybe (EqT a b)

    …and a language feature to declare them at top level:

    myWitness :: W Int a -> Exn

    Exn makes a box you can put stuff in of any type, and retrieve only if you have the key (in this case, myWitness). This is how exceptions should have been done in Haskell. Instead, we have the horror of the Typeable class, which attempts to reify types rather than merely provide witnesses to them, and needs special handling because writing instances of it is unsafe.

    • Nope, unlike Haskell, Standard ML is not defined by a compiler, but by a semantics that has been mechanically verified to be safe. Nice try, though!

    • Ashley Yakeley says:

      Haskell’s not defined by the compiler either.

    • I’ve never seen a semantics, and obviously no soundness proofs. A descriptive JFP article does not qualify as a definition; it doesn’t support proof.

      BTW, remember that ML Has Monads too!

    • Ashley Yakeley says:

      That’s true, but you’re changing the subject. The Haskell language does not include unsafePeformIO. So you can’t use unsafePeformIO to criticise Haskell. You can use unsafePeformIO to criticise GHC if you want, just as one can use Unsafe to criticise SML/NJ.

    • No. There are things you cannot do in Haskell, namely benign effects, without the kludge. There are no such things at all in Standard ML—no kludges to work around language design errors.

    • Ashley Yakeley says:

      Of course you can have effects (benign or any other kind) in Haskell without a kludge: all you need to do is give them the correct type. That’s what IO is for.

Leave a Reply

Please log in using one of these methods to post your comment:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

Join 1,424 other followers

%d bloggers like this: