Functional reactive programming in Elm

FRP can be defined as a λ-calculus that admits temporal types, i.e. types given by a propositional intuitionistic linear-time temporal logic (LTL). Although the Elm language uses only a subset of LTL, it achieves high expressivity for GUI programming. I will formally define the operational semantics of Elm. I discuss the current limitations of Elm and outline possible extensions. I also review the connections between temporal logic, FRP, and Elm.

[sergeiwinitzki]

Causality is maintained in Elm due to the fact that the only temporal primitives are "map2" and "foldp", which explicitly preserve causality.

[sergeiwinitzki]

3. When describing the semantics of "async" around 58:00, I should have said that the delayed update U_{i<-c'} of the signal "i" should be scheduled to apply not to the expression "async e" alone, but again to the entire Elm program being run.

[sergeiwinitzki]

This talk and the discussion happened on April 13, 2015, at the "SF Types, Theorems, and Programming Languages" meetup.

[sergeiwinitzki]

My most recent talk about functional reactive programming. I presented this at "SF Types, Theorems, and Programming Languages", which is the best computer science meetup in downtown SF.

[sergeiwinitzki]

The discussion following the talk uncovered two mistakes I made during the presentation.

1. I said that my notation for the semantics of Elm is perhaps not ideal, and Ian asked what semantics was used in the original papers published on Elm. I then said that no formal semantics was defined in those original papers. This is incorrect; although the original authors did not define a formal semantics in a concise notation (as I attempted to do in my talk), they gave a translation from Elm to Standard ML with message-passing concurrency. This translation is not easy to understand by reading the code, but, of course, it defines a semantics for Elm in a precise way.

2. Around 1:34:00 I was asked by Ian and Charles about the precise semantics of "foldp" during an update on another signal: according to my semantics, *every* signal updates whenever some signal updates, so the question is, whether "foldp" will execute another update in that case. In the formal semantics I presented, this would be the case. However, this is not the semantics of "foldp" as originally intended and as actually implemented in Elm. In order to represent this semantics correctly, I would have to refine my notation to include two versions of "current values": one that is updated, and one that is merely carried over from the previous current value of the signal. Evan Czaplicki's paper mentions that the Elm runtime caches the signals intelligently and represents current values as either NoChange or Update. It appears to be necessary to reflect this in the formal semantics (which my slides don't).

[JeffSmits]

Elm handles recursion on functions just fine. Recursion on values is impossible because Elm has a strict semantics, so you need functions for non-strictness.