world as value

[Fergus Henderson]

On 22-Jun-1999, Adrian Hey <ahey@iee.org> wrote:
> Suppose I ask my computer to perform some computationally intense activity
> which is going to take a long time, like placing and routing an FPGA (this
> takes hours). Immediately after this I ask the computer the time. Let's say
> I do this at precisely 2:00 pm.
>  First question   - What time should the computer output?
>  Answer           - The time of the "me ask computer" event I.E. 2:00 pm
>  Second quesition - When does it do this?
>  Answer           - When the FPGA has been placed and routed, lets say 4:15 pm
> 
> I think most people would regard this as "intolerable behaviour". What it
> should do is suspend the placing and routing of the FPGA to for moment, in
> order to respond, telling me the time is 2:00 pm at 2:00 pm, or very shortly
> thereafter. But it simply can't do this if it's running a program expressed as
> a function mapping input events to output events. This would be
> non-deterministic.

You can express this as a function mapping input events to output events.
For example:

	import IOExts	-- for forkIO
	import Time	-- for getClockTime, etc.

	main = forkIO compute_fpga tell_current_time

	compute_fpga = ...

	tell_current_time =
		do time_string <- get_current_time
		   putStrLn ("Current time is " ++ time_string)

	get_current_time =
		do time <- getClockTime
		   date <- clockTimeToCalenderTime time
		   return (calenderTimeToString date)

The above is all legal Haskell, except that forkIO is a ghc extension.
But you can express forkIO in Haskell too, using the techniques
described in the papers I previously cited to handle the required
nondeterminism.  You just need to put the nondeterminism in the input data,
for example by having the initial world contain a tree of timestamps
which are used to determine the order in which concurrent I/O actions
will get merged.  See the code at the end of this mail.

Of course an actual implementation will have to handle code generation
for forkIO specially, rather than using the equations given below.
But it's going to generate special code for `+' on Int or Float too.
I don't see that as a problem.  So long as there is a way of modelling
the behavior of `forkIO' and `+' within the language, then we can reason
about how they behave, and it doesn't matter if the actual implementation
doesn't resemble the source code, so long as it behaves the same.

> > > The issue which concerns me is:
> > > 
> > >  'Can systems with tolerable behaviour be described, reasoned about and
> > >   implemented within the same language?'.
> > > 
> > > I suppose the answer is yes (people must have been working on this problem
> > > for years), but not (yet) if you're a Haskell or Clean user. (And not ever
> > > if they remain purely functional ????)
> > 
> > I think the answer is yes, even if you're a Haskell or Clean user.
> > Why do you think otherwise?
> 
> Because I can't express non-deterministic programs in Haskell or Clean. I can
> build deterministic components of non-deterministic systems in Haskell or
> Clean, but I will always need outside 'black box' help to complete the system.
> What I want to do is describe my entire system in 1 language. 

The modelling technique described above uses only one language,
and describes all of the system except the bits which are deliberately
unspecified, which are treated as input data to `main'.

If you really want to formalize the _entire_ system, leaving absolutely
nothing unspecified, the results will not be very useful, since they
will only apply to a single run of your program on a single machine,
using a single compiler and a single set of compilation options.
However, in principle if you had a sufficiently detailed formal model
of the machine, the compiler, and so on, then you could write the whole
things as a single Haskell program with no input.  And in that case there
would of course be no nondeterminism.

...
> Now of course, the question arises what do I mean by 'entire system'. To
> properly answer this question perhaps we really need a define 'virtual machine'
> to which all programs are notionally targeted. I'm not sure quite what this
> machine should be capable of doing. You could argue that this is just another
> piece of 'black box' outside help, indeed it is. But if it's accurately
> defined, it will be less black than most.
> (and before anybody asks, yes I am aware of Java:-)

If your virtual machine is completely specifies all details, then it
won't be sufficiently expressive -- you won't be able to model the
concurrency that occurs on real machines.  If, like the JVM, your
virtual machine leaves some things unspecified, then there's really
not that much conceptual advantage in using a low-level virtual machine
model rather than a high-level model like the one I described, because
in both cases, some things will be left unspecified.

Of course, a low-level model will specify the operational semantics in
detail, whereas the high-level model that I described specifies only
the denotational semantics and leaves the operational semantics and 
completely unspecified.  Thus a lower-level model would certainly have
it's uses.

-- 
Fergus Henderson <fjh@cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh@128.250.37.3        |     -- the last words of T. S. Garp.