Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Direct-Style Effect Notation for Sequential and Parallel Programs

David Richter, Timon Böhler, Pascal Weisenburger, Mira Mezini

TL;DR

This work introduces a direct-style mixed applicative/monadic notation that preserves parallelism inherent in code structure while allowing sequential effects where necessary. It provides a one-pass translation from direct-style to a language of effect combinators ($Pure$, $Bind$, $Ap$) and proves that this translation preserves typability, semantics, and parallelism, with a Coq mechanisation based on PHOAS and intrinsically typed terms. The authors also implement the approach in Scala using macros, enabling a practical, type-preserving compilation path from mixed direct-style code to mixed monadic/applicative programs. By treating parallelism as a property derived from program structure (span and work), the method offers a principled, verifiable route to optimizing effectful code without sacrificing correctness. The work lays groundwork for richer language features and broader effect systems, while demonstrating concrete gains in parallelism preservation and reasoning about correctness.

Abstract

Modeling sequential and parallel composition of effectful computations has been investigated in a variety of languages for a long time. In particular, the popular do-notation provides a lightweight effect embedding for any instance of a monad. Idiom bracket notation, on the other hand, provides an embedding for applicatives. First, while monads force effects to be executed sequentially, ignoring potential for parallelism, applicatives do not support sequential effects. Composing sequential with parallel effects remains an open problem. This is even more of an issue as real programs consist of a combination of both sequential and parallel segments. Second, common notations do not support invoking effects in direct-style, instead forcing a rigid structure upon the code. In this paper, we propose a mixed applicative/monadic notation that retains parallelism where possible, but allows sequentiality where necessary. We leverage a direct-style notation where sequentiality or parallelism is derived from the structure of the code. We provide a mechanisation of our effectful language in Coq and prove that our compilation approach retains the parallelism of the source program.

A Direct-Style Effect Notation for Sequential and Parallel Programs

TL;DR

This work introduces a direct-style mixed applicative/monadic notation that preserves parallelism inherent in code structure while allowing sequential effects where necessary. It provides a one-pass translation from direct-style to a language of effect combinators (, , ) and proves that this translation preserves typability, semantics, and parallelism, with a Coq mechanisation based on PHOAS and intrinsically typed terms. The authors also implement the approach in Scala using macros, enabling a practical, type-preserving compilation path from mixed direct-style code to mixed monadic/applicative programs. By treating parallelism as a property derived from program structure (span and work), the method offers a principled, verifiable route to optimizing effectful code without sacrificing correctness. The work lays groundwork for richer language features and broader effect systems, while demonstrating concrete gains in parallelism preservation and reasoning about correctness.

Abstract

Modeling sequential and parallel composition of effectful computations has been investigated in a variety of languages for a long time. In particular, the popular do-notation provides a lightweight effect embedding for any instance of a monad. Idiom bracket notation, on the other hand, provides an embedding for applicatives. First, while monads force effects to be executed sequentially, ignoring potential for parallelism, applicatives do not support sequential effects. Composing sequential with parallel effects remains an open problem. This is even more of an issue as real programs consist of a combination of both sequential and parallel segments. Second, common notations do not support invoking effects in direct-style, instead forcing a rigid structure upon the code. In this paper, we propose a mixed applicative/monadic notation that retains parallelism where possible, but allows sequentiality where necessary. We leverage a direct-style notation where sequentiality or parallelism is derived from the structure of the code. We provide a mechanisation of our effectful language in Coq and prove that our compilation approach retains the parallelism of the source program.
Paper Structure (45 sections, 10 theorems, 9 figures, 1 table)

This paper contains 45 sections, 10 theorems, 9 figures, 1 table.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Structure.
  4. Overview
  5. Monadic, Applicative, Mixed and Direct Style Notations
  6. Functors, Applicatives and Monads.
  7. Monadic Notation.
  8. Applicative Notation.
  9. Mixed Notation.
  10. Direct-Style Mixed Notation.
  11. Discussion
  12. Scaling.
  13. Sub-notations.
  14. From Laws to a Rewrite System
  15. Laws.
  16. ...and 30 more sections

Key Result

Theorem 1

The translation function takes a well-typed term and produces a well-typed term, i.e.,

Figures (9)

  • Figure 1: Optimised Translation.
  • Figure 2: Types.
  • Figure 3: Type denotation.
  • Figure 4: Labels and denotation.
  • Figure 5: Term and their denotation.
  • ...and 4 more figures

Theorems & Definitions (10)

  • Theorem 1: PURE preserves types
  • Lemma 2: AP respects semantics
  • Lemma 3: JOIN respects semantics
  • Lemma 4: relabel preserves semantics
  • Theorem 5: PURE preserves semantics
  • Lemma 6: AP respects span and work
  • Lemma 7: JOIN respects span and work
  • Lemma 8: com is effect-free
  • Lemma 9: relabeled terms remain effect-free
  • Theorem 10: PURE preserves span and work