[Haskell-cafe] The values of infinite lists

[Brian Hulley]

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.

>
> 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? :-)
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...

Regards, Brian.