[Haskell-cafe] The values of infinite lists
brianh at metamilk.com
Thu May 11 07:56:55 EDT 2006
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.
> 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
> 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
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
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.
More information about the Haskell-Cafe