MobilityReadingGroup

Multiparty Session Type-safe Web Development with Static Linearity

Jonathan KING, Nicholas NG, Nobuko YOSHIDA

Modern web applications can now offer desktop-like experiences from within the browser, thanks to technologies such as WebSockets, which enable low-latency duplex communication between the browser and the server. While these advances are great for the user experience, they represent a new responsibility for web developers who now need to manage and verify the correctness of more complex and potentially stateful interactions in their application. In this paper, we present a technique for developing interactive web applications that are statically guaranteed to communicate following a given protocol. First, the global interaction protocol is described in the Scribble protocol language – based on multiparty session types. Scribble protocols are checked for well-formedness, and then each role is projected to a Finite State Machine representing the structure of communication from the perspective of the role. We use source code generation and a novel type-level encoding of FSMs using multi-parameter type classes to leverage the type system of the target language and guarantee only programs that communicate following the protocol will type check. Our work targets PureScript – a functional language that compiles to JavaScript – which crucially has an expressive enough type system to provide static linearity guarantees. We demonstrate the effectiveness of our approach through a web-based Battleship game where communication is performed through WebSocket connections.

@inproceedings{KNY2019,
  author = {Jonathan King and Nicholas Ng and Nobuko Yoshida},
  title = {{Multiparty Session Type-safe Web Development with Static Linearity}},
  booktitle = {Programming Language Approaches to Concurrency and Communication-cEntric Software},
  volume = {291},
  pages = {35--46},
  publisher = {Open Publishing Association},
  year = 2019
}

@inproceedings{KNY2019,
  author = {Jonathan King and Nicholas Ng and Nobuko Yoshida},
  title = {{Multiparty Session Type-safe Web Development with Static Linearity}},
  booktitle = {Programming Language Approaches to Concurrency and Communication-cEntric Software},
  volume = {291},
  pages = {35--46},
  publisher = {Open Publishing Association},
  doi = "10.4204/EPTCS.291.4",
  year = 2019
}