I agree with most of your comments Claus. I think that the remaining
difference of opinion is just how much of the I/O semantics one might
expect to see in a textbook on FP (more specifically, Haskell). My
concern is two-fold:
First, to cover ALL of I/O would be an enormous undertaking; at best we
might expect basic operations to be explained, to get the general
principles across.
Second, if explaining I/O means introducing things outside of the normal
formal semantics of a language, then I would get nervous. By "normal
formal semantics" I mean a conventional operational or denotational
semantics, say. By things "outside of the semantics" I mean things
needed to explain an operating system, like non-determinism,
concurrency, etc. If a language already has non-determinism or
concurrency then perhaps I wouldn't be as concerned.
I think that you would like the second point, at least, taken care of,
somehow. I agree that in an ideal world that would be nice, but the
formal semantics of most languages doesn't extend into the OS, so I
wouldn't know where to start. And in any case it also might be a huge
undertaking.
So, in the case of Haskell, my hope is that a suitable description of
the I/O monad in terms of equational reasoning would be adequate to get
the general principles across, if not the finer details. I wouldn't
even object if it had, say, one non-functional feature like a
non-deterministic merge, as long as the intuitions were right. (So,
maybe I need to do that in the next edition of my book :-)
-Paul
Claus Reinke wrote:
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
answers.
[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 below.
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;-).
cheers,
claus
--
Professor Paul Hudak
Department of Computer Science Office: (203) 432-1235
Yale University FAX: (203) 432-0593
P.O. Box 208285 email: [EMAIL PROTECTED]
New Haven, CT 06520-8285 WWW: www.cs.yale.edu/~hudak
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
