Typed concurrent functional programming with channels, actors and sessions

Abstract

The age of writing single-threaded applications is over. To develop scalable applications, developers must make use of concurrency and parallelism. Nonetheless, introducing concurrency and parallelism is difficult: naïvely implemented, concurrent code is prone to issues such as race conditions and deadlocks. Moving to the distributed setting introduces yet more issues, in particular the possibility of failure. To cope with many of the problems of concurrent programming, language designers have proposed a class of programming languages known as communication-centric programming languages, which provide lightweight processes which do not share memory, but instead communicate using explicit message passing. The focus of this thesis is on typed communication-centric functional programming languages, using type systems to provide static guarantees about the runtime behaviour of concurrent programs. We investigate two strands of work: the relationship between typed channel- and actor-based languages, and the integration of asynchrony, exception handling, and session types in a functional programming language. In the first strand, we investigate two particular subclasses of communication-centric languages: channel-based languages such as Go, and languages based on the actor model, such as Erlang. We distil the essence of the languages into two concurrent λ-calculi: λch for simply-typed channels, and lact for simply-typed actors, and provide type- and semantics-preserving translations between them. In doing so, we clear up confusion between the two models, give theoretical foundations for recent implementations of type-parameterised actors, and also provide a theoretical grounding for frameworks which emulate actors in channel-based languages. Furthermore, by extending the core calculi, we note that actor synchronisation drastically simplifies the translation from channels into actors, and show that Erlang’s selective receive mechanism can be implemented without specialised constructs. In the second strand, we integrate session types, asynchrony, and exception handling in a functional programming language. Session types are a behavioural type system for communication channel endpoints, allowing conformance to protocols to be checked statically. We provide the first integration of exception handling and asynchronous session types in a core functional language, Exceptional GV, and prove that it satisfies preservation, global progress, and that it is confluent and terminating. We demonstrate the practical applicability of the approach by extending the Links tierless web programming language with exception handling, in turn providing the first implementation of exception handling in the presence of session types in a functional language. As a result, we show the first application of session types to web programming, providing examples including a two-factor authentication workflow and a chat application.