Wormholes: Introducing Effects to FRP
📜 Abstract
Functional reactive programming (FRP) is a useful model for programming real-time and reactive systems in which one defines a signal function to process a stream of input values into a stream of output values. However, performing side effects (e.g. memory mutation or input/output) in this model is tricky and typically unsafe. In previous work, Winograd-Cort et al. [2012] introduced resource types and wormholes to address this problem. This paper better motivates, expands upon, and formalizes the notion of a wormhole to fully unlock its potential. We show, for example, that wormholes can be used to define the concept of causality. This in turn allows us to provide behaviors such as looping, a core component of most languages, without building it directly into the language. We also improve upon our previous design by making wormholes less verbose and easier to use. To formalize the notion of a wormhole, we define an extension to the simply typed lambda calculus, complete with typing rules and operational semantics. In addition, we present a new form of semantic transition that we call a temporal transition to specify how an FRP program behaves over time and to allow us to better reason about causality. As our model is designed for a Haskell implementation, the semantics are lazy. Finally, with the language defined, we prove that our wormholes indeed allow side effects to be performed safely in an FRP framework.
✨ Summary
Paper summary
The paper introduces wormholes, a mechanism for controlled side effects and non-local communication in arrow-based functional reactive programming. A wormhole is split into a read endpoint, called a whitehole, and a write endpoint, called a blackhole. Resource types ensure that each endpoint is used at most once, preventing conflicting access to physical or virtual resources.
The authors formalize the system as an extension of the simply typed lambda calculus with products, resource-typed signal functions, resource interaction, and dynamically created virtual resources. Its operational semantics separates ordinary lazy evaluation, instantaneous signal-function execution, and a temporal transition that advances the program one time step. The temporal model ensures that reads observe values from the previous step, thereby enforcing causality.
A significant result is that causal looping and delay can be constructed from wormholes rather than provided as primitive language features. The paper proves resource safety: a well-typed signal function accesses only resources listed in its type and interacts with each such resource at most once per time step. The theoretical design supports dynamic wormhole creation, although the authors identify limitations in implementing the full type-level resource-set machinery in Haskell.
Subsequent influence
The clearest later research extension is Functional Reactive Programming with Effects, A More Permissive Approach by Dabrowski and Ischard, which explicitly extends WORMHOLES, relaxes its single-use restriction for internal resources, and provides a translation back to effect-free Yampa programs. (arxiv.org) The original authors also continued this line of FRP research in their 2014 work on settable and non-interfering signal functions, which targets broader static optimization opportunities for arrowized FRP. (danwc.com) A later Coq-oriented formalization project separately identifies Wormholes as a language to formalize and studies subsets of its semantics. (univ-orleans.fr)
I found no reliable evidence of documented industry adoption or production-system use of the specific wormhole mechanism.