[Haskell-cafe] The values of infinite lists

[Paul Hudak]

Points well taken Claus.  See further comments below.

Claus Reinke wrote:
> Hi Paul,
> 
>> I think that you're asking for a semantics of the entire OS, i.e. the 
>> entire outside world, and for that I agree that something other than 
>> equational reasoning is needed to reason about it.  
> 
> 
> I was about to reply "no, only of the interface between Haskell and the 
> OS",
> but perhaps that comes to nearly the same in the end? at least, I'd like to
> see a simplified "Haskell view of the OS" added to the picture, which seems
> to imply that one needs to take at least one step beyond the "Haskell only"
> picture, into the domain in which different reasoning tools may be more
> appropriate. without having to go into all of the OS, such a step should 
> widen the horizon sufficiently to explain the difference between
> "i/o is purely functional" (wrong, but popular) and "haskell's role in 
> i/o is purely functional, but other roles need to be taken into account 
> to complete the picture" (better).

Yes, I could agree with that point of view.

>> However, I would argue that that is outside the mandate of a book on 
>> Haskell.  But maybe that's the point -- i.e. others feel otherwise.
> 
> I think I do, and obviously (judging from how often this topic reappears)
> Haskell learners find the current presentations confusing. if a Haskell 
> book
> shies away from the topic of i/o, or defers it to some late chapter, 
> beginners
> get the impression that it is more difficult than it should be while 
> advanced
> learners are frustrated by the lack of coverage.
> if a Haskell book shies away from explaining at least the basics of how 
> the interactions with the OS go beyond the functional world, even though 
> the Haskell part of it is still functional, beginners go away with a 
> wrong idea (often repeated as a dogma to other newcomers) and advanced 
> learners struggle with their intuition, which tells them that there must 
> be something else going on. the latter was the case Brian was making, I 
> think.

Well, in defense of such an approach, there are very few (if any?) 
textbooks in ANY language that take a formal approach to defining what 
I/O does.  But your point is still well taken, in that I think that the 
EXPECTATIONS for books on FP to do this are higher because (a) many of 
them take a formal approach to explaining the internal meaning of 
programs, and thus readers expect the same for I/O, and (b) the model of 
I/O that they use (say, monads) is sometimes so different from 
"conventional wisdom" that SOMETHING needs to be said, lest the reader 
be left in the dark!

>> My main point it that if we're reasoning about a single Haskell 
>> program (with no impure features), then the entire world, with all its 
>> non-determinism internal to it, can be modelled as a black box -- i.e. 
>> a function -- that interacts with the single Haskell program in a 
>> completely sequential, deterministic manner.  And for that, equational 
>> reasoning is perfectly adequate.
> 
> I assume you mean the Haskell program interacts deterministically with
> non-deterministic inputs, rather than that the OS interacts 
> deterministically
> with the Haskell program.

Yes.

>> The original Haskell report in fact had an appendix with a semantics 
>> for I/O written as a Haskell program with a single non-deterministic 
>> merge operator.  The reason for the non-deterministic merge was to 
>> account for SEVERAL Haskell programs interacting with the OS, but for 
>> a single program it can go away.  I claim that such a semantics is 
>> still possible for Haskell, and equational reasoning is sufficient to 
>> reason about it.
> 
> non-deterministic merge is necessary there, and beyond the purely
> functional domain. and unless you let all your Haskell programs run in
> the dark, there will always be more than one agent interacting with
> shared resources: that Haskell program, you, OS daemons, etc.

I think that I'm saying something a little stronger, namely that if you 
capture in a black box the entire universe EXCEPT for the one Haskell 
program that you're trying to reason about, then the interactions 
between that black box and the Haskell program can be explained purely 
functionally and deterministically.  That may be an over-simplified view 
of things -- but it's at least one line to draw when deciding "how much" 
about a language's semantics should be explained to the user.

> the merge idea stems from a time when i/o was described in terms of
> infinite streams and their transformations, which turned out to be 
> rather difficult to compose in practice. the transition to step-wise 
> interactions
> and their composition is what makes the process-calculus style more
> natural these days. not to mention that it prepares readers for other
> adventures in these modern times - in fact, future readers may be
> more familiar with process interactions from their other interests, and
> therefore confused by any attempt to avoid these ideas.

Interesting.  One might rewrite your first two sentences as:

"the merge idea stems from a time when i/o was described in terms of 
infinite streams and their transformations, which turned out to be 
rather difficult to compose in practice.  the transition to step-wise 
interactions and their composition is what makes MONADS more natural 
these days."

:-)  Seriously, I think that it would be a useful exercise to write a 
meta-interpreter of Haskell I/O, in Haskell.  That's basically what the 
appendix of the Haskell Report was many years ago, but it used a stream 
model of I/O.  And I think that this is consistent with your final point 
below.

> apart from that, yes, it might be sufficient to write a simplified OS as
> a meta interpreter, with access to resources and other agents, and in 
> control of scheduling. that interpreter would evaluate Haskell code and 
> execute its interactions with the OS. as with the old sorting-office/
> non-deterministic merge, such an artifact would allow the author to
> explain how the non-determinism is needed, but outside the Haskell
> code, and only permitted to influence the Haskell code in strictly 
> controlled ways.

   -Paul