Session type

In type theory, session types are used to ensure correctness in concurrent programs. They guarantee that messages sent and received between concurrent programs are in the expected order and of the expected type.^[1][2] Session type systems have been adapted for both channel and actor systems.^[3]

Session types are used to ensure desirable properties in concurrent and distributed systems, i.e. absence of communication errors or deadlocks, and protocol conformance.^[4]

Binary versus multiparty session types

Interaction between two processes can be checked using binary session types, while interactions between more than two processes can be checked using multiparty session types.^[5] In multiparty session types interactions between all participants are described using a global type, which is then projected into local types that describe communication from the local view of each participant. Importantly, the global type encodes the sequencing information of the communication, which would be lost if we were to use binary session types to encode the same communication.^[6]

Formal definition of binary session types

Binary session types can be described using send operations (${\displaystyle$ !} ), receive operations (${\displaystyle$ ?} ), branches (${\displaystyle \&}$), selections (${\displaystyle \oplus }$), recursion (${\displaystyle rec}$) and termination (${\displaystyle end}$).^[2]

For example, ${\displaystyle S=\;!bool.?int.end}$ represents a session type ${\displaystyle S}$ which first sends a boolean (${\displaystyle !bool}$), then receives an integer (${\displaystyle ?int}$) before finally terminating (${\displaystyle end}$).

Implementations

Session types have been adapted for several existing programming languages, including:

• lchannels (Scala)^[7]
• Effpi (Scala)^[7]
• STMonitor (Scala)^[8]
• EnsembleS^[9]
• Session-types (Rust)^[10]
• sesh (Rust)^[11]
• Session Actors (Python)^[12]
• Monitored Session Erlang (Erlang)^[13]
• FuSe (OCaml)^[14]
• session-ocaml (OCaml)^[15][16]
• Priority Sesh (Haskell)^[17]
• Java Typestate Checker (Java)^[18][19][20]
• Swift Sessions (Swift)^[21]

References

1. Hüttel, Hans; Lanese, Ivan; Vasconcelos, Vasco T.; Caires, Luís; Carbone, Marco; Deniélou, Pierre-Malo; Mostrous, Dimitris; Padovani, Luca; Ravara, António; Tuosto, Emilio; Vieira, Hugo Torres; Zavattaro, Gianluigi (5 April 2016). "Foundations of Session Types and Behavioural Contracts". ACM Computing Surveys. 49 (1): 3:1–3:36. doi:10.1145/2873052. hdl:2381/38761. ISSN 0360-0300. S2CID 3580137.
2. Ancona, Davide (2016). Behavioral types in programming languages. Hanover, Massachusetts: Now Publishers. ISBN 978-1-68083-135-1. OCLC 1053840486.
3. Fowler, Simon; Lindley, Sam; Wadler, Philip (10 May 2017). "Mixing Metaphors: Actors as Channels and Channels as Actors (Extended Version)". arXiv:1611.06276 [cs.PL].
4. Scalas, Alceste; Yoshida, Nobuko (June 2018). "Multiparty session types, beyond duality". Journal of Logical and Algebraic Methods in Programming. 97: 55–84. doi:10.1016/j.jlamp.2018.01.001. hdl:10044/1/56777. S2CID 48360420.
5. Honda, Kohei; Yoshida, Nobuko; Carbone, Marco (2008). "Multiparty asynchronous session types". Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 273–284. doi:10.1145/1328438.1328472. hdl:10044/1/26368. ISBN 9781595936899. S2CID 53038488.
6. Yoshida, Nobuko; Gheri, Lorenzo (2019). A Very Gentle Introduction to Multiparty Session Types. ICDCIT 2020. doi:10.1007/978-3-030-36987-3_5.
7. "Session programming in Scala". alcestes.github.io. Retrieved 2 November 2021.
8. "STMonitor". chrisbartoloburlo.github.io. Retrieved 2 November 2021.
9. Harvey, Paul; Fowler, Simon; Dardha, Ornela; Gay, Simon J. (2021). "Multiparty Session Types for Safe Runtime Adaptation in an Actor Language". 35th European Conference on Object-Oriented Programming (ECOOP 2021). 194: 10:1–10:30. doi:10.4230/LIPIcs.ECOOP.2021.10. S2CID 234681015.
10. Jespersen, Thomas Bracht Laumann; Munksgaard, Philip; Larsen, Ken Friis (30 August 2015). "Session types for Rust". Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming. WGP 2015. Association for Computing Machinery. pp. 13–22. doi:10.1145/2808098.2808100. ISBN 9781450338103. S2CID 18320631.
11. Kokke, Wen (12 September 2019). "Rusty Variation: Deadlock-free Sessions with Failure in Rust". Electronic Proceedings in Theoretical Computer Science. 304: 48–60. arXiv:1909.05970. doi:10.4204/EPTCS.304.4. ISSN 2075-2180. S2CID 198166990.
12. Yoshida, Nobuko; Neykova, Rumyana (29 March 2017). "Multiparty Session Actors". Logical Methods in Computer Science. 13 (1). doi:10.23638/LMCS-13(1:17)2017. S2CID 65240382.
13. Fowler, Simon (10 August 2016). "An Erlang Implementation of Multiparty Session Actors". Electronic Proceedings in Theoretical Computer Science. 223: 36–50. arXiv:1608.03321. doi:10.4204/EPTCS.223.3. ISSN 2075-2180. S2CID 418549.
14. Padovani, Luca (2017). "A simple library implementation of binary sessions". Journal of Functional Programming. 27: e4. doi:10.1017/S0956796816000289. hdl:2318/1634956. ISSN 0956-7968. S2CID 19776781.
15. Imai, Keigo; Yoshida, Nobuko; Yuen, Shoji (March 2019). "Session-ocaml: A session-based library with polarities and lenses". Science of Computer Programming. 172: 135–159. doi:10.1016/j.scico.2018.08.005. hdl:10044/1/63748. ISSN 0167-6423. S2CID 69673075.
16. Imai, Keigo. "Session OCaml". www.ct.info.gifu-u.ac.jp. Retrieved 2 November 2021.
17. Kokke, Wen; Dardha, Ornela (26 March 2021). "Deadlock-Free Session Types in Linear Haskell". arXiv:2103.14481 [cs.PL].
18. "Java Typestate Checker". GitHub.
19. Bacchiani, Lorenzo; Bravetti, Mario; Giunti, Marco; Mota, João; Ravara, António (2022). "A Java typestate checker supporting inheritance". Sci. Comput. Program. 221: 102844. doi:10.1016/j.scico.2022.102844. hdl:10362/145315. S2CID 250940803.
20. Mota, João; Giunti, Marco; Ravara, António (2021). "Java Typestate Checker". Proceedings of COORDINATION 2021. Lecture Notes in Computer Science. Vol. 12717. pp. 121–133. doi:10.1007/978-3-030-78142-2_8. ISBN 978-3-030-78141-5. S2CID 235383301.
21. Rubicini, Alessio; Padovani, Luca (2023). "Swift Sessions: a library implementation of binary session types in Swift". GitHub.