[Haskell-cafe] The values of infinite lists

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.

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
> Haskell-Cafe at haskell.org
> 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