Algebraic foundations for effect-dependent optimisations

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present a general theory of Gifford-style type and effect annotations, where effect annotations are sets of effects. Generality is achieved 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 operation symbols. We develop an annotated version of Levy's Call-by-Push-Value language with a kind of computations for every effect set; it can be thought of as a sequential, annotated intermediate language. We develop a range of validated optimisations (i.e., equivalences), generalising many existing ones and adding new ones. We classify these optimisations as structural, algebraic, or abstract: structural optimisations always hold; algebraic ones depend on the effect theory at hand; and abstract ones depend on the global nature of that theory (we give modularly-checkable sufficient conditions for their validity).
Original languageEnglish
Title of host publicationProceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
Place of PublicationNew York, NY, USA
PublisherACM
Pages349-360
Number of pages12
ISBN (Print)978-1-4503-1083-3
DOIs
Publication statusPublished - 2012

Keywords

  • algebraic theory of effects, call-by-push-value, code transformations, compiler optimisations, computational effects, denotational semantics, domain theory, inequational logic, relevant and affine monads, sum and tensor, type and effect systems, universal algebra

Fingerprint Dive into the research topics of 'Algebraic foundations for effect-dependent optimisations'. Together they form a unique fingerprint.

Cite this