research-article

Session types in Elixir

Authors:

Adrian FrancalanzaAuthors Info & Claims

AGERE 2021: Proceedings of the 11th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control

Pages 12 - 23

https://doi.org/10.1145/3486601.3486708

Published: 17 October 2021 Publication History

Abstract

This paper proposes an adaptation of session types to provide behavioural information about public functions in Elixir modules. We formalise typechecking rules for the main constructs of the language. This allows us to statically determine whether a function implementation observes its session endpoint specification. Based on this type system, we then construct a tool that automates typechecking for Elixir modules.

References

[1]

Gul A. Agha. 1990. ACTORS - a model of concurrent computation in distributed systems. MIT Press. isbn:978-0-262-01092-4

[2]

Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. 2016. Behavioral Types in Programming Languages. Found. Trends Program. Lang., 3, 2-3 (2016), 95–230. https://doi.org/10.1561/2500000031

Digital Library

[3]

Joe Armstrong, Robert Virding, and Mike Williams. 1993. Concurrent programming in ERLANG. Prentice Hall. isbn:978-0-13-285792-5

Digital Library

[4]

Duncan Paul Attard, Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. 2021. Better Late Than Never or: Verifying Asynchronous Components at Runtime. In FORTE (Lecture Notes in Computer Science, Vol. 12719). Springer, 207–225.

[5]

Christian Bartolo Burlò, Adrian Francalanza, and Alceste Scalas. 2021. On the Monitorability of Session Types, in Theory and Practice. In ECOOP (LIPIcs, Vol. 194). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 20:1–20:30.

[6]

Mauricio Cassola, Agustín Talagorria, Alberto Pardo, and Marcos Viera. 2020. A Gradual Type System for Elixir. Proceedings of the 24th Brazilian Symposium on Context-Oriented Programming and Advanced Modularity, Oct, isbn:9781450389433 https://doi.org/10.1145/3427081.3427084

Digital Library

[7]

Mauricio Cassola, Agustín Talagorria, Alberto Pardo, and Marcos Viera. 2021. A Gradual Type System for Elixir. CoRR, abs/2104.08366 (2021), arxiv:2104.08366. arxiv:2104.08366

[8]

David Castro-Perez, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. 2019. Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures. Proc. ACM Program. Lang., 3, POPL (2019), 29:1–29:30.

[9]

Zak Cutner and Nobuko Yoshida. 2021. Safe Session-Based Asynchronous Coordination in Rust. In Coordination Models and Languages - 23rd IFIP WG 6.1 International Conference, COORDINATION 2021, Held as Part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14-18, 2021, Proceedings, Ferruccio Damiani and Ornela Dardha (Eds.) (Lecture Notes in Computer Science, Vol. 12717). Springer, 80–89. https://doi.org/10.1007/978-3-030-78142-2_5

[10]

Ugo de’Liguoro and Luca Padovani. 2018. Mailbox Types for Unordered Interactions. In 32nd European Conference on Object-Oriented Programming, ECOOP 2018, July 16-21, 2018, Amsterdam, The Netherlands, Todd D. Millstein (Ed.) (LIPIcs, Vol. 109). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 15:1–15:28. https://doi.org/10.4230/LIPIcs.ECOOP.2018.15

[11]

Simon Fowler. 2016. An Erlang Implementation of Multiparty Session Actors. In Proceedings 9th Interaction and Concurrency Experience, ICE 2016, Heraklion, Greece, 8-9 June 2016, Massimo Bartoletti, Ludovic Henrio, Sophia Knight, and Hugo Torres Vieira (Eds.) (EPTCS, Vol. 223). 36–50. https://doi.org/10.4204/EPTCS.223.3

[12]

Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. 2019. Exceptional asynchronous session types: session types without tiers. Proc. ACM Program. Lang., 3, POPL (2019), 28:1–28:29. https://doi.org/10.1145/3290341

Digital Library

[13]

Qiang Guo, John Derrick, Clara Benac Earle, and Lars-Åke Fredlund. 2010. Model-Checking Erlang - A Comparison between EtomCRL2 and McErlang. In TAIC PART (Lecture Notes in Computer Science, Vol. 6303). Springer, 23–38.

[14]

