LaST-FP: Linear Types and Session Types for Functional Programming

点击翻译按钮获取中文摘要

State-of-the-art infrastructures for distributed applications rely more and more on microservices. Components in the infrastructure and in the application implement microservices that communicate with each other in a globally orchestrated way. Session types provide lightweight specifications for orchestrated and structured communication. They establish a whole class of desirable compile-time guarantees for components, for example type safety, session fidelity, and deadlock freedom. Builtin support for session types in a programming language would be a tremendous help for developers, as components in a distributed system are notoriously hard to debug and session typing eliminates a whole class of potential errors. As of today, session types are not available in programming languages for components. One of the reasons is that session types require support for linearity and other advanced features (like type functions) in the language's type system, to ensure that the sequence, direction, and type of messages in a communication is reliable and that no participant drops a connection.The goal of this project is to develop the theoretical foundations for enhancing a programming language with linearity and session types and to validate the resulting framework in practice with an implementation in an industrial strength programming language thatsupports programming communicating components. To achieve that goal, the project will further design and implement the connectors between the high-level session type layer and existing message-handling infrastructure to integrate into a microservice architecture.