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

LaST-FP：函数式编程的线性类型和会话类型

• 批准号: 395068988
• 负责人: Professor Dr. Peter Thiemann
• 金额: --
• 依托单位: Graduate School of Information Science
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2018
• 资助国家: 德国
• 起止时间: 2017-12-31 至 2021-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/395068988?language=en
• 关键词: LaST; FP; Linear; Types; Session

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.

分布式应用程序的最新基础设施越来越依赖于微服务。基础设施和应用程序中的组件实现了以全局编排方式相互通信的微服务。会话类型为协调和结构化通信提供轻量级规范。它们为组件建立了一整套理想的编译时保证，例如类型安全、会话保真度和死锁自由。在编程语言中内置对会话类型的支持将对开发人员有巨大的帮助，因为分布式系统中的组件非常难以调试，而会话类型可以消除整个类别的潜在错误。到目前为止，会话类型在组件的编程语言中不可用。原因之一是会话类型需要支持线性和其他高级特性（像类型函数）在语言的类型系统中，以确保序列，方向，这个项目的目标是为增强具有线性和会话类型的编程语言开发理论基础，并验证在实践中产生的框架与工业实力的编程语言，支持编程通信组件的实现。为了实现这一目标，该项目将进一步设计和实现高级会话类型层和现有消息处理基础设施之间的连接器，以集成到微服务架构中。