Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness

Yuyan Bao, Tiark Rompf

TL;DR

The paper addresses how to compare purification-focused typing disciplines for effects and capabilities using a semantic notion of purity grounded in contextual equivalence. It introduces a completeness-based expressiveness measure and proves that minimal binary effect and capability systems are incomparable, motivating a synthesis λ_{ae} that unifies types, abilities, and effects. A binary logical-relations framework is developed to prove purity-related properties and contextual equivalence across λ_e, λ_a, and λ_{ae}, with mechanized proofs. This semantic foundation enables rigorous comparisons and planning for language design that balances precision and usability in reasoning about effects and resources.

Abstract

Programming benefits from a clear separation between pure, mathematical computation and impure, effectful interaction with the world. Existing approaches to enforce this separation include monads, type-and-effect systems, and capability systems. All share a tension between precision and usability, and each one has non-obvious strengths and weaknesses. This paper aims to raise the bar in assessing such systems. First, we propose a semantic definition of purity, inspired by contextual equivalence, as a baseline independent of any specific typing discipline. Second, we propose that expressiveness should be measured by the degree of completeness, i.e., how many semantically pure terms can be typed as pure. Using this measure, we focus on minimal meaningful effect and capability systems and show that they are incomparable, i.e., neither subsumes the other in terms of expressiveness. Based on this result, we propose a synthesis and show that type, ability, and effect systems combine their respective strengths while avoiding their weaknesses. As part of our formal model, we provide a logical relation to facilitate proofs of purity and other properties for a variety of effect typing disciplines.

Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness

TL;DR

The paper addresses how to compare purification-focused typing disciplines for effects and capabilities using a semantic notion of purity grounded in contextual equivalence. It introduces a completeness-based expressiveness measure and proves that minimal binary effect and capability systems are incomparable, motivating a synthesis λ_{ae} that unifies types, abilities, and effects. A binary logical-relations framework is developed to prove purity-related properties and contextual equivalence across λ_e, λ_a, and λ_{ae}, with mechanized proofs. This semantic foundation enables rigorous comparisons and planning for language design that balances precision and usability in reasoning about effects and resources.

Abstract

Programming benefits from a clear separation between pure, mathematical computation and impure, effectful interaction with the world. Existing approaches to enforce this separation include monads, type-and-effect systems, and capability systems. All share a tension between precision and usability, and each one has non-obvious strengths and weaknesses. This paper aims to raise the bar in assessing such systems. First, we propose a semantic definition of purity, inspired by contextual equivalence, as a baseline independent of any specific typing discipline. Second, we propose that expressiveness should be measured by the degree of completeness, i.e., how many semantically pure terms can be typed as pure. Using this measure, we focus on minimal meaningful effect and capability systems and show that they are incomparable, i.e., neither subsumes the other in terms of expressiveness. Based on this result, we propose a synthesis and show that type, ability, and effect systems combine their respective strengths while avoiding their weaknesses. As part of our formal model, we provide a logical relation to facilitate proofs of purity and other properties for a variety of effect typing disciplines.

Paper Structure

This paper contains 70 sections, 17 theorems, 28 equations, 14 figures.

Table of Contents

  1. Introduction
  2. Maximizing Mathematical Reasoning
  3. Stateful Physical Reality
  4. Monads, Effects, Capabilities
  5. Challenges and Limitations
  6. Contributions
  7. Semantics of Effects and Purity
  8. Expressiveness of Effect Typing Disciplines
  9. Intuitive Definitions of Purity
  10. Pure Functions, Pure Ability
  11. A Semantic Definition of Purity
  12. Formalizing A Notion of Observational Purity
  13. Syntax and Semantics
  14. Observational Equivalence
  15. Observational Purity
  16. ...and 55 more sections

Key Result

theorem 1

If $\Gamma^{e} \vdash_e t : T^{e}\ \textcolor{red}{e}$, then $\Gamma^{e} \models_e t \mathrel{\approx_{\text{log}}}_{\textcolor{red}{e}} t : T^{e}\ \textcolor{red}{e}$.

Figures (14)

  • Figure 1: Examples illustrating intuitively pure and impure terms ($a$ refers to a mutable reference).
  • Figure 2: Examples illustrating intuitively pure and impure functions (which are all pure terms here, but could be the result of an impure computation), and the concept of ability or potential of a value: namely, to be the source of impure behavior when put in a specific context. Values with impure ability are what we intuitively understand as capabilities.
  • Figure 3: Syntax and Semantics.
  • Figure 4: Effect Type System $\lambda_e$.
  • Figure 5: Computing free variables of a given term (standard).
  • ...and 9 more figures

Theorems & Definitions (26)

  • definition 1: Pure Function -- Informal
  • definition 2: Pure-Ability Function -- Informal
  • definition 3: Operational Equivalence
  • definition 4: Observational Equivalence
  • definition 5: Observational Purity
  • theorem 1: Fundamental Property
  • theorem 2: Contextual Equivalence
  • theorem 3: Effect Safety of Effect Type System
  • theorem 4: Reordering
  • theorem 5: Fundamental Property
  • ...and 16 more