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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
