[Haskell-cafe] The values of infinite lists

[Robert Dockins]

On Wednesday 10 May 2006 02:49 pm, you wrote:
> Robert Dockins wrote:
> > On Wednesday 10 May 2006 12:30 pm, Brian Hulley wrote:
> >> Bjorn Lisper wrote:
> >>> Nontermination is not
> >>> the precisely the same as _|_. Only certain kinds of nontermination
> >>> can be modeled by _|_ in a non-strict language.
> >>
> >> What kinds of non-termination are *not* modelled by _|_ in Haskell?
> >
> > Non-termination that is "doing something".
> >
> > For example consider:
> >
> > ] ones = 1 : ones
> >
> > If I try to take its length, I get _|_.  So:
> >
> > ] main = print (length ones)
> >
> > Will churn my CPU forever without producing any output.
> >
> > However, if I print each item sequentially:
> >
> > ] main = mapM print ones
> >
> > I'll get a never-ending stream of '1' on my console.  This is not the
> > same as bottom because it's "doing something".
>
> I can see what you're getting at, but I don't know if I agree with the idea
> that "doing" should affect whether or not one sees the result of the above
> computation as bottom or not. With a hypothetical implementation of
>
>               runIO :: IO a -> RealWorld -> (RealWorld, a)
>
> 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?

More generally, if you want the possibility of implementing 'runIO' as a pure 
function (the world-state-transformer view of Haskell IO), you are forced to 
make a closed-world assumption.

I don't believe that concurrency can be given a nice story in this view;you 
pretty much have to do something ugly like calculate the result of all 
possible interleavings (yuck!).  And your world is still closed.

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.

> > Now, obviously this definition is pretty imprecise, but maybe it
> > helps you get the idea.  Now for the corner cases.  What about:
> >
> > ] main = sequence_ repeat (return ())
> >
> > ?  I'd personally say it is _not_ bottom.  Even though "return ()" is
> > a completely useless action, I'm inclined to say its "doing
> > something" in some theoretical sense (mostly because I think of _|_
> > as being a property of the functional part of Haskell).
>
> 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'd have thought that "doing" is simply a  projection of the purely
> functional "being" into the stream of time and therefore cannot be part of
> the discourse regarding the nature of bottom...

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.

> Regards, Brian.



Rob Dockins