[Cross-posted to e-lang from google-caja-discuss. I suggest continuing on e-lang, since there's not much that is Caja-specific here.]
[email protected] wrote: > Hi folks, > > Here is a proposal for a Cajita auditor for purely functional values: 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. (In the Caja context, L here would be Cajita, i.e. the expression is rewritten.) > 1. All transitively frozen JSON values are functional. > > 2. All function values are born frozen, so they are functional *as values*. > > 3. The compiler can conservatively annotate certain functions as > purely functional. This will miss some cases, but again, this is > conservative. It's unclear whether we should call a function "purely functional" if it is possible for it to be called with impure arguments (or use captured values that are impure). If it can, and we require it to have no side effects and be deterministic in that case, then almost no useful functions are pure. 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. (This is a soft effect system, with non-copaceticity being the only effect. Come to think of it, E-style auditing in general is a soft effect system.) So, a rewritten copacetic function instance must check that all its arguments are copacetic before using them. If such a function instance refers to a captured variable, then we must also check whether the variable's value is copacetic, and that the variable is 'const' (so that the value cannot change), before using it. The latter checks can (and for efficiency, should) be done when instantiating the function, not on every call. A failure of these checks would deterministically throw an exception, which is not counted as a side effect. > Perhaps we can add some annotation for programmers to > ask the compiler to treat failure to verify as an error, like: > > var f = /*...@functional*/ function(x, y) { ... }; In my proposal this would mark the function instance as copacetic, add the above argument checks to the function body, and check any captured values. So for example: const z = ...; var f = /*...@functional*/ function(x, y) { return x+y+z; }; would be rewritten (ignoring other aspects of the Cajita rewriting) to: const z = ...; var f = (___.checkCopacetic(z), ___.copaceticFunc(function(x, y) { ___.checkCopacetic(x); ___.checkCopacetic(y); return x+y+z; })); > 4. At runtime, any frozen data structure containing only functional > values as described above can pass a functional auditor, and the > decision can be memoized on the value. It's not clear to me that "a frozen data structure containing only functional values can pass a functional auditor" is correct or sufficient. Such a structure can contain arbitrary functions, which can refer to mutable, side-effecting, or nondeterministic values according to your suggested rules. So, it would not be the case that an arbitrary expression referring to such a structure would have no side effects and be deterministic. An auditor could however check that a frozen data structure contains only copacetic values, and if so mark it as copacetic. That would give a consistent soft effect / auditing system with the desired property. > Does this work? I think the modification I proposed works. As explained above, it would require changes to the Cajita rewriting. It also requires 'const' variables, and a programming style that uses them whereever possible. [*] Please, don't let this provisional term catch on :-) In practice we can probably get away with using "pure", or think of something better. -- David-Sarah Hopwood ⚥ http://davidsarah.livejournal.com
signature.asc
Description: OpenPGP digital signature
