[Haskell-cafe] The values of infinite lists

[Brian Hulley]

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.