Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Typing Composable Coroutines

Qiqi Gu, Wei Ke

TL;DR

The paper addresses the challenge of reasoning about asynchronous coroutine behavior by introducing a dependent-type based coroutine type notation and a composition calculus that combines a list of coroutine types into a single, checkable type using a compose function $\bm{\circ}$. It defines a formal grammar for coroutine types, eight composition rules, and analyses of type complexity $N$, termination, and evaluation order, supported by proofs of soundness and multiple language-agnostic applications. Key contributions include a practical framework for modeling data flow through yielding and resuming across first-class, stackless coroutines, plus concrete demonstrations in Python, OCaml, and Prolog to illustrate how complex control-flow patterns (mapping, file I/O, pattern matching, and goal-driven proof) can be typed and composed. The work enables static type checking of coroutine groups in single-threaded schedules and lays the groundwork for integrating coroutine typing into existing languages, with future directions toward polymorphism, inheritance, and deeper type-narrowing capabilities.

Abstract

Coroutine, as a powerful programming construct, is widely used in asynchronous applications to replace thread-based programming or the callback hell. Using coroutines makes code more readable and maintainable, for its ability to transfer control while keeping the literal scope. However, reasoning about coroutine behavior can be challenging without proper typing. We propose a type notation and calculus for composing asymmetric, first-class, stackless coroutines. Given the types of a list of coroutines, we can compute a composed type matching the collective behavior of the coroutines, so that the input and output can be type-checked by a type system. Our coroutine types can model the data received by or yielded from a coroutine, which be of coroutine types as well. On top of our type calculus, we discuss its soundness and evaluation issues, then provide four application scenarios of our coroutine types. Not only can our types be used in modern programming languages, such as Python, but also model program behaviors in OCaml and even Prolog.

Typing Composable Coroutines

TL;DR

The paper addresses the challenge of reasoning about asynchronous coroutine behavior by introducing a dependent-type based coroutine type notation and a composition calculus that combines a list of coroutine types into a single, checkable type using a compose function . It defines a formal grammar for coroutine types, eight composition rules, and analyses of type complexity , termination, and evaluation order, supported by proofs of soundness and multiple language-agnostic applications. Key contributions include a practical framework for modeling data flow through yielding and resuming across first-class, stackless coroutines, plus concrete demonstrations in Python, OCaml, and Prolog to illustrate how complex control-flow patterns (mapping, file I/O, pattern matching, and goal-driven proof) can be typed and composed. The work enables static type checking of coroutine groups in single-threaded schedules and lays the groundwork for integrating coroutine typing into existing languages, with future directions toward polymorphism, inheritance, and deeper type-narrowing capabilities.

Abstract

Coroutine, as a powerful programming construct, is widely used in asynchronous applications to replace thread-based programming or the callback hell. Using coroutines makes code more readable and maintainable, for its ability to transfer control while keeping the literal scope. However, reasoning about coroutine behavior can be challenging without proper typing. We propose a type notation and calculus for composing asymmetric, first-class, stackless coroutines. Given the types of a list of coroutines, we can compute a composed type matching the collective behavior of the coroutines, so that the input and output can be type-checked by a type system. Our coroutine types can model the data received by or yielded from a coroutine, which be of coroutine types as well. On top of our type calculus, we discuss its soundness and evaluation issues, then provide four application scenarios of our coroutine types. Not only can our types be used in modern programming languages, such as Python, but also model program behaviors in OCaml and even Prolog.
Paper Structure (16 sections, 5 theorems, 25 equations, 9 figures)

This paper contains 16 sections, 5 theorems, 25 equations, 9 figures.

Table of Contents

  1. Introduction
  2. Syntax of Coroutine Types
  3. Composition Rules
  4. Yielding
  5. Resuming
  6. Soundness
  7. Type Complexity
  8. Termination of Evaluation
  9. Evaluation Order
  10. Applications
  11. Mapping in Python
  12. Reading files in Python
  13. Pattern Matching
  14. Prolog Proof
  15. Related Work
  16. ...and 1 more sections

Key Result

Proposition 1

When the applied rules are yield (Rule eq:yield) and resume (Rule eq:resume), we assume the complexity of the yielded type is $x$ and let $E'$ and $\Theta'$ be the states after the transition, then the following condition in Hoare Logic holds.

Figures (9)

  • Figure 1: Abstract syntax of coroutine types
  • Figure 2: Definition of head ${\mathbf{h}}$ and tail ${\mathbf{t}}$ of a type
  • Figure 3: Definition of $\mathbf{match}$ for matching two types.
  • Figure 4: function $\mathbf{N}$ measures complexity of types
  • Figure 5: Both $\Theta$ and $E$ stay the same
  • ...and 4 more figures

Theorems & Definitions (7)

  • Proposition 1
  • proof
  • Proposition 2
  • proof
  • Proposition 3
  • Proposition 4
  • Proposition 5