[Haskell-cafe] The values of infinite lists
paul.hudak at yale.edu
Tue May 23 09:50:18 EDT 2006
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.
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 agree.
> a language that contains elements that are not best expressed as functions
> is not "purely functional" anymore, even when its design carefully
> ensures that it is still pure, and mainly functional, and can be reasoned
> about equationally. the element that falls outside the remit of functions
> 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
More information about the Haskell-Cafe