Freeing futures from fuziness

[Raphael Collet]

I am trying to model formally futures and by-need evaluation.  And this
work confronts me with several problems:
 - the definition is generally informal and not precise enough;
 - the word "future" is sometimes misleading;
 - their implementation contains bugs.

I would like to know your opinions about the two following questions,
which I develop below.
 (1) What is the precise definition of a "future"?
 (2) Does ByNeed return a "future"?

Thanks in advance.



I use the following documents as references:

 [1] Futures and By-need synchronization.
     http://www.mozart-oz.org/papers/abstracts/oz-futures.html

 [2] The Oz Base Environment.  (section 10.1)
     http://www.mozart-oz.org/documentation/base/node13.html



-1- What is the precise definition of a "future"?

Most documents define a future as "a read-only capability of a logic
variable".  But if I get a future of a given variable twice, i.e.,

	declare X
	F1=!!X
	F2=!!X

are F1 and F2 equal?  Only [1] answers this question: "Every variable is
associated with a future that is logically equal to the variable."  In
my opinion, this implies that both F1==F2 and F1==X do not block and
return true.

The platform currently does not implement this.  Each call to Value.'!!'
returns another read-only view of the variable, *except* if the variable
is already a future.  In other words, if F1 and F2 are defined as above,
both F1==F2 and F1==X block until X is bound.  Ugly (IMHO).

There is another possibility: each call to Value.'!!' returns a *new*
read-only view of the variable.  It can be used to limit the information
that can be extracted from an abstract data type, for instance.  Though
I do not adhere to that view, because it completely burns out the
logical nature of futures.  Ugly, too (IMHO).



-2- Does ByNeed return a "future"?

All the definitions I have seen are equivalent to:

	ByNeed takes a one-argument procedure P, and returns a future F.
	When a thread tries to access the value of F, {P X} is called,
	and its result value X is bound to F.

The term "future" in this context can be misleading.  Nothing is said in
the case where the returned value is an unbound variable, such as in

	declare X
	Y={ByNeed fun {$} X end}

If I execute Y=unit, will X be bound to unit?  I see two possible
answers to this question:

 (a) Y=unit binds X to unit.  This is what the current implementation
     does.  In this case, Y is not a barrier against binding, and I
     think we should not use the word "future" to describe Y.
     
     I could avoid the binding of X by executing !!Y=unit, which would
     request the evaluation of Y and protects Y against binding.  But
     the implementation contains a BUG: !!Y returns Y itself, because Y
     is already a "future"...

 (b) Y=unit blocks until X is bound.  It looks like Y is bound to a
     future of the result of the evaluation.  This looks closer to
     functional programming than logic programming...



That's all, folks!

--
Raphaël Collet - raph at info.ucl.ac.be - http://www.info.ucl.ac.be/~raph/
-
Please send submissions to hackers at mozart-oz.org
and administriva mail to hackers-request at mozart-oz.org.
The Mozart Oz web site is at http://www.mozart-oz.org/.