world as value

[Fergus Henderson]

On 21-Jun-1999, Bjorn Lisper <lisper@it.kth.se> wrote:
> Fergus Henderson:
> >It is quite possible to model non-determinism in a purely functional
> >framework. See for example the following references.
> >
> >     *  F. Warren Burton, ``Nondeterminism with Referential
> >        Transparency in Functional Programming Languages,'' in Computer
> >        Journal, 31(3), 1988, pp. 243-7.
> >
> >     *  John Hughes, John O'Donnell, ``Expressing and Reasoning About
> >        Non-deterministic Functional Programs,'' in Proc. of the 1989
> >        Glasgow Workshop on Functional Prog., pp. 308-28.
> 
> One must be careful not to mix up referential transparency and purely
> functional frameworks.

Well, OK, but my claim holds true for both of those, I think.
I don't think the distinction is relevant to whether or not you can
express nondeterminism, is it?

> Yes, one can model nondeterminism in a purely
> functional framework by "oracles" magically providing the missing
> information (the time stamps in the merge example above is a simple example
> of this).

The word "magically" here seems to have a disparaging connotation ;-)
In the context of the "world as value" paradigm, you don't need the
concept of a magic oracle; the missing information can just be part
of the world, with no magic needed.

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

P.S. to elaborate further on my explanation of what was a very minor point:

> Fergus Henderson:
> >In Clean, Haskell, and Mercury, the imperative-style parts are written using
> >syntax that has a very simple mapping to code using only pure functions
> >(or predicates) which have a relatively simple and clear declarative
> >(denotational) semantics.
> >For the imperative-style parts of the program, you can reason about them
> >using the operational semantics, but because they also have a declarative
> >semantics, it's possible to reason about them using the declarative semantics
> >too.
> >
> >This contrasts to the situation where the imperative-style parts of the
> >program are written using syntax that does not have a simple declarative
> >semantics, as would be the case if you wrote the imperative-style parts
> >of the program in C, for example.
> 
> Hmm, what do you mean by "not having a simple declarative semantics"?
> That one must resort to powerdomains?  Surely C programs can, at least in
> principle, be given a denotational semantics 

Yes, I suppose you are right.  I suppose that you can always give the
imperative parts a denotational semantics using either the world-as-value
paradigm or the IO Monad paradigm, even if that is not officially sanctioned
by the language specification.  However, if the relationship between the
imperative language's syntax and its operational semantics is complicated,
or if the operational semantics itself is complicated, as is the case for C,
then figuring out the denotational semantics of a particular piece of
imperative code may be quite difficult.

When I wrote my original statement

| It helps if the imperative parts also have a declarative semantics,
| as they do in Clean, Haskell, and Mercury, but this is not essential.

I had in mind the fact that compilers for Haskell can transform everything
into some kind of core syntax based on lambda calculus, and they can then
apply transformations based on the laws of lambda calculus, without
needing to specifically mark each function as being pure or impure and
check this annotation before performing such transformations.
(Similarly, in principle programmers can do the same.)

I suppose that a compiler could do the same kind of thing for a language 
with split imperative and functional parts, even if there was no "official"
declarative semantics for the imperative parts.  However, if the relationship
between the imperative syntax and its denotational semantics is not very
simple, then this probably wouldn't be worthwhile.

Anyway, as I said this is a very minor point.

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