Document Open Access Logo

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

Author Simon Fowler

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2020.14.pdf
  • Filesize: 0.81 MB
  • 28 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Software and its engineering → Concurrent programming languages
Keywords
  • Session types
  • concurrent programming
  • Model-View-Update

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Simon Fowler. Model-View-Update-Communicate: Session Types Meet the Elm Architecture. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 14:1-14:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ECOOP.2020.14

Author Details

Simon Fowler
  • University of Edinburgh, United Kingdom

Funding

This work was supported by ERC Consolidator Grant Skye (grant no. 682315) and an ISCF Metrology Fellowship grant provided by the UK government’s Department for Business, Energy and Industrial Strategy (BEIS).

Acknowledgements

I thank Jake Browning for sparking my interest in Elm and for his help with an early prototype of the Links MVU library; Sára Decova for a previous version of the multi-room chat server example; Sam Lindley for many useful discussions and suggestions; and James Cheney, April Gonçalves, and the anonymous ECOOP PC and AEC reviewers for detailed comments.

Supplementary Materials

References

  1. Elm: A delightful language for reliable webapps, 2019. Accessed on 2019-07-04. URL: http://www.elm-lang.org.
  2. React - a JavaScript library for building user interfaces, 2019. Accessed on 2019-09-02. URL: http://www.reactjs.org.
  3. WebSharper.Mvu, 2019. Accessed on 2019-07-04. URL: https://github.com/dotnet-websharper/mvu.
  4. Flux, 2020. Accessed on 2020-01-08. URL: https://facebook.github.io/flux/.
  5. Redux - a predictable state container for JavaScript apps, 2020. Accessed on 2020-01-08. URL: https://redux.js.org/.
  6. Robert Atkey. Parameterised notions of computation. J. Funct. Program., 19(3-4):335-376, 2009. Google Scholar
  7. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR, volume 6269 of Lecture Notes in Computer Science, pages 222-236. Springer, 2010. Google Scholar
  8. Iliano Cervesato and Frank Pfenning. A linear logical framework. In LICS, pages 264-275. IEEE Computer Society, 1996. Google Scholar
  9. Adam Chlipala. Ur/Web: A simple model for programming the web. In POPL, pages 153-165. ACM, 2015. Google Scholar
  10. Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. Links: Web programming without tiers. In FMCO, volume 4709 of Lecture Notes in Computer Science, pages 266-296. Springer, 2006. Google Scholar
  11. Evan Czaplicki. Farewell to FRP, 2016. Accessed on 2019-09-02. URL: https://elm-lang.org/news/farewell-to-frp.
  12. Evan Czaplicki and Stephen Chong. Asynchronous functional reactive programming for GUIs. In Hans-Juergen Boehm and Cormac Flanagan, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pages 411-422. ACM, 2013. URL: https://doi.org/10.1145/2491956.2462161.
  13. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. Inf. Comput., 256:253-286, 2017. Google Scholar
  14. Conal Elliott and Paul Hudak. Functional reactive animation. In ICFP, pages 263-273. ACM, 1997. Google Scholar
  15. Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. A functional I/O system or, fun for freshman kids. In ICFP, pages 47-58. ACM, 2009. Google Scholar
  16. Ian Fette and Alexey Melnikov. The WebSocket protocol, 2011. Google Scholar
  17. Robert Bruce Findler, John Clements, Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Paul Steckler, and Matthias Felleisen. DrScheme: a programming environment for Scheme. J. Funct. Program., 12(2):159-182, 2002. Google Scholar
  18. Simon Fowler. Model-View-Update-Communicate: Session types meet the Elm architecture (Extended version), 2019. URL: http://arxiv.org/abs/1910.11108.
  19. Simon Fowler, Loïc Denuzière, and Adam Granicz. Reactive single-page applications with dynamic dataflow. In PADL, volume 9131 of Lecture Notes in Computer Science, pages 58-73. Springer, 2015. Google Scholar
  20. Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. Exceptional asynchronous session types: session types without tiers. PACMPL, 3(POPL):28:1-28:29, 2019. URL: https://doi.org/10.1145/3290341.
  21. Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19-50, 2010. Google Scholar
  22. Ido Green. Web Workers - Multithreaded Programs in JavaScript. O'Reilly, 2012. Google Scholar
  23. Kohei Honda. Types for dyadic interaction. In CONCUR, volume 715 of Lecture Notes in Computer Science, pages 509-523. Springer, 1993. Google Scholar
  24. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP, volume 1381 of Lecture Notes in Computer Science, pages 122-138. Springer, 1998. Google Scholar
  25. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1-9:67, 2016. Google Scholar
  26. Anupam Jain. Concur, 2019. Accessed on 2019-09-02. URL: https://ajnsit.github.io/concur.
  27. Jonathan King, Nicholas Ng, and Nobuko Yoshida. Multiparty session type-safe web development with static linearity. In PLACES@ETAPS, volume 291 of EPTCS, pages 35-46, 2019. Google Scholar
  28. Naoki Kobayashi. Type systems for concurrent programs. In 10th Anniversary Colloquium of UNU/IIST, volume 2757 of Lecture Notes in Computer Science, pages 439-453. Springer, 2002. Google Scholar
  29. Naoki Kobayashi. A new type system for deadlock-free processes. In CONCUR, volume 4137 of Lecture Notes in Computer Science, pages 233-247. Springer, 2006. Google Scholar
  30. Glenn E. Krasner and Stephen T. Pope. A Cookbook for using the Model-view Controller user interface paradigm in Smalltalk-80. J. Object Oriented Program., 1(3):26-49, August 1988. URL: http://dl.acm.org/citation.cfm?id=50757.50759.
  31. Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In ESOP, volume 9032 of Lecture Notes in Computer Science, pages 560-584. Springer, 2015. Google Scholar
  32. Sam Lindley and J. Garrett Morris. Talking bananas: structural recursion for session types. In ICFP, pages 434-447. ACM, 2016. Google Scholar
  33. Sam Lindley and J Garrett Morris. Lightweight functional session types. Behavioural Types: from Theory to Tools. River Publishers, pages 265-286, 2017. Google Scholar
  34. Leo A. Meyerovich, Arjun Guha, Jacob P. Baskin, Gregory H. Cooper, Michael Greenberg, Aleks Bromfield, and Shriram Krishnamurthi. Flapjax: a programming language for Ajax applications. In OOPSLA, pages 1-20. ACM, 2009. Google Scholar
  35. Dimitris Mostrous and Vasco T. Vasconcelos. Affine sessions. Logical Methods in Computer Science, 14(4), 2018. URL: https://doi.org/10.23638/LMCS-14(4:14)2018.
  36. Joachim Niehren, Jan Schwinghammer, and Gert Smolka. A concurrent lambda calculus with futures. Theor. Comput. Sci., 364(3):338-356, 2006. Google Scholar
  37. Luca Padovani. Deadlock and lock freedom in the linear π-calculus. In CSL-LICS, pages 72:1-72:10. ACM, 2014. Google Scholar
  38. Luca Padovani. Context-free session type inference. In ESOP, volume 10201 of Lecture Notes in Computer Science, pages 804-830. Springer, 2017. Google Scholar
  39. Luca Padovani and Luca Novara. Types for deadlock-free higher-order programs. In FORTE, volume 9039 of Lecture Notes in Computer Science, pages 3-18. Springer, 2015. Google Scholar
  40. Adam Pedley. Functional Model-View-Update Architecture for Flutter, 2019. Accessed on 2019-09-24. URL: https://buildflutter.com/functional-model-view-update-architecture-for-flutter/.
  41. Manuel Serrano and Vincent Prunet. A glimpse of Hopjs. In ICFP, pages 180-192. ACM, 2016. Google Scholar
  42. The PureScript Contributors. PureScript, 2019. Accessed on 2019-09-02. URL: http://www.purescript.org/.
  43. Vasco T. Vasconcelos. Fundamentals of session types. Inf. Comput., 217:52-70, 2012. Google Scholar
  44. Philip Wadler. Linear types can change the world! In Programming Concepts and Methods, page 561. North-Holland, 1990. Google Scholar
  45. Philip Wadler. Propositions as sessions. J. Funct. Program., 24(2-3):384-418, 2014. URL: https://doi.org/10.1017/S095679681400001X.
  46. Pascal Weisenburger, Mirko Köhler, and Guido Salvaneschi. Distributed system development with ScalaLoci. PACMPL, 2(OOPSLA):129:1-129:30, 2018. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact