world as value

[Erik Zuurbier]

Martin,

I would like to comment on two points in your email:

> To keep things easy, I only consider file I/O. So:
> 
>     :: *World :== *Files
> 
I think you cannot do this that easily. The point is that, as far as the
program is concerned, the *World object could contain anything, for instance
an endless list of Booleans where each Boolean determines whether the next
fopen is going to fail or succeed. The only way you have access to this list
of Booleans is actually trying fopen.

The program is provided the *World value at a certain moment but you can
influence the contents of the list of booleans afterwards as you clearly
demonstrate. This is strange from a phylosophical point of view, but as far
as the program is concerned, this makes no difference, as the program only
evaluates Booleans when they are needed.


>     Start
>         #   world           = Files []
[snip]

> Let's write another program:
> 
>     Start world
>         = poll 0 world
> 
There is a big and essential difference between the two. In real life Clean,
as in the latter of your two examples, the program is PROVIDED with a world
value. You cannot completely specify its contents, as in your first example.
So each time you run a Clean program, it is provided with a potentially
different world value. Together with the idea that this different world
could contain a different list of Booleans (see above), this prevents you
from proving that different runs of the program should return the same value
of i, or that i should either be 0 or 100000000.

> The model is wrong.
> 
Indeed. The two steps you took (one: reducing the *World to just *Files,
two: switching from an unspecified world value PROVIDED to the program, to a
value that is completely specified within the program) seem unjustified to
me.

I hope this somehow helps to get a better understanding of Clean IO.

Regards Erik Zuurbier