#An algebraic theory of type-and-effect systems ####Ph.D. Thesis
PDF, and LaTeX/METAPOST/Haskell/SML source.
Abstract
We present a general semantic account of Gifford-style type-and-effect systems. These type systems provide lightweight static analyses annotating program phrases with the sets of possible computational effects they may cause, such as memory access and modification, exception raising, and non-deterministic choice. The analyses are used, for example, to justify the program transformations typically used in optimising compilers, such as code reordering and inlining. Despite their existence for over two decades, there is no prior comprehensive theory of type-and-effect systems accounting for their syntax and semantics, and justifying their use in effect-dependent program transformation.
We achieve this generality by recourse to the theory of algebraic effects, a development of Moggi’s monadic theory of computational effects that emphasises the operations causing the effects at hand and their equational theory. The key observation is that annotation effects can be identified with the effect operations.
Our first main contribution is the uniform construction of semantic models for type-and-effect analysis by a process we call conservative restriction. Our construction requires an algebraic model of the unannotated programming language and a relevant notion of predicate. It then generates a model for Gifford-style type-and-effect analysis. This uniform construction subsumes existing ad-hoc models for type-and-effect systems, and is applicable in all cases in which the semantics can be given via enriched Lawvere theories.
Our second main contribution is a demonstration that our theory accounts for the various aspects of Gifford-style effect systems. We begin with a version of Levy’s Call-by-push-value that includes algebraic effects. We add effect annotations, and design a general type-and-effect system for such call-by-push-value variants. The annotated language can be thought of as an intermediate representation used for program optimisation. We relate the unannotated semantics to the conservative restriction semantics, and establish the soundness of program transformations based on this effect analysis. We develop and classify a range of validated transformations, generalising many existing ones and adding some new ones. We also give modularly-checkable sufficient conditions for the validity of these optimisations.
In the final part of this thesis, we demonstrate our theory by analysing a simple example language involving global state with multiple regions, exceptions, and non-determinism. We give decision procedures for the applicability of the various effect-dependent transformations, and establish their soundness and completeness.
Lay summary
We instruct computers about their tasks using detailed textual descriptions, called “programs”, encoded in a precisely defined “programming language”. Another program, the “compiler”, then translates our textual description into a description the machine can execute. The compiler may change, or “optimise”, the translated program in order to achieve better performance, for example to make the program execute faster, or extend battery-life. One example for such “transformations” is the reordering of instructions.
Our programs may cause “computational effects” besides computing their end results, such as display an image on a monitor, respond to a keyboard stroke, and print a document. Some transformations become invalid in the presence of effects, causing tension between the two. For example, consider a program that first displays a message on the screen and then waits for the user to press a key on the keyboard. Our compiler must not reorder these two tasks during optimisation, or else the program will wait for the user to hit the keyboard before it displays the message to do so.
To ensure the optimisation process is correct, some compilers analyse the program and attach to each part a summary of the effects this part may cause. In the above example the part of the program that displays the message will be annotated with the effect “output”, and the part of the program that reads the user’s keystroke will be annotated “input”. This annotation is called a “type-and-effect system”. The compiler’s designers carefully study the programming language at hand and develop conditions that ensure the optimisations are indeed safe. For example, parts annotated with “output” should never be reordered with parts annotated with “input”. Despite their existence for over two decades, there is no prior comprehensive account of type-and-effect systems beyond a case-by-case study. This thesis develops such a general account.
We rely on the theory of “algebraic effects”, which describes many computational effects through equations and operations. This account combines the abstract “input” and “output” effects in a fashion reminiscent of how we combine addition and multiplication in elementary school algebra. Our first main contribution is a general mathematical description of these effect annotations based on such an algebraic description of the programming language at hand. Our second main contribution is a demonstration that our theory accounts for the various aspects of type-and-effect systems: it describes the effect annotations and their meaning; it validates the optimisations; and it justifies that the optimisation process does not change the meaning of the original program. Finally, we demonstrate our theory by analysing a simple example language.