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

Simon Fowler

doi:10.4230/LIPIcs.ECOOP.2020.14

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

Simon Fowler

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 λ_MVU, the first formal model of the MVU architecture, and prove it sound. By extending λ_MVU with commands as found in Elm, along with linearity and 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.

Original language	English
Title of host publication	34th European Conference on Object-Oriented Programming (ECOOP 2020)
Editors	Robert Hirschfeld, Tobias Pape
Publisher	Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany
Pages	14:1 - 14:28
Number of pages	28
ISBN (Electronic)	978-3-95977-154-2
DOIs	https://doi.org/10.4230/LIPIcs.ECOOP.2020.14
Publication status	Published - 6 Nov 2020
Event	European Conference on Object-Oriented Programming 2020 - Berlin, Germany Duration: 13 Jul 2020 → 17 Jul 2020 https://2020.ecoop.org/

Publication series

Name	Leibniz International Proceedings in Informatics (LIPIcs)
Publisher	Schloss Dagstuhl--Leibniz-Zentrum für Informatik
Volume	166
ISSN (Electronic)	1868-8969

Conference

Conference	European Conference on Object-Oriented Programming 2020
Abbreviated title	ECOOP 2020
Country/Territory	Germany
City	Berlin
Period	13/07/20 → 17/07/20
Internet address	https://2020.ecoop.org/

Keywords / Materials (for Non-textual outputs)

Session types
Concurrent programming
Model-View-Update

Access to Document

10.4230/LIPIcs.ECOOP.2020.14Licence: Creative Commons: Attribution (CC-BY)

Model-View-Update-Communicate_FOWLER_DOA08042020_AFVAccepted author manuscript, 752 KBLicence: Creative Commons: Attribution (CC-BY)
Model-View-Update-Communicate_FOWLER_DOA08042020_VOR_CC-BYFinal published version, 839 KBLicence: Creative Commons: Attribution (CC-BY)

Skye-A programming language bridging theory and practice for scientific data curation
Cheney, J. (Principal Investigator)
EU government bodies
1/09/16 → 28/02/23
Project: Research

Cite this

Fowler, S. (2020). Model-View-Update-Communicate: Session Types Meet the Elm Architecture. In R. Hirschfeld, & T. Pape (Eds.), 34th European Conference on Object-Oriented Programming (ECOOP 2020) (pp. 14:1 - 14:28). Article 14 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 166). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. https://doi.org/10.4230/LIPIcs.ECOOP.2020.14

@inproceedings{632bcbb4017d482d9d6952d518ae1759,

title = "Model-View-Update-Communicate: Session Types Meet the Elm Architecture",

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 λMVU, the first formal model of the MVU architecture, and prove it sound. By extending λMVU with commands as found in Elm, along with linearity and 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.",

keywords = "Session types, Concurrent programming, Model-View-Update",

author = "Simon Fowler",

year = "2020",

month = nov,

day = "6",

doi = "10.4230/LIPIcs.ECOOP.2020.14",

language = "English",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany",

pages = "14:1 -- 14:28",

editor = "Robert Hirschfeld and Tobias Pape",

booktitle = "34th European Conference on Object-Oriented Programming (ECOOP 2020)",

note = "European Conference on Object-Oriented Programming 2020, ECOOP 2020 ; Conference date: 13-07-2020 Through 17-07-2020",

url = "https://2020.ecoop.org/",

}

Fowler, S 2020, Model-View-Update-Communicate: Session Types Meet the Elm Architecture. in R Hirschfeld & T Pape (eds), 34th European Conference on Object-Oriented Programming (ECOOP 2020)., 14, Leibniz International Proceedings in Informatics (LIPIcs), vol. 166, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, pp. 14:1 - 14:28, European Conference on Object-Oriented Programming 2020, Berlin, Berlin, Germany, 13/07/20. https://doi.org/10.4230/LIPIcs.ECOOP.2020.14

Model-View-Update-Communicate: Session Types Meet the Elm Architecture. / Fowler, Simon.
34th European Conference on Object-Oriented Programming (ECOOP 2020). ed. / Robert Hirschfeld; Tobias Pape. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2020. p. 14:1 - 14:28 14 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 166).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Model-View-Update-Communicate: Session Types Meet the Elm Architecture

AU - Fowler, Simon

PY - 2020/11/6

Y1 - 2020/11/6

N2 - 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 λMVU, the first formal model of the MVU architecture, and prove it sound. By extending λMVU with commands as found in Elm, along with linearity and 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.

AB - 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 λMVU, the first formal model of the MVU architecture, and prove it sound. By extending λMVU with commands as found in Elm, along with linearity and 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.

KW - Session types

KW - Concurrent programming

KW - Model-View-Update

U2 - 10.4230/LIPIcs.ECOOP.2020.14

DO - 10.4230/LIPIcs.ECOOP.2020.14

M3 - Conference contribution

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 14:1 - 14:28

BT - 34th European Conference on Object-Oriented Programming (ECOOP 2020)

A2 - Hirschfeld, Robert

A2 - Pape, Tobias

PB - Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany

T2 - European Conference on Object-Oriented Programming 2020

Y2 - 13 July 2020 through 17 July 2020

ER -

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

Abstract

Publication series

Conference

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

Skye-A programming language bridging theory and practice for scientific data curation

Cite this