Session-ocaml: a session-based library with polarities and lenses
File(s) DTRS17-8.pdf (584.4 KB)
Published version
Author(s)
Imai, Keigo
Yoshida, Nobuko
Yuen, Shoji
Type
Report
Abstract
We propose session-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: ( ) 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 ( ) a parameterised monad
with a data structure called ‘slots’ manipulated with lenses, which can
statically enforce session linearity and delegations. We show applications
of session-ocaml including a travel agency usecase and an SMTP protocol.
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: ( ) 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 ( ) a parameterised monad
with a data structure called ‘slots’ manipulated with lenses, which can
statically enforce session linearity and delegations. We show applications
of session-ocaml including a travel agency usecase and an SMTP protocol.
Date Issued
2017-01-01
Citation
Departmental Technical Report: 17/8, 2017, pp.1-25
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
25
Journal / Book Title
Departmental Technical Report: 17/8
Copyright Statement
© 2017 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
17/8
