Brian Hulley wrote:
Therefore I humbly submit a call for authors of books/tutorials on IO to come clean and admit the fact that IO completely changes the language from being purely functional into a functional + process calculus language :-)
As an author of such a book, I'm not willing to do this. Or at least, if we omit concurrency and impure operations such as unsafePerformIO, Haskell is a purely functional, sequential, and deterministic language, whose semantics, including that of IO, can be explained via conventional equational reasoning. I'm sure that it can also be explained via a suitable process calculus, but that is an overkill -- such calculi are best used for describing non-deterministic / concurrent languages. -Paul Brian Hulley wrote:
Robert Dockins wrote:
On Wednesday 10 May 2006 02:49 pm, you wrote:
I could write:
] (r',_) = runIO (mapM print ones) realWorld
and this computation, even though some printing would be observable, still evaluates to bottom, because r' will never be bound.
Humm... how do you define observable? If r' is never bound, how can I observe any intermediate printing?
I meant observable in the sense that the printing is just like a debug trace of evaluation, and so is irrelevant when using the world-state transformer point of view.
[snip] The world-state-transformer idea is nice as a didactic tool, but I don't think its the right world-view for serious thinking about Haskell's semantics.
I thought everything in Haskell is purely functional - surely that is the whole point of using monads? :-)
Sure. But in that world-view then you don't think of the IO actions as "running" at all, so you can't discuss their termination properties. This is more or less what all accounts (at least the ones I've seen) of Haskell's semantics do -- they provide a denotational semantics for the lambda terms basicaly ignore the meaning of IO actions.
I think from the world-state transformer pont of view, all non-terminating computations must be seen as evaluating to _|_, but as you point out, this point of view isn't that useful in practice.
My favorite view of Haskell semantics is of a coroutining abstract machine which alternates between evaluating lambda terms to obtain the terms of a process calculus, and then reducing those process calculus terms; some process calculus reduction rules call into the lambda reduction engine to grow more (process calculus) terms to reduce. The observable behavior of the program is defined in terms of the sequence of reductions undertaken by the process calculus engine.
In this view "bottom" is the denotion of all (lambda) terms which make the lambda portion of the machine fail to terminate, and never return control to the process calculus part -- thus no further observations will be generated by the program.
Thanks for pointing out the process calculi. I found a good page about them at http://en.wikipedia.org/wiki/Process_calculus
It would be good if there was a more detailed description of Haskell semantics along the lines of what you've said above, so that it would be clear that the running of an IO action is something very different from the running of other monads. (Not too mathematical a description but a tutorial style description)
As I understand it, the IO monad shares with other monads the fact that first a composite action is built from primitive actions using >>= and return etc, and this composition is purely functional, even though >>= and return are special built-in functions for the IO monad. (As an aside, I must point out that the word "do" is ultra confusing in this respect, because "do" does not actually run the action, it is just syntactic sugar for composing actions which might be "done" later.)
Then, in contrast to all other monadic actions, which are "run" by simply evaluating something hidden inside them (eg applying a function hidden inside the monad to some initial state), the running of an IO action involves the quite complicated interaction you've described above, and really does go outside the functional realm.
The problem with the RealWorld view of IO, is that it is quite wrong, yet this is the view propounded everywhere, so that anyone who thinks there is something complicated about IO assumes it is because they themselves haven't understood something properly since books/tutorials keep saying how simple and purely functional it all is! ;-)
(Just like in primary school when teachers make out associativity and commutivity of addition/multiplication are trivial thus leading countless would-be mathematicians who immediately see these are complicated but think this is their fault alone, to abandon all hope ;-))
Therefore I humbly submit a call for authors of books/tutorials on IO to come clean and admit the fact that IO completely changes the language from being purely functional into a functional + process calculus language :-)
Best regards, Brian.