Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Functional Reactive Programming with Effects, A More Permissive Approach

Frédéric Dabrowski, Jordan Ischard

TL;DR

The paper tackles reconciling functional reactive programming with effectful resources by introducing Molholes, a permissive extension of Wormholes that separates input/output resources from internal ones and relaxes single-use constraints on internals.Its approach combines a rich semantic framework based on categories, functors/monads, and arrows with a two-layer YampaCore semantics and a Kleisli-style Molholes semantics, enabling formal reasoning about reactive programs with memoryful effects.Two key results underpin the contribution: a normal-form theorem for Molholes terms and a correctness theorem showing translation to equivalent YampaCore programs via bisimulation, preserving observable behavior.The work demonstrates that Molholes preserves the functional FRP semantics while enabling more flexible resource usage, offering a path toward practical, certified reactive programming in impure languages such as OCaml, with plans for Coq formalization and extraction of certified code.

Abstract

We introduce a functional reactive programming language that extends WORMHOLES, an enhancement of YAMPA with support for effects. Our proposal relaxes the constraint in WORMHOLES that restricts all resources to single-use. Resources are categorized into two kinds: input/output resources and internal resources. Input/output resources model interactions with the environment and follow constraints similar to those in WORMHOLES. Internal resources, on the other hand, enable communication between program components and can be used multiple times. We demonstrate that programs written in our language can be translated into equivalent effect-free YAMPA programs, ensuring that our approach remains compatible with existing functional reactive paradigms.

Functional Reactive Programming with Effects, A More Permissive Approach

TL;DR

The paper tackles reconciling functional reactive programming with effectful resources by introducing Molholes, a permissive extension of Wormholes that separates input/output resources from internal ones and relaxes single-use constraints on internals.Its approach combines a rich semantic framework based on categories, functors/monads, and arrows with a two-layer YampaCore semantics and a Kleisli-style Molholes semantics, enabling formal reasoning about reactive programs with memoryful effects.Two key results underpin the contribution: a normal-form theorem for Molholes terms and a correctness theorem showing translation to equivalent YampaCore programs via bisimulation, preserving observable behavior.The work demonstrates that Molholes preserves the functional FRP semantics while enabling more flexible resource usage, offering a path toward practical, certified reactive programming in impure languages such as OCaml, with plans for Coq formalization and extraction of certified code.

Abstract

We introduce a functional reactive programming language that extends WORMHOLES, an enhancement of YAMPA with support for effects. Our proposal relaxes the constraint in WORMHOLES that restricts all resources to single-use. Resources are categorized into two kinds: input/output resources and internal resources. Input/output resources model interactions with the environment and follow constraints similar to those in WORMHOLES. Internal resources, on the other hand, enable communication between program components and can be used multiple times. We demonstrate that programs written in our language can be translated into equivalent effect-free YAMPA programs, ensuring that our approach remains compatible with existing functional reactive paradigms.

Paper Structure

This paper contains 27 sections, 18 theorems, 57 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Overview
  3. Yampa
  4. Wormholes
  5. Semantic Domains
  6. Categories
  7. Functors and Monads
  8. Arrows
  9. Bisimulations
  10. YampaCore
  11. Syntax and Semantics
  12. Normal form
  13. The Molholes language
  14. Syntax
  15. Dynamic semantics
  16. ...and 12 more sections

Key Result

Lemma 1

Let ${\mathit{sf}}$, ${\mathit{sf}}_{\!1}$, ${\mathit{sf}}_{\!1}'$, ${\mathit{sf}}_{\!2}$ and ${\mathit{sf}}_{\!2}'$ be signal functions and let $v$ be a value. The following properties hold:

Figures (6)

  • Figure 1: Equivalent programs in Yampa (top) and in Wormholes (bottom)
  • Figure 2: Graphical representation a ${\mathit{rsf}}$ term computation.
  • Figure 3: Graphical representation of resource accesses
  • Figure 4: Syntax of Molholes
  • Figure 5: Memory domain
  • ...and 1 more figures

Theorems & Definitions (36)

  • Lemma 1
  • proof
  • Theorem 1
  • proof
  • Lemma 2
  • proof
  • Theorem 2
  • proof
  • Example 1
  • Lemma 3
  • ...and 26 more