world as value

[Rolf-Thomas Happe]

> I want to start a discussion about Clean's "world as value" paradigm.
> The questions that always go through my mind are:
[...]
> My problems with the world as value paradigm arise from the fact, that
> the world is not only changed by a Clean program, but also changes
> itself independently.
[...] 
> I would like to have a FORMAL model of the World type. In principle it
> should be possible to derive with that model from the input value which
> number will be calculated by the poll function.

I'd naively try a more resignative approach (naively since I'm no expert):
   For each run of a Clean program there is a Clean model (which doesn't
rely on library functions) of the World and the basic World transforming
functions.  This model has the autonomous actions of the world wired in
and can be determined only after the fact (i.e. after the disk crashed,
the printer went offline, and the user furiously left the room).  Still
you may devise a scheme of Clean models resp. a Clean subprogram which
contains fresh constants (or free variables, evil, misChief, and badLuck)
representing the things the stubborn world does on its own.  That is,
every run of a Clean program would interpret these constants by pure
Clean functions (hopefully identity functions which leave the world alone).
   When you want to prove the program correct, you will have to do some
logical inferencing in addition to the equational transformations of
lambda calculus, due to these constants in the definitions of the World
transformers.
   (Actually, I think you can get away with one model of the World type,
and you may regard the basic *World -> *World function symbols as constants
which get an extra interpretation per every run of the program.)

rthappe