[Haskell-cafe] The values of infinite lists
robdockins at fastmail.fm
Tue May 23 10:54:10 EDT 2006
On May 23, 2006, at 9:50 AM, Paul Hudak wrote:
> Hi Claus --
> 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. 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.
> 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.
> 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.
> If you disagree, then please tell me which features in Haskell (a
> particular I/O command, perhaps?) cannot be modelled as a
> function. I'm not familiar with your thesis, but I note in the
> abstract that you "extend an existing, purely functional language
> with facilities for input/output and modular programming". If
> those extensions cannot be modelled as pure functions, then I would
> agree that a process calculus (say) would be the right way to go.
> But as far as i know, Haskell doesn't have such features.
IO.hGetContents? I suspect the result of using hGetContents on a
file you have open for writing in the same program can't be modeled
as a pure function; at best you can say it depends on the order of
evaluation which isn't defined. Not that it's necessarily a huge
blow to your argument (hGetContents is viewed with some suspicion
anyway), but it is a Haskell98 feature.
Things obviously get more complicated in the presence of
concurrency. I'm not certain, but I believe some of the memory
consistency models being discussed for Haskell' are not expressible
using a non-deterministic merge, which basically assumes that all
program actions are serializable.
> Claus Reinke wrote:
>> Paul Hudak wrote:
>>> As an author of such a book, I'm not willing to do this. Or at
>>> least, if we omit concurrency and impure operations such as
>>> unsafePerformIO, Haskell is a purely functional, sequential, and
>>> deterministic language, whose semantics, including that of IO,
>>> can be explained via conventional equational reasoning.
>> I'm very surprised to hear you say this, and I certainly cannot
>> a language that contains elements that are not best expressed as
>> is not "purely functional" anymore, even when its design carefully
>> ensures that it is still pure, and mainly functional, and can be
>> about equationally. the element that falls outside the remit of
>> is the interaction with the runtime context (operating system/other
>> processes/users/external world/..).
>> Haskell's approach to this issue is mostly functional and clearly
>> separates functional part from the part that is "out of its
>> hands": functionally compute an interaction description, have that
>> interaction performed under outside control, have control returned
>> to functional evaluation with a representation of the interaction
>> result, repeat until done. (an informal recipe like this may be
>> even more suitable for
>> learners than either process calculus rules or claims about being
>> purely functional in principle).
>> if you wanted to model that middle part functionally, you'd have
>> to cover all of the external world as well as scheduling. one nice
>> thing about a process calculus style operational semantics is the
>> modular description; you only need to model how Haskell programs
>> fit into the external world, not the external world itself:
>> assuming that world to be modelled in the same style, we need a
>> miniscule amount of process calculus rules to describe the i/o
>> interactions, falling back to functional-only reasoning for the
>> vast majority of the language.
>>> I'm sure that it can also be explained via a suitable process
>>> calculus, but that is an overkill -- such calculi are best used
>>> for describing non-deterministic / concurrent languages.
>> using a process calculus framework does not imply that each
>> process has to be non-deterministic / concurrent -- it just makes
>> it easier to
>> show how the "purely functional, sequential and deterministic"
>> evaluation inside a process running Haskell is embedded into and
>> influenced by interactions with the rest of the framework.
>> attempts to ignore that external framework tend to cloud the issues.
>> and as Brian points out, that is more confusing for learners of the
>> language than having to take a tiny bit of process calculus with
>> your mostly functional prescription!-)
>> (*) it is rather dated by now, and certainly not up to the demands
>> of pragmatic Haskell programmers today, but I discussed some
>> of the various functional i/o styles in this way in chapter 3 of
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
More information about the Haskell-Cafe