Auxiliary Computations: A Framework for a Step-Wise, Non-Disruptive Introduction of Static Guarantees to Untyped Programs Using Partial Evaluation Techniques

Abstract

Type inference can be considered a form of partial evaluation that only evaluates a program with respect to its type annotations. Building on this key observation, this dissertation presents a uniform framework for expressing computation, its dynamic properties and corresponding static type information. By using a unified approach, the static phase divide between values and types is lifted. Instead, computations and properties can be freely assigned to the static or dynamic phase of computation. Even more, moving a property from one world to the other does not require any program modifications. This thesis builds a bridge between two worlds: That of statically typed languages and the dynamically typed world. The former is wanted for the offered static guarantees and detection of a range of defects. With the increasing power of type systems available, the kinds of errors that can be statically detected is growing, nearing the goal of proving overall program correctness from the program’s source code alone. However, such power does come for a price: Type systems are becoming more complex, restrictive and invasive, to the point where specifying type annotations becomes as complex as specifying the algorithm itself. Untyped languages, in contrast, may provide less static safety but they have simpler semantics and offer a higher flexibility. They allow programmers to express their ideas without worrying about provable correctness. Not surprisingly, untyped languages have a strong following when it comes to prototyping and rapid application development. Using the framework presented in this thesis, the programmer can have both: Prototyping applications using a dynamically typed approach and gradual refinement of prototypes into programs with static guarantees. Technically, this flexibility is achieved with the novel concept of auxiliary computations. Auxiliary computation are additional streams of computation. They model, next to the data’s computation, the computation of property of data. These streams thereby may depend on the actual data that is computed, as well as on further auxiliary computations. This expressiveness brings auxiliary computations into the domain of dependent types. Partial evaluation of auxiliary computations is used to infer static knowledge from auxiliary computations. Due to the interdependencies between auxiliary computations, evaluating only those parts of a program that contribute to a property is non trivial. A further contribution of this work is the use of demands on computations to narrow the extent of partial evaluation to a single property. An algorithm for demand inference is presented and the correctness of the inferred demands is shown.