Session type

Last updated

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]

Contents

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 (), receive operations (), branches (), selections (), recursion () and termination (). [2]

For example, represents a session type which first sends a boolean (), then receives an integer () before finally terminating ().

Implementations

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

Related Research Articles

In computer science, functional programming is a programming paradigm where programs are constructed by applying and composing functions. It is a declarative programming paradigm in which function definitions are trees of expressions that map values to other values, rather than a sequence of imperative statements which update the running state of the program.

This is a "genealogy" of programming languages. Languages are categorized under the ancestor language with the strongest influence. Those ancestor languages are listed in alphabetic order. Any such categorization has a large arbitrary element, since programming languages often incorporate major ideas from multiple sources.

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every term. Usually the terms are various language constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.

Type inference, sometimes called type reconstruction, refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistics.

In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.

An expression-oriented programming language is a programming language in which every construction is an expression and thus yields a value. The typical exceptions are macro definitions, preprocessor commands, and declarations, which expression-oriented languages often treat as statements.

Many programming language type systems support subtyping. For instance, if the type Cat is a subtype of Animal, then an expression of type Cat should be substitutable wherever an expression of type Animal is used.

SIGPLAN is the Association for Computing Machinery's Special Interest Group on programming languages.

In computer science, a type class is a type system construct that supports ad hoc polymorphism. This is achieved by adding constraints to type variables in parametrically polymorphic types. Such a constraint typically involves a type class T and a type variable a, and means that a can only be instantiated to a type whose members support the overloaded operations associated with T.

A bigraph can be modelled as the superposition of a graph and a set of trees.

In functional programming, a generalized algebraic data type is a generalization of parametric algebraic data types.

QuickCheck is a software library, specifically a combinator library, originally written in the programming language Haskell, designed to assist in software testing by generating test cases for test suites – an approach known as property testing.

Thrift is an IDL and binary communication protocol used for defining and creating services for programming languages. It was developed by Facebook. Since 2020, it is an open source project in the Apache Software Foundation.

BSON is a computer data interchange format. The name "BSON" is based on the term JSON and stands for "Binary JSON". It is a binary form for representing simple or complex data structures including associative arrays, integer indexed arrays, and a suite of fundamental scalar types. BSON originated in 2009 at MongoDB. Several scalar data types are of specific interest to MongoDB and the format is used both as a data storage and network transfer format for the MongoDB database, but it can be used independently outside of MongoDB. Implementations are available in a variety of languages such as C, C++, C#, D, Delphi, Erlang, Go, Haskell, Java, JavaScript, Julia, Lua, OCaml, Perl, PHP, Python, Ruby, Rust, Scala, Smalltalk, and Swift.

MessagePack is a computer data interchange format. It is a binary form for representing simple data structures like arrays and associative arrays. MessagePack aims to be as compact and simple as possible. The official implementation is available in a variety of languages, some official libraries and others community created, such as C, C++, C#, D, Erlang, Go, Haskell, Java, JavaScript (NodeJS), Lua, OCaml, Perl, PHP, Python, Ruby, Rust, Scala, Smalltalk, and Swift.

The table shows a comparison of functional programming languages which compares various features and designs of different functional programming languages.

<span class="mw-page-title-main">Rosetta Code</span> Wiki-based programming chrestomathy

Rosetta Code is a wiki-based programming chrestomathy website with implementations of common algorithms and solutions to various programming problems in many different programming languages. It is named for the Rosetta Stone, which has the same text inscribed on it in three languages, and thus allowed Egyptian hieroglyphs to be deciphered for the first time.

Multitier programming is a programming paradigm for distributed software, which typically follows a multitier architecture, physically separating different functional aspects of the software into different tiers. Multitier programming allows functionalities that span multiple of such tiers to be developed in a single compilation unit using a single programming language. Without multitier programming, tiers are developed using different languages, e.g., JavaScript for the Web client, PHP for the Web server and SQL for the database. Multitier programming is often integrated into general-purpose languages by extending them with support for distribution.

In computer science, choreographic programming is a programming paradigm where programs are compositions of interactions among multiple concurrent participants.

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. 1 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. 1 2 "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 .


This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.