Joseph Harrison. 2018. Automatic detection of core Erlang message passing errors. In Proceedings of the 17th ACM SIGPLAN International Workshop on Erlang, ICFP 2018, St. Louis, MO, USA, September 23-29, 2018, Natalia Chechina and Adrian Francalanza (Eds.). ACM, 37–48. https://doi.org/10.1145/3239332.3242765

Digital Library

[15]

Joseph Harrison. 2019. Runtime type safety for erlang/otp behaviours. In Proceedings of the 18th ACM SIGPLAN International Workshop on Erlang, Erlang@ICFP 2019, Berlin, Germany, August 18, 2019, Adrian Francalanza and Viktória Fördós (Eds.). ACM, 36–47. https://doi.org/10.1145/3331542.3342571

Digital Library

[16]

Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. 2021. Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), Anders Møller and Manu Sridharan (Eds.) (LIPIcs, Vol. 194). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 10:1–10:30. https://doi.org/10.4230/LIPIcs.ECOOP.2021.10

[17]

Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, Eike Best (Ed.) (Lecture Notes in Computer Science, Vol. 715). Springer, 509–523. https://doi.org/10.1007/3-540-57208-2_35

[18]

Kohei Honda, Aybek Mukhamedov, Gary Brown, Tzu-Chun Chen, and Nobuko Yoshida. 2011. Scribbling Interactions with a Formal Foundation. In Distributed Computing and Internet Technology - 7th International Conference, ICDCIT 2011, Bhubaneshwar, India, February 9-12, 2011. Proceedings, Raja Natarajan and Adegboyega K. Ojo (Eds.) (Lecture Notes in Computer Science, Vol. 6536). Springer, 55–75. https://doi.org/10.1007/978-3-642-19056-8_4

[19]

Keigo Imai, Rumyana Neykova, Nobuko Yoshida, and Shoji Yuen. 2020. Multiparty Session Programming With Global Protocol Combinators. In 34th European Conference on Object-Oriented Programming, ECOOP 2020, November 15-17, 2020, Berlin, Germany (Virtual Conference), Robert Hirschfeld and Tobias Pape (Eds.) (LIPIcs, Vol. 166). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 9:1–9:30. https://doi.org/10.4230/LIPIcs.ECOOP.2020.9

[20]

Keigo Imai, Nobuko Yoshida, and Shoji Yuen. 2019. Session-ocaml: A session-based library with polarities and lenses. Sci. Comput. Program., 172 (2019), 135–159. https://doi.org/10.1016/j.scico.2018.08.005

[21]

Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. 2015. Session types for Rust. In Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, WGP@ICFP 2015, Vancouver, BC, Canada, August 30, 2015, Patrick Bahr and Sebastian Erdweg (Eds.). ACM, 13–22. https://doi.org/10.1145/2808098.2808100

Digital Library

[22]

Wen Kokke. 2019. Rusty Variation: Deadlock-free Sessions with Failure in Rust. In Proceedings 12th Interaction and Concurrency Experience, ICE 2019, Copenhagen, Denmark, 20-21 June 2019, Massimo Bartoletti, Ludovic Henrio, Anastasia Mavridou, and Alceste Scalas (Eds.) (EPTCS, Vol. 304). 48–60. https://doi.org/10.4204/EPTCS.304.4

[23]

Wen Kokke and Ornela Dardha. 2021. Deadlock-Free Session Types in Linear Haskell. CoRR, abs/2103.14481 (2021), arxiv:2103.14481. arxiv:2103.14481

[24]

Nicolas Lagaillardie, Rumyana Neykova, and Nobuko Yoshida. 2020. Implementing Multiparty Session Types in Rust. In Coordination Models and Languages - 22nd IFIP WG 6.1 International Conference, COORDINATION 2020, Held as Part of the 15th International Federated Conference on Distributed Computing Techniques, DisCoTec 2020, Valletta, Malta, June 15-19, 2020, Proceedings, Simon Bliudze and Laura Bocchi (Eds.) (Lecture Notes in Computer Science, Vol. 12134). Springer, 127–136. https://doi.org/10.1007/978-3-030-50029-0_8

[25]

Tobias Lindahl and Konstantinos Sagonas. 2006. Practical type inference based on success typings. In Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 10-12, 2006, Venice, Italy, Annalisa Bossi and Michael J. Maher (Eds.). ACM, 167–178. https://doi.org/10.1145/1140335.1140356

Digital Library

