[Haskell-cafe] The values of infinite lists

[Paul Hudak]

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.

   -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