Model-View-Update-Communicate: Session Types meet the Elm Architecture
share
The Elm programming language pioneers the Model-View-Update (MVU) architecture for writing web applications in a functional style. Although popular amongst developers, MVU has not been studied formally; it is therefore difficult to reason about any extensions, and each implementer must re-discover the essence of the architecture. In this paper we introduce λ_MVU, a formal model of the MVU architecture as a concurrent λ-calculus, and prove its correctness. We extend λ_MVU with subscriptions and commands as found in Elm. By further extending the calculus with linearity and model transitions, we provide the first formal integration of session-typed communication with a GUI framework. We implement our approach in the Links web programming language, and show examples including a two-factor authentication workflow and multi-room chat server.
READ FULL TEXT