Session-ocaml: A Session-Based Library with Polarities and Lenses
Session-ocaml: A Session-Based Library with Polarities and Lenses
复制标题
Session-ocaml：具有极性和透镜的基于会话的库
DOI：
10.1007/978-3-319-59746-1_6
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Yuen Shoji
中科院分区：
文献类型：
--
作者：
Imai Keigo;Yoshida Nobuko;Yuen Shoji
我们提出了一个新的OCaml会话类型并发/分布式编程库-ocaml。我们的技术完全依赖于参数多态性，它可以编码的核心会话类型的结构具有强大的静态保证。我们的核心理念是：（1）极化的会话类型，其给出了二元性的替代公式，使得OCaml能够以合理的标记开销自动推断会话中的适当会话类型;以及（2）参数化的monad，其具有被称为“槽”的数据结构，该数据结构用透镜操纵，其可以静态地强制会话线性，包括委托。我们引入了一个符号扩展，以提高会话的线性集成到函数式编程风格的会话类型。我们展示了session-ocaml在一个旅行社用例和一个SMTP协议实现中的应用。此外，我们评估了一些基准的性能。
We proposesession-ocaml, a novel library for session-typed concurrent/distributed programming in OCaml. Our technique solely relies on parametric polymorphism, which can encode core session type structures with strong static guarantees. Our key ideas are: (1)polarised session types, which give an alternative formulation of duality enabling OCaml to automatically infer an appropriate session type in a session with a reasonable notational overhead; and (2) aparameterised monadwith a data structure called ‘slots’ manipulated withlenses, which can statically enforce session linearity including delegations. We introduce a notational extension to enhance the session linearity for integrating the session types into the functional programming style. We show applications ofsession-ocamlto a travel agency use case and an SMTP protocol implementation. Furthermore, we evaluate the performance of on a number of benchmarks.