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
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
