Asynchronous functional reactive programming for GUIs

Asynchronous functional reactive programming for GUIs
Evan Czaplicki and Stephen Chong
PLDI 2013 (see also http://elm-lang.org/)

This paper presents a new functional reactive programming-based programming language aimed at graphical user interaction (particularly on Web pages as embedded in Javascript).  Graphical user interaction has frequently been cited as a motivation for FRP techniques since the first work on it by Elliott and Hudak.  Early techniques had some significant performance problems, while more recent techniques have introduced restrictions or refinements that seek to reconcile convenient programming with efficiency.



This paper presents a new approach, that combines two basic ideas.  First, the type system is restricted to forbid forming "signal of signal" types, which rules out many (unintentionally) inefficient programs, by ensuring that the current value of a signal cannot depend on unbounded history.  (Other recent work on FRP at ICFP, which I discussed here, also provides ways to avoid this.)  Second, the language includes a primitive called $\mathsf{async}$ that marks parts of the program that can be executed asynchronously.  The language design, called FElm, is presented with a type system and its semantics is described via a translation to Concurrent ML.

Particularly interesting is the fact that the system in the paper forms the basis of a programming language called Elm with an active user community, and many interesting examples of short, nontrivial graphical interactive programs. On the other hand, I'd still like to see a significant development of a "real" user interface (something as complicated as the interactive editor that Blogger provides for me to write this post, for example) in a FRP-based language.

The paper doesn't present formal results that back up its claims (or correctness of the translation to Concurrent ML, for that matter).  So it is difficult to evaluate the claim that FElm is better than other approaches.  The prototype implementation is enough (for me at least) to convince me that this doesn't matter, though it would still be nice to see an attempt at a direct semantics for FElm and proof of its type soundness or other desirable properties (perhaps this is covered in a TR somewhere that I haven't seen).   Even a fairly lightweight specification such as showing the translation from FElm types to Concurrent ML types might be helpful for intuition.  In any case, Elm (and the core language presented in this paper) is an interesting design point and it is genuinely encouraging to see functional programming and FRP techniques influencing an emerging language.

Stray thoughts:

• The $\mathsf{lift}_n$ operations seem to make the $\mathsf{signal}$ type into an applicative functor (and vice versa, I think, at least based on the types).  It would be interesting to see whether $\mathsf{signal}$ "really" is an applicative functor in disguise.
• Formlets also satisfy applicative functor laws, and so if signals and formlets can both be formulated in terms of the same abstraction, maybe they can be combined more easily (applicative functors are closed under composition).
• On the other hand, the $\mathsf{fold}$ operation does not come along for free with an applicative functor; it seems to make explicit a limited kind of stateful or automaton-like transduction (this is made explicit by the $\mathtt{Automaton}$ type described in section 4.3, which comes from work on Arrowized FRP that I'm not familiar with).  
• Similarly, the $\mathtt{run}$ function in that section that maps an automaton $\mathtt{Automaton}~a~b$ and a start state $b$ to a function on signals $\mathsf{signal}~a\to \mathsf{signal}~b$ seems like it ought to be the basis of a functor from (some category based on) the $\mathtt{Automaton}$ type to the $\mathsf{signal}$ type.  Perhaps this is already explored in the Arrowized FRP literature on which the $\mathtt{Automaton}$ type is based, though.