文章基本信息

标题：Model-View-Update-Communicate: Session Types Meet the Elm Architecture
本地全文：下载
作者：Simon Fowler
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：166
页码：1-28
DOI：10.4230/LIPIcs.ECOOP.2020.14
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Session types; concurrent programming; Model-View-Update