world as value

[Pedro Palao Gostanza]

Hello,

Here is my little grain of sand related to the problem
that Martin Wierich posed.

Contrary to Erik Zuurbier, i think that Martin only made
one error: reasoning about i/o using his simplified model,
i.e. thinking that the "provided" world will behave like
his "algebraic" model.

In think that there is no problem with World having only
the Files part. The World of each program can only have
the data used in the program; the rest have no use, cannot
be modified and cannot change the behaviour of the program.

Martin suggests a change in the i/o semantics.
> you have a World parameter". But I think a Clean developer should not
> forget about the semantics of his functions !!! AND MAYBE A DIFFERENT
> FUNCTION IMPLEMENTATION WOULD LEAD INTO A SIMPLER MODEL OF THE WORLD.
> For instance we could keep the easy above *World model, if we would
> alter the function implementations in "StdFile" appropiately. You could
> make proposals here, too.
But i think that the present "semantics" (behaviour) is the
correct one. We need a formal model of the actual semantics.
For example, World could be simulated with a pair: the real data
of the world and an infinite list of actions of other agents that
use this data concurrently. Whenever we access the data, the
next action modifies it.

:: *World :== (*WorldData, [*WorldData -> *WorldData])
:: *WorldData :== *Files

This definition of *World is an "Abstract Data Type" that can only
be accesed with

overData :: *World (*WorldData -> (.b,*WorldData)) -> (.b,*World)
overData (data, [g:gs]) f = (b, (data`,gs))
where (b,data`) = f (g data)

This model don't have this property:

  fopen s FAppendText w = (b,_,w`) && b = False  =>  w = w'

that Martin relies on to prove that poll 0 world must return
0 or 100000000.

Regards,
  Pedro Palao