world as value

[Claus Reinke]

Hi Martin,

>I want to start a discussion about Clean's "world as value" paradigm.
>..
>    How can we assign a semantics 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.

Just follow this train of thought, you are in for some surprises!-)

First (before anyone is scared away from clean i/o;-), let me point out
that there are at least two levels to the problem: (a) how to integrate
i/o cleanly into a purely functional language, (b) how to reason about
multi-process systems where each process could be described as a purely
functional program doing i/o.

On one hand, nobody (I think) claims that the basis for Clean's i/o
system is shaky, so there is little worry about (a). On the other hand,
few (if any) would claim that Clean's approach to i/o makes the problems
of reasoning about concurrent systems go away.

I had to struggle with these doubts about pure/impure and i/o myself
during my own thesis work, and you can find some of the results in
Chapter 3 of my dissertation [1] (I tried to keep the discussion there
as informal as possible, most of this chapter is about (a) and should be
readable by non-academics; please let me know if this impression is
wrong).

While mostly informal, the different i/o systems are also described
formally as transformation systems, borrowing and adapting notation for
communication from the description of concurrent systems. If you want to
reason about systems of concurrent processes, whether functional or not,
you should investigate the theories of concurrency and the formal
systems and tools developed there (look for bisimulation, observational
equivalence, and co-induction, have a look at the pi-calculus; none of
these are mentioned in my thesis;-).

But I would like to focus here on some things I didn't describe there,
and which might help to get to the root of Martin's problem. Consider
the following simplified variant of Martin's example: a Clean P program
opens a file, closes the file, and exits. If the semantics of Clean i/o
could be described by functions from *World to *World, you would expect
P to be equal to the identity, wouldn't you? (*)

But it isn't! At some point during the execution of the program, the
file is opened, and locked for access from other concurrently active
programs (if I understand Martin's description correctly).

In concurrency theory, these problems are tackled by defining suitable
notions of observation (i.e., answering the question: what do we know
about a program and its execution?). 

In purely functional languages, we can only observe the values of
programs. We are happy about that because it makes our life and
understanding functional programs much easier (reduction is
context-free; replacing an expression by its evaluated form neither
depends on the context in which the expression occurs nor does it change
the context in any way).

If our programs engage in i/o, the situation becomes more complex: the
whole idea of i/o is for programs to interact with their runtime
contexts (to get information from files or devices and to output data to
files/devices).

So, if we want to reason about programs engaged in i/o, our notion of
observation has to take these interactions between programs and their
context into account. The formal theory is at least unusual for most
functional programmers, see [2,3] for examples, but the idea is
(roughly): 
  
  to see whether two functional programs are equivalent, we "only"
    need to observe their values and compare these
  to see whether two i/o programs are equivalent, we simulate them
    and compare whether our observations about their behaviour match
    up at each step (if A's first i/o-operation is to block a file,
    then B's first i/o-operation should be the same; if both programs
    go on to unlock the file and to terminate, we might consider them
    observationally equivalent, whatever non-i/o computation they
    do in between)

>The difficult thing here is, that TIME matters. 

Don't go down this route!-) For most purposes, it will be sufficient
(and complex enough) to consider relationships between chains of actions
taken by different agents/processes. Whether two programs interact at
noon or in the morning is likely to be as irrelevant as the clock speed
(in most cases, anyway).

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

Clean is a functional language, Clean's core is a purely functional
language, full Clean is a purely functional core + i/o facilities which
are cleanly integrated into the purely functional core. If you want to
talk about how Clean programs interact with each other, the whole
system may *not* be purely functional anymore (unless you restrict
yourself to deterministic cases; you have functions and interactions,
context-free and context-sensitive program transformations).

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

Good idea, I started from the same question and was quite surprised by
my findings. Two or three times I thought I understood completely how
monadic i/o or statically uniqueness typed environment passing i/o
worked, only to discover something new later!

Hth,
Claus

(*) You also asked for ways to adapt the *World -> *World idea to this
    wider context. One approach (hack) would be to include not only the
    current state but the whole history of the world into the *World
    object. This way, interactions would become observable in the
    function results.

[1] @phdthesis{Reinke97,
      author  = {Claus Reinke},
      title   = {{Functions, Frames, and Interactions -- completing a
                  $\lambda$-calculus-based purely functional language
                  with respect to programming-in-the-large and
                  interactions with runtime environments}},
      school  = {Faculty of Engineering, University of Kiel},
      note    = {published as technical report no. 9804, Department of
                 Computer Science, May 1998}, 
      year    = 1997,
      sourceURL     = {http://www.cs.nott.ac.uk/~czr/publications/phd.html},
      month   = aug,
      topics  = {FFI,FP - Input/Output,Modules,FP - General,Language Design/Semantics}
    }

[2] @book{Gordon94,
      author  = {Andrew D. Gordon},
      title   = {{Functional Programming and Input/Output}},
      publisher = {Cambridge University Press},
      year    = 1994,
      series  = {Distinguished Dissertations in Computer Science},
      topics  = {FP - Input/Output}
    }

    see also http://research.microsoft.com/~adg/

[3] Colin Taylor: Formalising and reasoning about Fudgets.
    PhD thesis, see also 
    http://www.cs.nott.ac.uk/Research/lap/taylor-thesis.ps
    or
    http://www.freeyellow.com/members6/drcjt/index.html

[4] see also the section on FP - Input/Output on my virtual bookshelf
    http://www.cs.nott.ac.uk/~czr/bib/bookshelf.html
    (warning: this probably misses lots of more recent work in
    functional i/o)