[Haskell-cafe] lambda calculus and equational logic

[Peter Gammie]

Ben, comments from the peanut gallery:

On 13/07/2010, at 11:51 PM, Ben Lippmeier wrote:

> What kind of equality do you use for  getChar :: IO Char ?

Surely this is easy: getChar denotes a particular IO action, which is always the same thing (i.e. self-identical and distinct from all other IO actions).

> By "massively complicated" you mean "harder than the simplest case." Haskell's do-notation makes the "state of the world" implicit, and performing the desugaring makes it explicit again -- but then that state isn't really "the state of the word"...

... which tells you that the passing-the-world semantics is not a faithful model of I/O.

In the archives of this list there are many comments on exactly this topic. A couple of quick pointers:

- Wouter Swierstra wrote a paper on this.

http://www.cse.chalmers.se/~wouter/repos/IOSpec/index.html

- Resumptions are a better model:

http://www.haskell.org/pipermail/haskell-cafe/2003-August/004892.html

Intuitively the state monad used by GHC works because it only needs to track dependencies between I/O actions - there is no need for the compiler to impose a total order on everything going on in the world (taken to be all of the context that could influence the execution of the program). For interesting programs it cannot, anyway.

cheers
peter

-- 
http://peteg.org/