Haskell Is Exceptionally Unsafe


It is well known that Haskell is not type safe.  The most blatant violation is the all too necessary, but aptly named, unsafePerformIO operation.  You are enjoined not to use this in an unsafe manner, and must be careful to ensure that the encapsulated computation may be executed at any time because of the inherent unpredictability of lazy evaluation.  (The analogous operation in monadic ML, safePerformIO, is safe, because of the value restriction on polymorphism.)  A less blatant violation is that the equational theory of the language with seq is different from the equational theory without it, and the last I knew the GHC compiler was willing to make transformations that are valid only in the absence of this construct.  This too is well known.  A proper reformulation of the equational theory was given by Patricia Johann a few years ago as a step towards solving it.  (If the GHC compiler is no longer unsafe in this respect, it would be good to know.)

I’ve asked around a little bit, including some of the Haskell insiders, whether it is equally well known that the typed exception mechanism in Haskell is unsound.  From what I can tell this seems not to be as well-understood, so let me explain the situation as I see it, and I am sure I will be quickly corrected if I am wrong.  The starting point for me was the realization that in Haskell pure code (outside of the IO monad) may raise an exception, and, importantly for my point, the exceptions are user-defined.  Based on general semantic considerations, it seemed to me that this cannot possibly be sound, and Karl Crary helped me to isolate the source of the problem.

The difficulty is really nothing to do with exceptions per se, but rather with exception values.  (So my point has nothing whatsoever to do with imprecise exceptions.)  It seems to me that the root cause is an all-too-common misunderstanding of the concept of typed exceptions as they occur, for example, in Standard ML.  The mistake is a familiar one, the confusion of types with classes; it arises often in discussions related to oop.  To clarify the situation let me begin with a few remarks exception values in ML, and then move on to the issue at hand.

The first point, which is not particularly relevant to the present discussion, is that exceptions have nothing to do with dynamic binding.  The full details are in my book, so I will only summarize the situation here.  Many seem to have the idea that an exception handler, which typically looks like a sequence of clauses consisting of an exception and an action, amounts to a dynamic binding of each exception to its associated handler.  This is not so.  In fact the left-hand side of an exception clause is a pattern, including a variable (of which a wild card is one example), or nested patterns of exceptions and values.  I realize that one may implement the exception mechanism using a single dynamically bound symbol holding the current exception handler, but this implementation is but one of many possible ones, and does not in any case define the abstraction of exceptions.  Exceptions have no more to do with dynamic binding than does the familiar if-then-else available in any language.

The second point, which is pertinent to this discussion, is that exceptions have only one type.  You read that right: the typed exception mechanism in Standard ML is, in fact, uni-typed (where I have I heard that before?).  It is perfectly true that in Standard ML one may associate a value of any type you like with an exception, and this value may be communicated to the handler of that exception.  But it is perfectly false to say that there are multiple types of exceptions; there is only one, but it has many (in fact, “dynamically many”) classes.  When you declare, say, exception Error of string in Standard ML you are introducing a new class of type string->exn, so that Error s is an exception value of type exn carrying a string.  An exception handler associates to a computation of type α a function of type exn->α that handles any exceptions thrown by that computation.  To propagate uncaught exceptions, the handler is  implicitly post-composed with the handler fn x => raise x.  Pattern matching recovers the type of the associated value in the branch that handles a particular exception.  So, for example, a handler of the form Error x => exp propagates the fact that x has type string into the expression exp, and similarly for any other exception carrying any other type.  (Incidentally, another perfectly good handler is Error “abcdef” => exp, which handles only an Error exception with associated value “abcdef”, and no other.  This debunks the dynamic binding interpretation mentioned earlier.)

The third point is that exception classes are dynamically generated in the sense that each evaluation of an exception declaration generates a fresh exception.  This is absolutely essential for modularity, and is extremely useful for a wide variety of other purposes, including managing information flow security within a program. (See Chapter 34 of my book for a fuller discussion.)  O’Caml attempted to impose a static form of exceptions, but it is now recognized that this does not work properly in the presence of functors or separate compilation.  This means that exception declarations are inherently stateful and cannot be regarded as pure.

