Model-View-Update-Communicate: Session Types meet the Elm Architecture

TL;DR

This paper introduces a formal model combining session types with the Elm architecture for GUI development, enabling safe communication protocols in graphical applications, demonstrated through web examples.

Contribution

It presents the first formal integration of session types with GUI programming using the MVU architecture, extending the model with commands, linearity, and model transitions.

Findings

Formal model of MVU architecture proved sound

Implementation in Links language with practical examples

First integration of session types with GUI development

Abstract

Session types are a type discipline for communication channel endpoints which allow conformance to protocols to be checked statically. Safely implementing session types requires linearity, usually in the form of a linear type system. Unfortunately, linear typing is difficult to integrate with graphical user interfaces (GUIs), and to date most programs using session types are command line applications. In this paper, we propose the first principled integration of session typing and GUI development by building upon the Model-View-Update (MVU) architecture, pioneered by the Elm programming language. We introduce $\lambda_{\textsf{MVU}}$, the first formal model of the MVU architecture, and prove it sound. By extending $\lambda_{\textsf{MVU}}$ with \emph{commands} as found in Elm, along with \emph{linearity} and \emph{model transitions}, we show the first formal integration of session typing and GUI programming. We implement our approach in the Links web programming language, and show examples including a two-factor authentication workflow and multi-room chat server.