Yang wrote:
Furthermore, is there any way to embed this information [about async execptions] in the type system, so that Haskellers don't produce async-exception-unaware code? (Effectively, introducing checked interrupts?)
Yes, it is possible to make the information about exceptions and interrupts a part of operation's type: http://www.haskell.org/pipermail/haskell/2004-June/014271.html Here is a simple illustration for your specific case
{-# OPTIONS -fglasgow-exts #-}
module B where import Control.Exception
idarn _ msg = error msg
myPutStrLn _ | False = idarn ?e_async "myPutStrLn is interruptible" myPutStrLn x = putStrLn x
*B> :t myPutStrLn myPutStrLn :: (?e_async::()) => String -> IO () Now it is obvious that myPutStrLn is subject to async interruptions
test1 x = do myPutStrLn "String" myPutStrLn x
*B> :t test1 test1 :: (?e_async::()) => String -> IO () and so can test1. The compiler figured that out.
myblock :: ((?e_async::()) => IO a) -> IO a myblock x = let ?e_async = undefined -- meaning, we `handle' the exc in block x
If we try to *B> test1 "here" <interactive>:1:0: Unbound implicit parameter (?e_async::()) arising from use of `test1' at <interactive>:1:0-11 In the expression: test1 "here" In the definition of `it': it = test1 "here" meaning that we ought to `handle' that exceptional condition. The typechecker will not let us overlook the test.
-- ?e_async::t causes a problem: we really have to `handle' it -- main = test1 "here"
test3 = myblock (test1 "here")
*B> :t test3 test3 :: IO () The type of test3 shows that the condition is `handled'. And so test3 may now be run.
(Something like this is straightforward to build if I abandon Concurrent Haskell and use cooperative threading, and if the operations I wanted to perform could be done asynchronously.) All operations could be done asynchronously, at least on Linux and many Unixes:
http://www.usenix.org/events/usenix04/tech/general/full_papers/elmeleegy/elm...
(Something like this is straightforward to build if I abandon Concurrent Haskell and use cooperative threading, and if the operations I wanted to perform could be done asynchronously.)
From the abstract: ``Although threads seem to be a small step from sequential computation, in fact, they represent a huge step. They discard the most essential and appealing properties of sequential computation: understandability,
That seems as a very good idea. You might be aware that well-respected and well-experienced systems researchers call for *abandoning* threads. Threads are just a very bad model. The Problem with Threads Edward A. Lee http://www.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-1.html Also, IEEE computer, May 2006, pp. 33-42. predictability, and determinism. Threads, as a model of computation, are wildly nondeterministic, and the job of the programmer becomes one of pruning that nondeterminism. Although many research techniques improve the model by offering more effective pruning, I argue that this is approaching the problem backwards. Rather than pruning nondeterminism, we should build from essentially deterministic, composable components. Nondeterminism should be explicitly and judiciously introduced where needed, rather than removed where not needed. The consequences of this principle are profound. I argue for the development of concurrent coordination languages based on sound, composable formalisms. I believe that such languages will yield much more reliable, and more concurrent programs.'' I believe that delimited continuations is a good way to build coordination languages, because delimited continuations let us build a sound model of computation's interaction with its context.