Re: [Caja] Functional auditor for Cajita

David Wagner wrote:
> David-Sarah Hopwood wrote:
>> First let's decide what property we want from a purely functional auditing
>> system. I think the property we want is:
>>
>>  If all values directly referred to by an expression in language L
>>  (that is, all captured values and literals, including function literals)
>>  pass some auditor, then I know that evaluating the expression in L will
>>  have no side effects, and the resulting value or exception will be a
>>  deterministic function of those values.
> 
> Hmm.  I wonder if this is overly strict.  Maybe what we care about
> is observational side-effect-freedom: i.e., it's OK if the function
> internally performs some side-effect on an object it allocated itself
> as long as that side effect is not externally visible.  Does that
> sound right?
> 
> e.g., this is all fine, even though it internally performs
> some side-effecting operations:
> 
>     /* functional */ function f() {
>         var n = 0;
>         n++;  // OK
>         var o = {};
>         o.x = 5; // OK
>         return o; // OK
>     }

Yes, I think you're right. For an imperative or only-mostly-functional
language, there would be a severe loss of expressiveness in not allowing
internal side effects. (I hadn't intended them to be included as
"side effects" in the above definition, but didn't make that sufficiently
clear.)

> Does Cajita have the equivalent of Java's OutOfMemoryError,
> which can be thrown under effectively non-deterministic conditions?
> (The condition under which it is thrown is a deeply non-local
> condition.)

The current failure of the Caja implementation to prevent Cajita
code from catching such exceptions is issue 460, and other causes of
nondeterminism are issue 1175:

<http://code.google.com/p/google-caja/issues/detail?id=460>
<http://code.google.com/p/google-caja/issues/detail?id=1175>

Idealized Cajita, with these bugs fixed (and no other correctness
bugs in the implementation or underlying platform), would be fail-stop
deterministic -- i.e. the computation can stop at an arbitrary point
in case of failure, but is deterministic up to that point.

> Are we guaranteed in Cajita that whether an exception is thrown at
> any point is a deterministic function of the local state of named
> values involved in a specified computation (not the global state
> of the interpreter; not as a function of values not named explicitly
> in the code)?

For idealized Cajita, yes.

>> To dodge this issue, let's provisionally call a function *instance*
>> "copacetic" [*] if:
>> - that instance has only captured copacetic values, and
>> - it has no side effects and is deterministic whenever it is
>>   only called with copacetic argument values, and
>> - it uses no side-effecting or nondeterministic primitives.
> 
> If I understand correctly, this seems overly strict.  It should
> be safe for a functionally pure function to capture and invoke a
> reference to a non-copacetic function, shouldn't it?

Yes, provided the return value is deep-frozen. In that case, we
have almost exactly E's Functional auditor (modulo the lack of
explicit guards).

> I may not be thinking about this clearly, so there may well be
> numerous errors in what I wrote above!

No, that was an impressively quick and accurate response (but you
didn't catch the return value error ;-)

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

_______________________________________________
e-lang mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/e-lang

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.12 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iF4EAREIAAYFAkseF34ACgkQWUc8YzyzqAf5QgEAgueIpnM2rDkl6G+CECO1Gq0O
b8taUfM/1O1hAtZIICsA/3d54r0wVXQ2UzsNxhoHlno/j+IRm4XlGaEGJj5+FpGz
=+QkQ
-----END PGP SIGNATURE-----