Lambda the Ultimate

Functional Reactive Programming (FRP) is a form of reactive programming whose model is pure functions over signals. FRP is often expressed in terms of arrows with loops, which is the type class for a Freyd category (that is a premonoidal category with a cartesian centre) equipped with a premonoidal trace. This type system suffices to define the dataflow structure of a reactive program, but does not express its temporal properties. In this paper, we show that Linear-time Temporal Logic (LTL) is a natural extension of the type system for FRP, which constrains the temporal behaviour of reactive programs. We show that a constructive LTL can be defined in a dependently typed functional language, and that reactive programs form proofs of constructive LTL properties. In particular, implication in LTL gives rise to stateless functions on streams, and the “constrains” modality gives rise to causal functions. We show that reactive programs form a partially traced monoidal category, and hence can be given as a form of arrows with loops, where the type system enforces that only decoupled functions can be looped.

As I'm sure most people here are aware Adobe announced they are discontinuing developing the Flash plugin (player) for mobile devices. Mike Chambers, Principal Product Manager for developer relations for the Flash Platform at Adobe, listed a variety of reasons for this in his explanatory post (link). Most are business and consumer oriented. One thing I thought might be of interest to LtU readers is the technical issues they faced on the mobile platform. Because performance was critical on mobile devices (minimizing data usage, handling low CPU and reducing power usage) Adobe ended up having to work specifically with:

1. Mobile Operating System Vendors (such as Google and RIM)
2. Hardware Device Manufacturers (such as Motorola and Samsung)
3. Component Manufacturers (such as NVIDIA)

They were building a specific version of the pluggin for each: OS/Device/GPU combination, and that was the cost that made the player a money loser. To me what Adobe faced seems like a classic interpreter language problem. So I figure I'd bring this up: Is it possible to design an interpreter optimized for video playback and vector graphics that makes heavy use of hardware specific advantages (like video decoding hardware or vector computations on the GPU and not the CPU), and abstracts different input methods (think hover on mouseover abstracted for touchscreen input). That is a flexible and configurable interpreter building system capable of support low level libraries. What does the FP community have that does something like this or at least is a prototype?

While there exist good HTML5 solutions for video (H.264 in hardware for example), I don't know of anything that can really take the place of Flash for vector graphics. Further the hardware issues that Adobe faced simply pass up to each website under HTML5 schemes. There are other business reasons, like the DRM, Flash enables control of the user experience which prevents people "skipping the ads" in video. So I think this is now a wide open opportunity until some other technology fills it.