1   The Need for Effect Checking

In most languages, the effects of an expression are often only implicitly defined, if at all. One approach used in pure functional programming languages like Haskell is to express effects in terms of monads at the cost of additional complexity.

However, it is possible to get some of the benefits of effect checking without fully specifying all types and effects by allowing the programmer to tag functions with the different kinds of effects involved in evaluating the function and annotate function arguments with the set of expected effects.

As a motivating example, the following snippet of JavaScript code calls alert from within a web worker^{1 1} An HTML5 web worker runs JavaScript in the background without access to the page DOM. Here, a non-standard startWorker function is used. which causes a crash in all current browsers.

startWorker(function() {

  alert(); // crashes at runtime
});

It is easy to see that this example will crash but more complex examples could call alert indirectly in the worker code depending on conditions that are difficult to cover with tests. It is possible to dynamically enforce that alert is not called in a worker by tracking the allowed effects in the current dynamic scope. However, this would not be a significant improvement over the eventual crash without the check. By statically checking effect annotations, it is possible to prevent this kind of runtime crash for all possible executions.

Statically checking effect annotations requires reasoning about closures, object properties and aliasing, therefore a complete and sound solution is undecidable. Instead, our analysis overapproximates effects but never misses a potential effect error, so the crash in Figure 1 is correctly detected but in the following example our analysis erroneously reports an error:

startWorker(function() {
  if (false) alert(); // would never crash

});

2   Static Analysis

As first step of the analysis, JavaScript code gets rewritten using JS_WALA [1] to the following language (“JS Normal Form”):^{2 2} Some syntactic forms like literals, arrays, method and constructor calls were omitted from the formalism as they do not add new insights.

All function definitions λ_f and object literals { ... }_o are assigned unique names/indices f and o. Additionally, all property names p occurring in the program are known in advance.

Based on control flow-insensitive set constraint-based analysis [2, 8], we approximate the type τ with a subset of all possible function definitions Λ and object literals Ω with two functions or objects considered to be the same if they originate from the same function definition or object literal.

The goal of the static analysis is to assign every variable x a type τ_x , every function λ_f a return type τ_f,R and arguments types τ_f,j and every object literal {}_o a type τ_o,p for every property p. To infer a suitable assignment, the analysis generates subset (type inclusion) constraints to a constraint system C for every statement in the program according the following rules:^{3 3} These constraints are generated with complexity O(n³) [8].

This constraint system includes a complete call graph for all functions and forms the basis for the following analysis of the effect contracts.

3   Effect Checking

In order to specify effects, we extend function definitions in the language to allow a set of effect names [e] as well as expected effects [!e] to function arguments.

The effects are simple tags/strings which cannot be parametrized. In addition to types, the constraint system now also infers a mapping from functions λ_f to their effects ϕ_f based on two constraint generation rules. The first rule adds effect and effect restrictions; the second rule propagates effects from callee to the calling function which is the current function scope c during constraint generation C_f.

The resulting constraint system can then be solved with an SMT solver like Z3 [5]. If the system is unsatisfiable, the unsatisfiable core of constraints is used to highlight code in the original program involved in the effect errors (see Figure 1).

4   Related Work

Prior work on effect systems encompasses decades of research and often goes beyond the restricted set of effect tags presented in this paper by better integrating the effect system with the operational semantics of the language [3 , 9 ]. Effect systems with algebraic effects [10] allow an even richer effect language, e.g. Brady [4] showed an effect system for Idris in which effects can be parametrized by other types, so a STATE Inteffect would allow type-safe state updates on integer values.

Additionally, set constraint-based program analysis [2, 8] for JavaScript has been explored before, e.g. the idea of typing objects and functions by their generating definition or literal has previously been applied by Hackett and Guo [7] to improve the performance of the SpiderMonkey JIT compiler.

5   Discussion

Effects are an integral part of the program behavior, so leaving these unspecified might increase the potential for accidental programming errors. Unfortunately, specifying all the types and effects in a program might hinder scripting and prototyping, so a light-weight effect system which automatically infers unspecified effects might serve as compromise solution.

Our prototype implementation^{4 4} Source and demo are available at https://github.com/levjj/jsfxs shows that effects can be checked statically in a language like JavaScript. It requires effect annotations which are automatically desugared by a set of sweet.js macros [6]. However, other ways of specifying effect contracts might be of interest for future work.

Apart from restricting certain kinds of programmer-specified effects like DOM or file system access, effect contracts could also be used to enforce checked exceptions as used in Java. Furthermore, effect annotations as presented in this paper can also be seen as statically-checked higher-order temporal contracts which is part of a broad area of research in contract systems.