world as value

Martin Wierich martinw@cs.kun.nl
Mon, 14 Jun 1999 18:10:00 +0200


Hi everybody,

I want to start a discussion about Clean's "world as value" paradigm.
The questions that always go through my mind are:

    How can we assign a semantics to the *World ?

and if we have an answer:

    What semantics do we WANT to assign to the *World ?

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.

Let's start at the beginning.

Clean programs are functions. They return a value, that solely depends
on the input parameter. To do I/O, the uniquely attributed World type
was invented. We have to give functions that take arguments of that type

a semantic (does anybody disagree ?). How can we give these functions a
semantic ? Well, we have to do it like in mathematics. At the very end
every function is a subset of the cartesian product of the input "types"

(sets) and the result "type" (a set), that satisfies certain conditions
(a function is a special case of a relation). We have to specify this
set in a precise notation. I call Clean programs that do not call any C
functions or ABC code directly or indirectly "pure" Clean programs. The
semantics of pure Clean programs is obvious. In the following I want to
try to assign a semantic to functions that operate on the *World by
defining them in pure Clean. Later I show that, it is not that simple.

To keep things easy, I only consider file I/O. So:

    :: *World :== *Files

Further I assume, that there is only one disk, and that there is no
directory structure (like on the old Apple II).
Then the *Files subworld could be a list of files:

    :: *Files = Files [File_]
    :: File_ :== (Filename, Maybe Contents)
    :: Filename :== String
    :: Contents :== [Char]
    :: Maybe x = Just x | Nothing

I use the Maybe type to model whether a file is open or not (in an
Operating system sense): iff the file is open then the Maybe part will
be Nothing. The String and Char type aren't pure, but this doesn't
matter, because they could easily be expressed in terms of algebraic
types. With these type definitions I give the StdFile module's fopen,
fwritec and fclose functions a semantic:

    FAppendText :== 2              // for simplicity I restrict
                                   // myself to that file mode

    // open a file:

    fopen :: String Int *Files -> (Bool, *File_, *Files)
    fopen filename FAppendText (Files files)
        #   (l,r)   = span (\(fname,_) -> fname<>filename) files
        = case r of
            []
                // the file doesn't exist. Create a new one
                -> ( True
                   , (filename, Just [])
                   , Files [(filename, Nothing): files]
                   )
            [(_,Nothing): r2]
                // the file is open. Give back a dummy file
                -> ( False
                   , (filename, Nothing)
                   , Files (l++[(filename, Nothing):r2])
                   )
            [(_,Just contents): r2]
                -> ( True
                   , (filename, Just contents)
                   , Files (l++[(filename, Nothing):r2])
                   )

    // append a character to a file

    fwritec :: Char *File_ -> *File_
    fwritec ch file=:(_, Nothing)
        = file
    fwritec ch file=:(filename, Just contents)
        = (filename, Just (contents++[ch]))

    // close a file

    fclose :: *File_ *Files -> (Bool, *Files)
    fclose (filename, Nothing) files
        = (False, files)
    fclose file=:(filename,_) (Files files)
        #   (l,r)   = span (\(fname,_) -> fname<>filename) files
        = (True, Files (l++[file:tl r]))

Fantastic ! I have created a precise semantic ! Let's write a program:

    Start
        #   world           = Files []
        #   (_, file, world)= fopen "myFile" FAppendText world
            file            = fwritec 'X' file
            (_, world)      = fclose file world
        = world

Good ! This program returns what I expected:

    (Files [("myFile, Just ['X'])])

And guess what ? The semantics even matches reality. I only have to make

my program impure. So I replace the function definitions of fopen,
fwritec and fclose with imports from the StdFile module and I replace
the first two lines of the Start rule above
with "Start world". Now I have a program that affects my harddisk by
creating a file named "myFile" which contains the character 'X'.

Let's write another program:

    Start world
        = poll 0 world

    poll i world
        | i==100000000
            = (i, world)
        # (ok, file, world) = fopen "myFile" FAppendText world
        | ok
            = (i, world)
        | otherwise
            = poll (inc i) world

This program increments a counter until this counter reaches the value
100000000 or until the opening of the file succeeds. We can derive from
the pure version of this program, that the return value will be either 0

or 100000000.

HERE IS A CONTRADICTION

The model is wrong. If I first open "myFile" with another program, and
then start the poll program, the opening of "myFile" will not succeed at

first. The counter will be incremented. If I quit the program, that has
opened "myFile", then suddenly the poll function would be able to open
the file, and could return a value different from 0 or 100000000.

How can we alter our model of the world to remove this contradiction ?

Dear readers of this message. I want you to make proposals.

The difficult thing here is, that TIME matters. Also the execution speed

of the program is involved. Many things are involved, If you really
think about it.

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.
At least I want to have some outline of a formalism that makes me
believe it is sound. I want to have this, because otherwise I would have

problems to call Clean a functional programming language. Will it ever
be possible to use proof tools with functions that have a world
parameter ? (A tool called "Clean Prover System" is in development.) And

last but not least I want to have an answer, because I as a Clean
developer often write functions that affect the whole *World. These
functions simply ignore the *World parameter and make a call to a C
function. It is very pragmatic to say "everything is allowed, as long as

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.

Shortly, I want to have some clarity, because I want to know, what I'm
doing.

best wishes
  Martin Wierich
  University of Nijmegen