New Draft: Simple and Efficient Higher-Order Reactive Programming

I've got a new draft out Simple and Efficient Higher-Order Reactive Programming. Here's the abstract:

Functional reactive programming (FRP) is an elegant approach to declaratively specify reactive systems. However, the powerful abstractions of FRP have historically made it difficult to predict and control the resource usage of programs written in this style.

In this paper we give a simple type theory for higher-order functional reactive programming, as well as a natural implementation strategy for it. Our type theory simplifies and generalizes prior type systems for reactive programming. At the same time, we give a an efficient implementation strategy which eagerly deallocates old values, ruling out space and time leaks, two notorious sources of inefficiency in reactive programs. Our language neither restricts the expressive power of the FRP model, nor does it require a complex substructural type system to track the resource usage of programs.

We also show that for programs well-typed under our type system, our implementation strategy of eager deallocation is safe: we show the soundness of our type system under our implementation strategy, using a novel step-indexed Kripke logical relation.

Last year, Nick Benton, Jan Hoffmann, and I worked out how to control the space usage of FRP programs. Our techniques worked, but it required a rather complicated linear type discipline to make everything work. In this paper, I've worked out how to dramatically simplify the type system, make the language more expressive, use simpler implementation strategies, which also make it more efficient.

This is also basically the implementation strategy I am using in my AdjS compiler, which should see a release as soon as I add support for a few more type system features, and squash the soundness bugs the correctness proof in this paper revealed.