This got me to wondering how Haskell could get away with user-defined typed exceptions in “pure” code.  The answer seems to be “it can’t”, as the following example illustrates:

import Control.Exception

import Data.Typeable

newtype Foo = Foo (() -> IO ())

{- set Foo’s TypeRep to be the same as ErrorCall’s -}

instance Typeable Foo where

  typeOf _ = typeOf (undefined :: ErrorCall)

instance Show Foo where  show _ = “”

instance Exception Foo

main = Control.Exception.catch (error “kaboom”) (\ (Foo f) -> f ())

If you run this code in GHC, you get “internal error: stg_ap_v_ret”, which amounts to “going wrong.”  The use of exceptions is really incidental, except insofar as it forces the use of the class Typeable, which is exploited here.

How are we to understand this unsoundness?  My own diagnosis is that typed exceptions are mis-implemented in Haskell using types, rather than classes.  There is no need in ML for any form of type casting to implement exceptions, because there is exactly one type of exception values, albeit one with many classes.  Haskell, on the other hand, tries to have exceptions with different types.  This immediately involves us in type casting, and hilarity ensues.

The problem appears to be difficult to fix, because to do so would require that exception values be declared within the IO monad, which runs against the design principle (unavoidable, in my opinion) that exceptions are permissible in pure code.  (Exceptions are, according to Aleks Nanevski, co-monadic, not monadic.)  Alternatively, since Haskell lacks modularity, a possible fix is to permit only static exceptions in essentially the style proposed in O’Caml.  This amounts to collecting up the exception declarations on a whole-program basis, and implicitly making a global data declaration that declares all the exception constructors “up front”.  Exception handlers would then work by pattern matching, and all would be well.  Why this is not done already is a mystery to me; the current strategy looks a lot like a kludge once you see the problem with safety.

Insofar as my interpretation of what is going on here is correct, the example once again calls into question the dogma of the separation of Church from state as it is realized in Haskell.  As beguiling as it is, the idea, in its current form, simply does not work.  Dave MacQueen recently described it to me as a “tar baby”, from the Brer Rabbit story: the more you get involved with it, the more entangled you become.

About these ads