[26]

Chris MacCord. 2015. Metaprogramming Elixir - Write Less Code, Get More Done (and Have Fun!). O’Reilly. isbn:978-1-680-50041-7 http://www.oreilly.de/catalog/9781680500417/index.html

[27]

Simon Marlow and Philip Wadler. 1997. A Practical Subtyping System For Erlang. In Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming (ICFP ’97), Amsterdam, The Netherlands, June 9-11, 1997, Simon L. Peyton Jones, Mads Tofte, and A. Michael Berman (Eds.). ACM, 136–149. https://doi.org/10.1145/258948.258962

Digital Library

[28]

Hernán C. Melgratti and Luca Padovani. 2017. Chaperone contracts for higher-order sessions. Proc. ACM Program. Lang., 1, ICFP (2017), 35:1–35:29.

[29]

Dimitris Mostrous and Vasco Thudichum Vasconcelos. 2011. Session Typing for a Featherweight Erlang. In Coordination Models and Languages - 13th International Conference, COORDINATION 2011, Reykjavik, Iceland, June 6-9, 2011. Proceedings, Wolfgang De Meuter and Gruia-Catalin Roman (Eds.) (Lecture Notes in Computer Science, Vol. 6721). Springer, 95–109. https://doi.org/10.1007/978-3-642-21464-6_7

[30]

Rumyana Neykova. 2013. Session Types Go Dynamic or How to Verify Your Python Conversations. In Proceedings 6th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES 2013, Rome, Italy, 23rd March 2013, Nobuko Yoshida and Wim Vanderbauwhede (Eds.) (EPTCS, Vol. 137). 95–102. https://doi.org/10.4204/EPTCS.137.8

[31]

Rumyana Neykova and Nobuko Yoshida. 2017. Multiparty Session Actors. Log. Methods Comput. Sci., 13, 1 (2017), https://doi.org/10.23638/LMCS-13(1:17)2017

[32]

Rumyana Neykova, Nobuko Yoshida, and Raymond Hu. 2013. SPY: Local Verification of Global Protocols. In Runtime Verification - 4th International Conference, RV 2013, Rennes, France, September 24-27, 2013. Proceedings, Axel Legay and Saddek Bensalem (Eds.) (Lecture Notes in Computer Science, Vol. 8174). Springer, 358–363. https://doi.org/10.1007/978-3-642-40787-1_25

[33]

Sven-Olof Nyström. 2003. A soft-typing system for Erlang. In Proceedings of the 2003 ACM SIGPLAN Workshop on Erlang, Uppsala, Sweden, August 29, 2003, Bjarne Däcker and Thomas Arts (Eds.). ACM, 56–71. https://doi.org/10.1145/940880.940888

Digital Library

[34]

Luca Padovani. 2017. A simple library implementation of binary sessions. J. Funct. Program., 27 (2017), e4.

[35]

Benjamin C. Pierce. 2002. Types and programming languages. MIT Press. isbn:978-0-262-16209-8

Digital Library

[36]

Riccardo Pucella and Jesse A. Tov. 2008. Haskell session types with (almost) no class. In Proceedings of the 1st ACM SIGPLAN Symposium on Haskell, Haskell 2008, Victoria, BC, Canada, 25 September 2008, Andy Gill (Ed.). ACM, 25–36. https://doi.org/10.1145/1411286.1411290

Digital Library

[37]

Nithin Vadukkumchery Rajendrakumar and Annette Bieniusa. 2021. Bidirectional typing for Erlang. In Proceedings of the 20th ACM SIGPLAN International Workshop on Erlang, Erlang@ICFP 2021, Virtual Event, Korea, August 26, 2021, Stavros Aronis and Annette Bieniusa (Eds.). ACM, 54–63. https://doi.org/10.1145/3471871.3472966

Digital Library

[38]

Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala. In 30th European Conference on Object-Oriented Programming, ECOOP 2016, July 18-22, 2016, Rome, Italy, Shriram Krishnamurthi and Benjamin S. Lerner (Eds.) (LIPIcs, Vol. 56). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 21:1–21:28. https://doi.org/10.4230/LIPIcs.ECOOP.2016.21

[39]

