[Haskell-cafe] The values of infinite lists

[Claus Reinke]

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

> 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.

> 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.
 
> 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.

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.

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.

cheers,
claus