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: paul.hudak@yale.edu New Haven, CT 06520-8285 WWW: www.cs.yale.edu/~hudak