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.
http://www.haskell.org//pipermail/haskell-prime/2006-March/001168.html
-Paul
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!-)
cheers,
claus
(*) 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
http://www.cs.kent.ac.uk/people/staff/cr3/publications/phd.html
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Rob Dockins
Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
-- TMBG
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
