On 10/02/2009, at 4:45 AM, Tillmann Rendel wrote:
A Haskell runtime system is a somewhat vaguely specified interpreter for (IO a) values. While it would be nice to a have a better specification of that interpreter, it is not part of the semantics of the language Haskell.
While not "official", there is always "Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell" by Simon Peyton Jones. https://research.microsoft.com/en-us/um/people/simonpj/papers/marktoberdorf/ Another nice aspect of that paper is that it discusses some of the difficulties in coming up with a denotation for values of type IO a, see particularly section 3.1. It suggests a set of event traces as a possible way forward: type IO a = (a, Set Trace) type Trace = [Event] data Event = PutChar Char | GetChar Char | ... (Incidentally, this view is quite useful in a declarative debugger, which emphasises the denotational semantics of a program.) In the end the paper goes for an operational semantics, on the grounds that the author finds it "simpler and easier to understand". Cheers, Bernie.