Algebraic theory of type-and-effect systems
View/ Open
Date
27/06/2014Author
Kammar, Ohad
Metadata
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 typeand-
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 Callby-
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 nondeterminism.
We give decision procedures for the applicability of the various effect-dependent
transformations, and establish their soundness and completeness.