Alceste Scalas, Nobuko Yoshida, and Elias Benussi. 2019. Effpi: verified message-passing programs in Dotty. In Proceedings of the Tenth ACM SIGPLAN Symposium on Scala, Scala@ECOOP 2019, London, UK, July 17, 2019, Jonathan Immanuel Brachthäuser, Sukyoung Ryu, and Nathaniel Nystrom (Eds.). ACM, 27–31. https://doi.org/10.1145/3337932.3338812

Digital Library

[40]

Alceste Scalas, Nobuko Yoshida, and Elias Benussi. 2019. Verifying message-passing programs with dependent behavioural types. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, Kathryn S. McKinley and Kathleen Fisher (Eds.). ACM, 502–516. https://doi.org/10.1145/3314221.3322484

Digital Library

[41]

Dave Thomas. 2018. Programming Elixir: Functional, Concurrent, Pragmatic, Fun. Pragmatic Bookshelf.

[42]

Nachiappan Valliappan and John Hughes. 2018. Typing the wild in Erlang. In Proceedings of the 17th ACM SIGPLAN International Workshop on Erlang, ICFP 2018, St. Louis, MO, USA, September 23-29, 2018, Natalia Chechina and Adrian Francalanza (Eds.). ACM, 49–60. https://doi.org/10.1145/3239332.3242766

Digital Library

[43]

Vasco T. Vasconcelos. 2012. Fundamentals of session types. Inf. Comput., 217 (2012), 52–70. https://doi.org/10.1016/j.ic.2012.05.002

Digital Library

Cited By

Fowler SAttard DSowul FGay STrinder P(2023)Special Delivery: Programming with Mailbox TypesProceedings of the ACM on Programming Languages10.1145/36078327:ICFP(78-107)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607832
Le Brun MDardha O(2023)MAG: Types for Failure-Prone CommunicationProgramming Languages and Systems10.1007/978-3-031-30044-8_14(363-391)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_14
Tabone GFrancalanza A(2022)Session Fidelity for ElixirST: A Session-Based Type System for Elixir ModulesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.365.2365(17-36)Online publication date: 9-Aug-2022
https://doi.org/10.4204/EPTCS.365.2

Index Terms

Session types in Elixir
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
2. Theory of computation
  1. Models of computation
    1. Concurrency
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis

Recommendations

A Gradual Type System for Elixir
SBLP '20: Proceedings of the 24th Brazilian Symposium on Context-Oriented Programming and Advanced Modularity

Elixir is a functional programming language with dynamic typing. In this paper we propose a type system that makes it possible to perform static type-checking on a significant fragment of Elixir. An important feature of the type system we introduce is ...
Haskell session types with (almost) no class
HASKELL '08

We describe an implementation of session types in Haskell. Session types statically enforce that client-server communication proceeds according to protocols. They have been added to several concurrent calculi, but few implementations of session types ...
Haskell session types with (almost) no class
Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell

We describe an implementation of session types in Haskell. Session types statically enforce that client-server communication proceeds according to protocols. They have been added to several concurrent calculi, but few implementations of session types ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

AGERE 2021: Proceedings of the 11th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control

October 2021

36 pages

ISBN:9781450391047

DOI:10.1145/3486601

General Chairs:
Elias Castegren
Uppsala University, Sweden
,
Joeri De Koster
Vrije Universiteit Brussel, Belgium
,
Simon Fowler
University of Glasgow, UK

Copyright © 2021 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 October 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SPLASH '21

Sponsor:

SIGPLAN

SPLASH '21: Software for Humanity

October 17, 2021

IL, Chicago, USA

Acceptance Rates

Overall Acceptance Rate 19 of 35 submissions, 54%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
175
Total Downloads

Downloads (Last 12 months)28
Downloads (Last 6 weeks)1

Reflects downloads up to 14 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Fowler SAttard DSowul FGay STrinder P(2023)Special Delivery: Programming with Mailbox TypesProceedings of the ACM on Programming Languages10.1145/36078327:ICFP(78-107)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607832
Le Brun MDardha O(2023)MAG: Types for Failure-Prone CommunicationProgramming Languages and Systems10.1007/978-3-031-30044-8_14(363-391)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30044-8_14
Tabone GFrancalanza A(2022)Session Fidelity for ElixirST: A Session-Based Type System for Elixir ModulesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.365.2365(17-36)Online publication date: 9-Aug-2022
https://doi.org/10.4204/EPTCS.365.2

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents