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