[e-lang] [Caja] Functional auditor for Cajita: EQ vs referential transparency

[David-Sarah Hopwood]

David-Sarah Hopwood wrote:
> David Wagner wrote:
>> David-Sarah Hopwood  wrote:
>>> In fact I'm wrong [in claiming that @pure implies referentially transparent
>>> in my original proposal], as shown by this example:
>>>
>>>  /*@pure*/ function f() { return cajita.deepFreeze({}); }
>>>
>>>  const a = f();
>>>  const b = f();
>>>
>>>  /*@pure*/ function g(x) { return x === a; }
>>>
>>>  g(a); // true
>>>  g(b); // false
>>>
>>> Since a and b are observably different, either f or g must not
>>> be referentially transparent.
>>
>> I'm not sure if I follow this example.  Can you elaborate
>> what it illustrates?
>>
>> Here's my understanding of the bit I think you may be getting at:
>> conceptually, a referentially transparent function should satisfy the
>> following property: whenever x=y, then f(x)=f(y).  However, to fill out this
>> definition, we must define what we mean by "=": what form of equality we
>> have in mind.
> 
> Yes. But whatever we mean by "=", it's clear that we can't reasonably
> have true = false. In the above example, we can apply referential
> transparency once to conclude a = b (since the calls to f() have no
> arguments -- or they could have been passed the same argument), and
> again to conclude g(a) = g(b). Therefore either true = false, or
> one of f or g is not referentially transparent. But both were declared
> as @pure, therefore @pure does not imply referentially transparent for
> any definition of = satisfying not(true = false).

It appears that the Functional auditor in the design described in
<http://www.erights.org/elang/kernel/auditors/> suffers from essentially
the same issue.

Consider the E equivalent of the above example (note that 'def obj {}' has
no mutable state):

  def f() :DeepFrozen { return def obj {} }
  f :Functional  # passes

  def a := f()
  def b := f()

  def g(x) :boolean { return x == a }
  g :Functional  # passes

  g(a)  # true
  g(b)  # false

This is because each 'obj' returned by f is DeepFrozen but not DeepSelfless
(see Figure 3 of <http://www.erights.org/elang/kernel/auditors/>). If a
Functional object returns an object that is not DeepSelfless, then it fails
to be referentially transparent.

The auditors page doesn't explicitly claim that the Functional guard is
supposed to provide referential transparency. However, it does say that

# if we know that an object is functional, we can cache its output,
# reorder calls, or skip repeated calls ...

Memoization (cacheing) depends on referential transparency.

The problem with memoizing functions that don't return a DeepSelfless
value has been noted before in this thread started by Kevin Reid:
<http://www.eros-os.org/pipermail/e-lang/2006-May/011206.html>

Kevin first suggested requiring the return of a memoized function to
be guarded by DeepPassByCopy (which implies DeepSelfless). In the
specific case of memoization -- not necessarily for other uses of
referential transparency -- there are workarounds that are less
restrictive than this. For example MarkM gave a solution that involved
only adding a non-DeepPassByCopy result to the memo table when it is
seen twice: <http://www.eros-os.org/pipermail/e-lang/2006-May/011207.html>

Alternatively, for some applications it may be possible to use a
different form of cache, call it an "interning memoizer", as described
in <http://www.eros-os.org/pipermail/e-lang/2006-May/011270.html> and
<http://www.eros-os.org/pipermail/e-lang/2006-May/011282.html>.

However, those approaches are specific to memoization. If we want
to avoid the problem more generally, then we have roughly three
options:

1. Prevent pure code from using identity-revealing operations. This
   includes both primitives like === and !==, and APIs such as
   cajita.identical, Array.prototype.indexOf/lastIndexOf or the
   proposed EphemeronTable -- these would simply not be whitelisted
   as deep-frozen.

   Note that impure code can still observe that a pure function has
   returned different objects on different calls. But it is reasonable
   to ask impure code not to rely on that -- whereas if pure code itself
   could make such an observation, it would defeat the point of auditing
   as a method of determining properties of code without having to
   review it.

   This introduces the problem that pure code no longer has access
   to *any* efficient equality predicate. Below is an equality test that
   is safe to give to pure code; in the cases where egal would do
   structural comparison, it sticks its head in the sand and returns
   undefined. (This at least has the advantage of bounding the time
   for comparison to be proportional to the number of own properties
   in any tested object. It would be O(1) if not for the calls to
   Object.isFrozen, and an ES5 implementation *should* cache whether
   objects are frozen.)

     /**
      * If both x and y are frozen objects, return undefined.
      * Otherwise give the same result as cajita.identical(x, y).
      */
     function ostrichEq(x, y) {
       if (x === y) {
         if (x === Object(x)) {
           // x and y are the same object. If that object is frozen, return
           // undefined.
           return Object.isFrozen(x) ? undefined : true;
         }
         // Usually true, but might be a false positive for 0 and -0.
         return x !== 0 || 1/x === 1/y;
       }
       if (x === Object(x)) {
         if (y === Object(y) && Object.isFrozen(x) && Object.isFrozen(y)) {
           // x and y are different objects, but both are frozen.
           return undefined;
         }
         return false;
       }
       // Usually false, but might be a false negative for NaN and NaN.
       return x !== x && y !== y;
     }

2. Force all DeepFrozen objects to be DeepSelfless. Note that if
   functions can be DeepFrozen, then this is equivalent to using
   the same comparison for function instances as the original egal
   (see the definition of 'egal-function' on page 8 of Baker's paper
   <http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.9999>),
   which compares function identities and lexical environments.

   However, this may weaken encapsulation for DeepFrozen objects that
   wouldn't otherwise have been DeepSelfless.

3. [For E] Define a Pure auditor that is like Functional but also
   requires all returns to be guarded by DeepSelfless or DeepPassByCopy.

   [For Cajita] Introduce a deep-selfless auditor, and strengthen @pure
   so that a rewritten @pure function checks that its return value is
   deep-selfless.

> Forbidding use of === and !== in a deep-frozen function solves the
> problem.

This is option 1 above.

> It's similar to Joe-E restricting on == and != to non-value
> types, but we can't do that in Cajita because it is untyped.

-- 
David-Sarah Hopwood  ⚥  http://davidsarah.livejournal.com

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 292 bytes
Desc: OpenPGP digital signature
Url : http://www.eros-os.org/pipermail/e-lang/attachments/20091214/4b481b50/attachment.bin