[Haskell-cafe] The values of infinite lists

[Paul Hudak]

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