Appendix E. Denotational semantics of Sodium
This document is the formal specification of the semantics of Sodium, an FRP system based on the concepts from Conal Elliott’s paper “Push-Pull FRP.” The code in this document is in Haskell, and a basic knowledge of Haskell is required to understand it. Most readers won’t need this information, but people interested in FRP semantics and developers of FRP systems will find it useful. Note that this has nothing to do with the Haskell implementation of Sodium. The executable version of this specification can be found at https://github.com/SodiumFRP/sodium/blob/master/denotational/.
- 1.0 (19 May 2015)—First version
- 1.1 (24 July 2015)—The times for streams changed to increasing instead of nondecreasing so that multiple events per time are no longer representable
- 1.1 (8 Oct 2015, 26 Apr 2016)—Minor corrections; no semantic change
Sodium has two data types:
- Stream a—A sequence of events, equivalent to Conal’s Event
- Cell a—A value that changes over time, equivalent to Conal’s Behavior
We replace Conal’s term event occurrence with event.