[Haskell-cafe] The values of infinite lists

[Paul Hudak]

Brian Hulley wrote:
 > Therefore I humbly submit a call for authors of books/tutorials on IO to
 > come clean and admit the fact that IO completely changes the language
 > from being purely functional into a functional + process calculus
 > language :-)

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 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.

   -Paul


Brian Hulley wrote:
> Robert Dockins wrote:
> 
>> On Wednesday 10 May 2006 02:49 pm, you wrote:
>>
>>> I could write:
>>>
>>> ] (r',_) = runIO (mapM print ones) realWorld
>>>
>>> and this computation, even though some printing would be observable,
>>> still evaluates to bottom, because r' will never be bound.
>>
>>
>> Humm... how do you define observable? If r' is never bound, how can I
>> observe any intermediate printing?
> 
> 
> I meant observable in the sense that the printing is just like a debug 
> trace of evaluation, and so is irrelevant when using the world-state 
> transformer point of view.
> 
>> [snip]
>> The world-state-transformer idea is nice as a didactic tool, but I
>> don't think its the right world-view for serious thinking about
>> Haskell's semantics.
>>
>>>
>>> I thought everything in Haskell is purely functional - surely that
>>> is the whole point of using monads? :-)
>>
>>
>> Sure.  But in that world-view then you don't think of the IO actions
>> as "running" at all, so you can't discuss their termination
>> properties.  This is more or less what all accounts (at least the
>> ones I've seen) of Haskell's semantics do -- they provide a
>> denotational semantics for the lambda terms basicaly ignore the
>> meaning of IO actions.
> 
> 
> I think from the world-state transformer pont of view, all 
> non-terminating computations must be seen as evaluating to _|_, but as 
> you point out, this point of view isn't that useful in practice.
> 
>> My favorite view of Haskell semantics is of a coroutining abstract
>> machine which alternates between evaluating lambda terms to obtain
>> the terms of a process calculus, and then reducing those process
>> calculus terms; some process calculus reduction rules call into the
>> lambda reduction engine to grow more (process calculus) terms to
>> reduce.  The observable behavior of the program is defined in terms
>> of the sequence of reductions undertaken by the process calculus
>> engine.
>>
>> In this view "bottom" is the denotion of all (lambda) terms which
>> make the lambda portion of the machine fail to terminate, and never
>> return control to the process calculus part -- thus no further
>> observations will be generated by the program.
> 
> 
> Thanks for pointing out the process calculi. I found a good page about 
> them at http://en.wikipedia.org/wiki/Process_calculus
> 
> It would be good if there was a more detailed description of Haskell 
> semantics along the lines of what you've said above, so that it would be 
> clear that the running of an IO action is something very different from 
> the running of other monads. (Not too mathematical a description but a 
> tutorial style description)
> 
> As I understand it, the IO monad shares with other monads the fact that 
> first a composite action is built from primitive actions using >>= and 
> return etc, and this composition is purely functional, even though >>= 
> and return are special built-in functions for the IO monad. (As an 
> aside, I must point out that the word "do" is ultra confusing in this 
> respect, because "do" does not actually run the action, it is just 
> syntactic sugar for composing actions which might be "done" later.)
> 
> Then, in contrast to all other monadic actions, which are "run" by 
> simply evaluating something hidden inside them (eg applying a function 
> hidden inside the monad to some initial state), the running of an IO 
> action involves the quite complicated interaction you've described 
> above, and really does go outside the functional realm.
> 
> The problem with the RealWorld view of IO, is that it is quite wrong, 
> yet this is the view propounded everywhere, so that anyone who thinks 
> there is something complicated about IO assumes it is because they 
> themselves haven't understood something properly since books/tutorials 
> keep saying how simple and purely functional it all is! ;-)
> 
> (Just like in primary school when teachers make out associativity and 
> commutivity of addition/multiplication are trivial thus leading 
> countless would-be mathematicians who immediately see these are 
> complicated but think this is their fault alone, to abandon all hope ;-))
> 
> Therefore I humbly submit a call for authors of books/tutorials on IO to 
> come clean and admit the fact that IO completely changes the language 
> from being purely functional into a functional + process calculus 
> language :-)
> 
> Best regards, Brian.