[Haskell-cafe] The values of infinite lists
claus.reinke at talk21.com
Wed May 24 19:07:08 EDT 2006
Thanks a lot for your positive reply, Paul. we seem to agree on most
points, or at least understand our different preferences, but there is one
remaining point I'd like to clear up.
> 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!
I would agree with (a), although an informal, unambiguous explanation
might also do, and (b) has been the topic of most beginner's i/o questions
and answers on these lists, so that sounds right as well. I would add,
however, that while i/o in Haskell uses the general monadic interface
popular for so many problems, monadic i/o is still different from other
uses of monads in Haskell, and that difference tends to get lost when
the usual explanations focus on issues of monads in general.
let me try to explain what I mean: the usual way of reasoning about
Haskell programs is, as you say, equational, but more than that, the
equations are *context-independent*, ie, they equate programs in
all (valid) contexts. this also works for monads, and still applies to
the monadic aspects of Haskell i/o, but those monadic aspects
*only account for construction of i/o-"scripts" and for some
structural properties required of those scripts*.
in other words, we can use context-free equations to reason about
different ways to construct the same script, and we can use the
context-free monad laws to establish structural equivalences
between syntactically different scripts. but we can not use
context-free equations between Haskell programs to reason
about the execution of those scripts, because the very essence
of i/o (at least how I explained it to myself in that thesis chapter;-)
is interaction with the program's runtime context.
so, if we want to reason about these interactions as well, we need
to take the context into account. as you say, we could do that by
simply enlarging our scope, and define an interpreter for both the
Haskell program and the OS, but that quickly gets complex,
especially once we start taking multiple interacting programs into
account (and how many programs these days aren't interactive
in that sense?).
the alternative is to use *context-dependent* equations, but to
abstract away as much of the context as possible (Felleisen's
evaluation contexts for operational semantics). Haskell's standard
context-free reasoning rules then simply fall out as rules that hold
"for all contexts" and we are back in our old familiar world, but
we can now use the very same reasoning framework to talk about
interactions as well, and about why an i/o-script "at the top-level"
(result of Main.main) is different from an i/o-script nested
anywhere else in the program.
the difference is that the two have different contexts: only at
the top-level (empty context, or leftmost innermost position in
the top-level >>=-tree) does an i/o-script become directly
accessible to the i/o-loop or OS or meta-interpreter or
whatever we may call it, and with the help of that external entity,
and under external control, it can be said to have access to and
to interact with resources outside the Haskell program text,
inside the runtime context (about which context-free reasoning
can't tell us anything).
> 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.
I don't see how the whole of black box and Haskell program could be
captured purely functionally and deterministically. even if Stoye limited
the necessary extensions to the purely functional world view to just one
non-deterministic merge, only in his sorting office, he needed that extension
of the purely functional world, and once you have a black box with such
a merge in it, you cannot guarantee that the non-determinism won't be
visible at the black box interface (in fact, that would be the whole point
of introducing it in the first place), so even if you don't know anything
else about that black box, you cannot assume that it will be a pure
function. which means, as far as I can see, that even if the Haskell
program is purely functional, the combined system of Haskell program
and black box is not.
you and I may know what you are doing when taking that over-simplified
view of things, but I vaguely remember my struggles with the intricacies
of the various functional i/o systems, and from those memories I claim
that you would not help your readers if you chose not to explain or even
to hide those intricacies. you can always tell the beginner that they can,
for many cases, ignore those details - they will look into it briefly, then go
away happy that they don't need to understand it immediately. but you
do need to help the advanced learners by giving them the option to look
into those details once their intuition develops far enough to want better
[that is just my view of things, naturally, but I remember going through
the library shelves to find books that would suit me, and if I saw any
"skimming over" interesting details, I dropped those books faster than
any group of populistic authors could publish them; of course, I had
to go to the original papers in the end, but I did prefer those books
that, instead of hiding advanced material, guided the reader initially
around, and eventually into them:-]
> :-) 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
I wrote my first substantial Haskell program at the time of about
Haskell 1.2, and I agree: that appendix was useful for understanding
Haskell's i/o story at the time (request/response streams, if I recall
correctly; before monads;-).
More information about the Haskell-Cafe