Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Signature Restriction for Polymorphic Algebraic Effects

Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi

TL;DR

This paper tackles the classical problem of safely combining polymorphic effects with polymorphic type assignment by introducing signature restriction, which constrains how the type variables in an operation's signature may occur. Using algebraic effects and handlers, it proves that safety is preserved when all operations satisfy this restriction, and it develops two complementary type systems—a Curry-style System F-based polymorphic system and a polymorphic type-and-effect system—to allow mixing of safe and potentially unsafe polymorphic effects within a single program. The authors extend the core calculus with products, sums, and lists, provide an interpreter for a decidable subset (let-polymorphism), and relate the approach to the relaxed value restriction. Overall, the work offers a direct, sound framework for modularly reasoning about polymorphic effects and their interfaces, with practical implications for languages that support user-defined effects and dynamic control flow.

Abstract

The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment. A novelty of our work lies in finding a restriction on effect interfaces. To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction, a new notion to restrict the type signatures of operations, and show that signature restriction is sufficient to ensure type safety of an effectful language equipped with unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both operations that satisfy and do not satisfy the signature restriction in a single program.

Signature Restriction for Polymorphic Algebraic Effects

TL;DR

This paper tackles the classical problem of safely combining polymorphic effects with polymorphic type assignment by introducing signature restriction, which constrains how the type variables in an operation's signature may occur. Using algebraic effects and handlers, it proves that safety is preserved when all operations satisfy this restriction, and it develops two complementary type systems—a Curry-style System F-based polymorphic system and a polymorphic type-and-effect system—to allow mixing of safe and potentially unsafe polymorphic effects within a single program. The authors extend the core calculus with products, sums, and lists, provide an interpreter for a decidable subset (let-polymorphism), and relate the approach to the relaxed value restriction. Overall, the work offers a direct, sound framework for modularly reasoning about polymorphic effects and their interfaces, with practical implications for languages that support user-defined effects and dynamic control flow.

Abstract

The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the other for restricting how they are implemented. This work explores a new approach to ensuring the safety of polymorphic effects in polymorphic type assignment. A novelty of our work lies in finding a restriction on effect interfaces. To formalize our idea, we employ algebraic effects and handlers, where an effect interface is given by a set of operations coupled with type signatures. We propose signature restriction, a new notion to restrict the type signatures of operations, and show that signature restriction is sufficient to ensure type safety of an effectful language equipped with unrestricted polymorphic type assignment. We also develop a type-and-effect system to enable the use of both operations that satisfy and do not satisfy the signature restriction in a single program.

Paper Structure

This paper contains 12 sections, 3 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Background: Polymorphic Type Assignment with Computational Effects
  3. Our Work
  4. Organization.
  5. Overview
  6. Review: Algebraic Effects and Handlers
  7. Typechecking.
  8. Polymorphic Effects
  9. (Naive) Polymorphic Typechecking and Its Unsoundness
  10. Our Work: Signature Restriction
  11. A $\lambda$-Calculus with Algebraic Effects and Handlers
  12. Syntax

Figures (1)

  • Figure 1: Syntax of $\lambda_\text{eff}$.