Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Simplifying explicit subtyping coercions in a polymorphic calculus with effects

Filip Koprivec, Matija Pretnar

TL;DR

This paper tackles the performance cost of explicit subtyping coercions in a polymorphic, effectful calculus by introducing a structured, semantics-preserving simplification pipeline. It defines a CoreEff language with explicit dirt and coercions, develops a polarity-based framework to safely reduce type and dirt constraints, and proves denotational preservation of the simplifications. The authors implement the approach in Eff, showing that the simplified polymorphic code matches manually monomorphised performance across benchmarks while drastically reducing coercion parameters and monadic overhead. This work enables scalable, modular handling of algebraic effects without sacrificing efficiency, and it outlines concrete avenues for future refinement and broader applicability.

Abstract

Algebraic effect handlers are becoming an increasingly popular way of structuring effectful computations, and their performance is often a concern. One of the proposed approaches towards efficient compilation is tracking effect information through explicit subtyping coercions. However, in the presence of polymorphism, these coercions are compiled into additional arguments of compiled functions, incurring significant overhead. In this paper, we present a polymorphic effectful calculus, identify simplification phases needed to reduce the number of unnecessary constraints, and prove that they preserve semantics. In addition, we implement the simplification algorithm in the Eff language and evaluate its performance on a number of benchmarks. Though we do not prove the optimality of the presented simplifications, the results show that the algorithm eliminates all coercions, resulting in code as efficient as manually monomorphised one.

Simplifying explicit subtyping coercions in a polymorphic calculus with effects

TL;DR

This paper tackles the performance cost of explicit subtyping coercions in a polymorphic, effectful calculus by introducing a structured, semantics-preserving simplification pipeline. It defines a CoreEff language with explicit dirt and coercions, develops a polarity-based framework to safely reduce type and dirt constraints, and proves denotational preservation of the simplifications. The authors implement the approach in Eff, showing that the simplified polymorphic code matches manually monomorphised performance across benchmarks while drastically reducing coercion parameters and monadic overhead. This work enables scalable, modular handling of algebraic effects without sacrificing efficiency, and it outlines concrete avenues for future refinement and broader applicability.

Abstract

Algebraic effect handlers are becoming an increasingly popular way of structuring effectful computations, and their performance is often a concern. One of the proposed approaches towards efficient compilation is tracking effect information through explicit subtyping coercions. However, in the presence of polymorphism, these coercions are compiled into additional arguments of compiled functions, incurring significant overhead. In this paper, we present a polymorphic effectful calculus, identify simplification phases needed to reduce the number of unnecessary constraints, and prove that they preserve semantics. In addition, we implement the simplification algorithm in the Eff language and evaluate its performance on a number of benchmarks. Though we do not prove the optimality of the presented simplifications, the results show that the algorithm eliminates all coercions, resulting in code as efficient as manually monomorphised one.
Paper Structure (35 sections, 19 theorems, 88 equations, 11 figures, 3 tables)

This paper contains 35 sections, 19 theorems, 88 equations, 11 figures, 3 tables.

Table of Contents

  1. Overview
  2. Explicit effect subtyping
  3. Compiling to a pure language
  4. Explicit polymorphism
  5. Type constraint simplification
  6. Effect annotations
  7. Operations
  8. Language
  9. Types
  10. Coercions
  11. Terms
  12. Substitutions
  13. Valid substitutions
  14. A canonical form of contexts
  15. Polarity
  16. ...and 20 more sections

Key Result

Proposition 3.1

For an arbitrary valid substitution $\vdash_{{ \space\mathtt{}}} \sigma : \Xi \Rightarrow \Xi'$, the following holds:

Figures (11)

  • Figure 1: Well-formedness rules for types
  • Figure 2: Coercion well-formedness rules
  • Figure 3: CoreEff typing rules
  • Figure 4: Substitution validity rules
  • Figure 5: Substitution action on skeletons, dirt, and types
  • ...and 6 more figures

Theorems & Definitions (32)

  • Proposition 3.1
  • Proposition 3.2
  • Proposition 3.3
  • Theorem 3.4
  • Proposition 3.5
  • Proposition 3.6
  • proof
  • Definition 4.1
  • Proposition 4.2
  • Definition 4.3
  • ...and 22 more