[Haskell-cafe] Monad explanation

[Bernie Pope]

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.