Traditional session types prescribe bidirectional communication protocols for concurrent computations, where well-typed programs are guaranteed to adhere to the protocols. However, simple session types cannot capture properties beyond the basic type of the exchanged messages. In response, recent work has extended session types with refinements from linear arithmetic, capturing intrinsic attributes of processes and data. These refinements then play a central role in describing sequential and parallel complexity bounds on session-typed programs. The Rast language provides an open-source implementation of session-typed concurrent programs extended with arithmetic refinements as well as ergometric and temporal types to capture work and span of program execution. To further support generic programming, Rast also enhances arithmetically refined session types with recently developed nested parametric polymorphism. Type checking relies on Cooper's algorithm for quantifier elimination in Presburger arithmetic with a few significant optimizations, and a heuristic extension to nonlinear constraints. Rast furthermore includes a reconstruction engine so that most program constructs pertaining the layers of refinements and resources are inserted automatically. We provide a variety of examples to demonstrate the expressivity of the language.
翻译:传统会话类型为同时计算规定了双向通信协议, 保证有良好的程序类型来遵守协议。 但是, 简单的会话类型无法捕捉到交换信息的基本类型以外的属性。 作为回应, 最近的工作扩大了会话类型, 精细的线性算术, 捕捉了过程和数据的内在属性。 这些改进在描述相继和平行复杂程度与会话类型程序的关系方面起着核心作用。 拉斯特语为会议类型的同时程序提供了开放源头的实施, 配有精细的算术和时间类型, 以捕捉工程和方案执行的范围。 为了进一步支持通用的编程, Rast 也用最近开发的嵌套的参数多形态加强计算精细的会话类型。 类型检查依赖于Cooper的算法, 以少数重大优化的方式消除前斯堡算术中的量化标准, 以及非线性约束的超理论扩展。 拉斯特语还包括一个重建引擎, 以便大多数方案在精细度和资源层次上建构成。 我们提供各种例子, 以证明语言的清晰性。