51 Responses to Haskell Is Exceptionally Unsafe

  1. hydo says:

    Regarding unsafePerformIO, I just pretend it doesn’t exist and thus never use it. If I find myself thinking about using it, I rethink the problem.

  2. From a strictly theoretical standpoint, you would need to show the compiler exploding *without* using undefined in order to demonstrate unsoundness. It’s really not fair to take a feature that is already *known* to be unsound, compose it with some other features and then use the results to claim that one of those other features is also unsound. I’m not saying your point is invalid, but you haven’t really proven it.

    • undefined is a perfectly good value in Haskell; it’s the point of the call-by-name semantics.

    • undefined is a valid value in the same way that `foo where foo = foo` is a valid value. Which is to say, only if you don’t evaluate it. Getting a value with bottom type and then ascribing a non-bottom type to it is going to be unsound by definition. You started with a contradiction, which you used to prove something. That’s not interesting, because “something” in this case could be anything whatsoever.

  3. reuleaux says:

    Maybe a litte off topic: I just saw, that your book, as announced on amazon.com is going to have 391 pages, whereas in its current version 1.32 on your website http://www.cs.cmu.edu/~rwh/plbook/book.pdf it has 590 pages. Will there be anything substantially missing in the printed/amazon version?

    • That’s news to me. The published version will differ slightly from the online version, but the reduction in length is solely due to the formatting, not to restrictions on the content.

    • reuleaux says:

      OK, thanks for this clarification, and of course for sharing the book.

  4. I thought in Standard ML you could declare an exception within an expression (let exception Foo of int in … end) in which case you don’t even need modules to see the dynamic allocation issue.

    Both languages suck for not reflecting exceptions in types.

  5. Jesse Tov says:

    This argument is exceptionally silly. If feature A depends on a mis-designed feature B, but we know how to repair B such that the fix does not materially harm the utility of feature A, then it’s wrong to argue that feature A is broken due to its dependence on broken feature B.

    It may be that a single, dynamically-extensible exception type is more useful than multiple exception types with typecase—and it would be interesting to read an argument for that position, preferably with some examples—but the unsafety of allowing programmers to write their own (lying) Typeable instances has nothing to do with Haskell’s extensible exceptions per se.

  6. Bob, you must use exceptions a whole lot more than I do. I don’t think I’ve ever defined a new exception in Haskell. I only use exceptions for when things go catastrophically wrong, never as flow control for normal case. The only way you could convince me to use exceptions for flow control would be to make the set of thrown exceptions part of the type.

    • Probably so. Pretty much any signature for any non-trivial abstraction has an exception declaration in it. Each instance generates a new exception. This ensures that linking can always be done without clashes, for even if two exceptions have the same name, they are in fact different. Karl tossed out the Haskell exception mechanism and rolled his own version of the ML one, presumably similar to Edward’s. I can ask him to explain why.

  7. ezyang says:

    Here is how you might have done it “the SML way” in Haskell. Note that defining “global” exception classes requires a call to unsafePerformIO/NOINLINE, since operations on modules at least need to be a commutative monad.

    {-# LANGUAGE ExistentialQuantification, GADTs, DeriveDataTypeable #-}
    
    -- Dynamic classification as described in Chapter 34 of "Practical
    -- Foundations for Programming Languages"
    
    import Prelude hiding (catch)
    import Data.IORef
    import Data.Typeable
    import System.IO.Unsafe
    import qualified Control.Exception as E
    import Unsafe.Coerce
    
    -- The arbiter of unicity of symbol names. Bob suggests probabilistic
    -- methods would be more practical, but I haven't looked up the
    -- cleverness to avoid collisions in that strategy.
    {-# NOINLINE globalTagNo #-}
    globalTagNo :: IORef Int
    globalTagNo = unsafePerformIO (newIORef 0)
    
    -- "Symbols" which don't have values (they're labels) but have types and
    -- can allocated freshly in IO.
    data Sym a = Sym {-# UNPACK #-} !Int
        deriving Show
    
    -- We could have forced lexical scoping using ST-like trick but we'll
    -- play fast and loose for now.  Luckily, GHC will prevent us from
    -- committing the polymorphic reference problem.
    newsym :: IO (Sym a)
    newsym = Sym `fmap` atomicModifyIORef globalTagNo (\n -> (n+1, n))
    
    data Clsfd = forall a. Clsfd (Sym a) a
    
    mkIn :: Sym a -> a -> Clsfd
    mkIn a e = Clsfd a e
    
    -- We can do it without the unsafeCoerce (with an explicit value-level
    -- GADT witness), but this way is much more convenient!
    isIn :: Sym a -> Clsfd -> (a -> r) -> r -> r
    isIn (Sym n') (Clsfd (Sym n) e) f z | n == n'   = f (unsafeCoerce e)
                                        | otherwise = z
    
    -- Dynamic classification is a pretty good way to do exception handling
    
    data Exn = Exn Clsfd
        deriving (Typeable)
    instance Show Exn where
        show _ = "Exn _" -- boo, maybe the existential should posit Show
    instance E.Exception Exn where
    
    throw :: Sym t -> t -> a
    throw a e = E.throw (Exn (mkIn a e))
    
    throwIO :: Sym t -> t -> IO a
    throwIO a e = E.throwIO (Exn (mkIn a e))
    
    catch :: Sym t -> IO a -> (t -> IO a) -> IO a
    catch a m h = E.catch m (\i@(Exn e) -> isIn a e h (E.throwIO i))
    
    data Handler a = Handler (forall t. (Sym t, t -> IO a))
    
    catches :: IO a -> [Handler a] -> IO a
    catches io handlers = io `E.catch` catchesHandler handlers
    
    catchesHandler :: [Handler a] -> Exn -> IO a
    catchesHandler handlers i@(Exn e) = foldr tryHandler (E.throwIO i) handlers
        where tryHandler (Handler (a, h)) res = isIn a e h res
    
    {-
    *Main> :r
    [1 of 1] Compiling Main             ( DynClass.hs, interpreted )
    Ok, modules loaded: Main.
    *Main> x :: Sym Int  y :: Sym Char  z :: Sym Int  catch x (throw x 3) (\(x :: Int) -> print x)
    3
    *Main> catch x (throw y 'a') (\(x :: Int) -> print x)
    *** Exception: Exn _
    *Main> catch x (throw z 3) (\(x :: Int) -> print x)
    *** Exception: Exn _
    -}
    
    • Cool! Why not reboot Haskell exceptions to work this way, and avoid the messiness of Typeable?

      (This is also a good example of a situation where unsafePerformIO is necessary to get something useful done.)

    • ezyang says:

      A few reasons come to mind, though I think the issue here boils down to the classic philosophical difference between Haskell type classes (easy to use but lacking features) and ML module systems (very powerful but harder to use).

      1. You’d need a bit of language support/sugar; much like how SML doesn’t explicitly program with newsym, the direct encoding needs a lot of typing that people don’t like!

      2. At the moment, the language construct in Haskell that has the most module-ish flavor are newtypes (which create a “fresh” type name). This system represents a substantial further step in the direction of module systems (esp. first class ones)

      3. In the absence of dynamic classification, the Haskell system for exceptions is actually a pretty good approximation of the more general system that doesn’t suffer from (1) and (2), and while sealing is very useful for values, I haven’t seen very many systems which take advantage of it for exceptions.

    • 1. ML directly supports newsym, as I previously explained. There’s no difference.
      2. newtypes are single-constructor datatypes, as far as I know, which means static classification, rather than dynamic. Why not use this for exceptions?
      3. I don’t agree. We use dynamic exceptions quite often in ML, that’s why they are there. (O’Caml learned this the harder way.)

    • ezyang says:

      1. It’s not much, but I do think of the fact that I need to put down the syntax for defining a new module as a little bit further from “direct support”. (I’m not sure if I was 100% clear, but the actual point was that some work would be needed to make this something pleasant for Haskell users to use. It’s purely cosmetic, but unfortunately, people care terribly much about this sort of thing.)

      2. In some sense, we can already, since you can define a distinct Exception type class instance for a newtype.

      3. I’d love to hear some examples. My intuition says that these cases arise naturally when you’re programming with modules; so when you go to Haskell and your modules are taken away, you program a bit differently and then you use dynamic exceptions much more rarely. (OCaml is a bit of a red headed stepchild, isn’t it.)

    • Ashley Yakeley says:

      This is essentially open type witnesses. I use Template Haskell to generate witnesses at top level, though of course that’s not Safe Haskell. Ideally it would be a language feature.

    • Ganesh Sittampalam says:

      Isn’t this just as unsafe as Typeable if I fake a Sym value?

    • No, because you can’t fake a sym value.

    • ezyang says:

      (e.g. you wouldn’t export the Sym constructor)

    • Ganesh Sittampalam says:

      With the code above, if x = Sym 1 then I can just write catch x (throw (Sym 1) ‘c’) for example.

      We can avoid it by hiding Sym in a module and not exporting the internals, but the same is true of Typeable.

    • Type casting is inherently unsafe and senseless. Dynamic symbol generation and pattern matching is inherently safe and sensible. That is the point.

    • Ganesh Sittampalam says:

      But ezyang’s code is also based on type casting, which is why it can be broken if the Sym constructor is exposed.

      He mentions an alternative using an type equality witness, so perhaps it’s not essential, but the details of how that’d work aren’t obvious to me.

    • We were talking cross-purposes. I’m referring to a built-in symbol type, you’re referring to ezyang’s hacked up version in Haskell.

  8. orclev says:

    I’m hardly an expert in either Haskell or ML (more of a novice in Haskell, and never done anything in ML), but from what I’ve been able to tell the problem has nothing at all to do with Exceptions and is entirely to do with the fact that Typeable allows you to muck with Haskells understanding of the types involved. I haven’t tested it (mainly because I don’t have GHC available to me at the moment), but I suspect you’d see something similar if you attempt to perform *any* pattern match against a type that lies about its TypeRep in this manner. Once again, I haven’t tested this, but I suspect it would also demonstrate the problem you’ve shown (I’ve omitted the definition of Foo, assume it is the same as the one you provide above):

    main = foo (error “kaboom”)
    foo :: a -> IO ()
    foo e = case e of
    Foo f -> f ()
    _ -> return ()

    • Yes, but my point is that the implementation of typed exceptions in Haskell forces you, without good reason, into having the class Typeable, from which the problems flow. Had exceptions been done properly, as in ML, none of this would’ve arisen. I’d like to understand why exceptions are done in this crazy way in Haskell, or, equivalently, why they were not done properly (it was known technology).

    • daira says:

      This is disallowed, and for the right reason:

      exceptions.hs:11:11:
      Couldn’t match expected type `a’ with actual type `Foo’
      `a’ is a rigid type variable bound by
      the type signature for foo :: a -> IO () at exceptions.hs:9:8
      In the pattern: Foo f
      In a case alternative: Foo f -> f ()
      In the expression:
      case e of {
      Foo f -> f ()
      _ -> return () }

  9. I disagree with many of your ideas but someone who disparage Haskell cannot be that bad…

  10. ezyang says:

    Oh man! I guess I’ll have to take your word for it, since I don’t have a copy of the SML language standard handy. (What’s the syntax for it?)

    Because Haskell permits *static* declaration of constructors in the open sum type, it’s not too difficult to piggy-back dynamic declarations on top of it, though it does require some (unsafely initialized) global state.

    • ezyang says:

      It seems like the piece Standard ML is missing is the “newsym” language feature (utilized on pg. 337 of your book), which lets us dynamically allocate fresh symbols?

    • That is not missing from Standard ML, it is disguised in the “exception X of tau” syntax. People have consistently misunderstood this concept in Standard ML. The things called exceptions in ML are really classes of type exn, and have nothing to do with exceptions as a control mechanism. This is all explained in PFPL, btw.

    • ezyang says:

      Ah, sure, that plus first class modules (which SML has and OCaml only got recently) is enough, sure. It sure is wordy though!

    • Ashley Yakeley says:

      The problem Typeable & Dynamic are trying to solve in Haskell is this: define a type A such that for any type B one can define functions “up :: B -> A” and “down :: A -> Maybe B” such that “down . up = Just”.

      Is it true that “exn” is ML’s solution to this? It’s certainly an unusual choice of name, if so. (Sorry, I haven’t read PFPL yet.)

    • Yes, you could say that every type is a retract of exn. I won’t argue about the name. The Haskell approach is conceptually whack; it relies on secret name mangling to hopefully make a type comparison properly, but this is not necessary at all, and in fact the ML approach is far more flexible and useful.

      In PFPL I describe (the equivalent of) exn as supporting “secret sharing”. The idea in the case of exceptions is that the raiser and the handler wish to share a secret in the sense that the raiser wishes to communicate only with those handlers that know the secret, which is the name of the exception class. No other handler can intervene. This is critically important to getting good composition properties, which is why the issue is connected with modularity in an indirect way. This also explains why it is impossible even in principle to put “raises” information into types: you often are not even able to name the exception that is raised, because it is a secret (out of scope). This is a good thing, pace Greg.

    • neelkrishnaswami says:

      I don’t understand what you mean when you say it is impossible even in principle to put raises information into types. As long as you have the ability to handle exceptions parametrically, all seems well to me. E.g., if you type exceptions using something like row polymorphism, then you can type map as something like

      forall a, b : type, r : row. (a -> b raises r) -> list a -> list b raises r

      (Here I write “a raises r” as a monadic type for computations of type a that can raise an exception in the row r.)

      Quantifying over unnamed exceptions lets you define map operations that are indifferent to the specific choice of tags. This remains true even with dynamic generation of tag names — map will work even when you use tags that did not exist when it was defined. This gets you the composition property you describe above, since client code must be parametric in all the exceptions it doesn’t know by name.

    • Which will be basically all of them. Plus you have to have a calculus of rows to handle handlers. It’s a mess, I think.

    • Putting it another way, what you’re interested in is the case where you can show that an expression raises nothing. But this will never be possible, because of the dynamic nature of exception classes. You’ll always end up with “it raises whatever it raises”. It’s the negative information that’s interesting, and that’s what you can’t have, it seems to me.

    • Derek Dreyer says:

      I haven’t studied this topic at all, but Blume, Acar and Chae worked out something along the lines of what Neel is suggesting in quite some detail in their APLAS’08 paper: http://people.cs.uchicago.edu/~blume/papers/aplas08-exceptions.pdf

  11. As has been already pointed out, I don’t think you have found a new problem. You have simply used the your own Typeable instance together with exceptions. As far as I can tell, the exceptions are a red herring, it’s really making your own instances of Typeable that is unsafe.

    Note that Haskell-98 doesn’t have any of these holes, since it lacks lots of things, like unsafePerformIO and exception handling. It is precisely to bring back some sanity to Haskell’s unsafety that the Safe Haskell extension was added to GHC.

    • Right, I think I mentioned that. The connection with exceptions is that they force you to have Typeable, because they are done improperly using casts rather than pattern matching against a multi-class type.

  12. User-defined Typeable instances (as opposed to derived ones) are well-known to be unsafe. Try to write your code using Safe Haskell (-XSafe flag with GHC 7.4 or newer).

    • Yes, but my point is that the language doesn’t work, you have to be enjoined not to use it. In this sense C is perfectly safe; just don’t do anything that’s not safe, and you’re golden.

    • schoenfinkel says:

      `{-#LANGUAGE SafeHaskell#-}` is a language.

    • schoenfinkel says:

      `Can’t create hand written instances of Typeable in Safe Haskell! Can only derive them
      Failed, modules loaded: none.`

    • Ashley Yakeley says:

      Safe Haskell is safe, like ML but unlike Haskell. But it also has a type of pure functions, like Haskell but unlike ML. It’s really the best of both worlds. (Though pedantically plain Haskell has a type for pure functions, but not a type of them, because of unsafePeformIO.)

      To reiterate what others have said, Safe Haskell does have Typeable, but in a safe manner. But, Typeable is also ugly, even in Safe Haskell.

  13. ezyang says:

    Disclaimer: This post is written from the perspective of an insider, so I may be missing the point.

    The type-directed nature of exception is fairly well acknowledged; operationally, you can think of the exception handler as having a specified type, which GHC attempts to cast a caught exception to one of these types, rethrowing if the cast fials. (So your example fails because Foo is not *actually* an ErrorCall, and of course if you ask GHC to do the incorrect cast it will crash. Alas, we didn’t add enough warnings to that typeclass because the expectation was that most people would ask GHC to derive it.)

    In practice, this ends up being the same as ML’s dynamically many classes of exceptions, because it is very rare that we actually assert representational equivalence of two exception types. (The case of newtypes is one exception, but most people choose not to erase the type information when they use them with Typeable when they use GHC’s derived instance.) So you “think of” each type as a constructor case, and all is well. I am not 100% clear how the “exceptions are dynamically generated argument” works, so there may still be a modularity hole there.

    • It’s definitely not the same as ML’s dynamic exceptions, because dynamic exceptions are, um, dynamic. What I’m wondering is why they are not done properly as classes, rather than types? One reason is that doing them properly puts exception allocation into the IO monad. But not doing so opens a hole in the type system, because cast is inherently unsafe, and provides only limited functionality compared to the dynamic form.

    • ezyang says:

      Sorry, I’m not as culturally as familiar with ML, so you’re going to have to spell some things out for me.

      My impression was that dynamic classification for exceptions (e.g. as described by chapter 34) was not implemented in any of the currently widely used dialects of ML (neither SML nor OCaml). It is certainly a dynamism that would cannot be encoded *directly* in Haskell; we don’t support runtime declaration of type classes, for one thing! (Which is why I’m confused about the claim that they could be done properly as classes.)

      Still, as you point out, there is no reason we couldn’t build an allocation library in IO, with all of the sealing and encapsulation properties you’d want. (I don’t think anyone has written this library yet, though I am tempted to now.) But there is nothing wrong with me performing this allocation, and then passing it as an argument to the pure computation (much the same way ‘IORef Int -> IORef Int’ is a pure function), which can then throw it, with no trouble. Separate allocation and computation, I say!

    • I affirm that Standard ML does and always has implemented dynamic exceptions properly as such. Why would Haskell not do the same? Your suggestion seems to make sense, but now exceptions are done “wrong” and there is no chance to fix it.

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,014 other followers

%d bloggers like this: