Multiparty session type-safe web development with static linearity

Abstract

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