Document Open Access Logo

Lightweight Session Programming in Scala

Authors Alceste Scalas, Nobuko Yoshida

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2016.21.pdf
  • Filesize: 1.24 MB
  • 28 pages

Document Identifiers

Author Details

Alceste Scalas
Nobuko Yoshida

Cite As Get BibTex

Alceste Scalas and Nobuko Yoshida. Lightweight Session Programming in Scala. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 21:1-21:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.ECOOP.2016.21

Abstract

Designing, developing and maintaining concurrent applications is an
error-prone and time-consuming task; most difficulties arise because
compilers are usually unable to check whether the inputs/outputs
performed by a program at runtime will adhere to a given protocol
specification. To address this problem, we propose lightweight session programming in Scala: we leverage the native features of the Scala
type system and standard library, to introduce (1) a representation of session types as Scala types, and (2) a library, called lchannels, with a convenient API for session-based programming, supporting local and distributed communication. We generalise the idea of Continuation-Passing Style Protocols (CPSPs), studying their formal relationship with session types. We illustrate how session programming can be carried over in Scala: how to formalise a communication protocol, and represent it using Scala classes and lchannels, letting the compiler help spotting protocol violations. We attest the practicality of our approach with a complex use case, and evaluate the performance of lchannels with a series of benchmarks.

Subject Classification

Keywords
  • session types
  • Scala
  • concurrency

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Karim Ali, Marianna Rapoport, Ondřej Lhoták, Julian Dolby, and Frank Tip. Constructing call graphs of Scala programs. In ECOOP, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44202-9_3.
  2. Nada Amin, Tiark Rompf, and Martin Odersky. Foundations of path-dependent types. In OOPSLA, 2014. URL: http://dx.doi.org/10.1145/2660193.2660216.
  3. Stephanie Balzer and Frank Pfenning. Objects as session-typed processes. In AGERE!, 2015. URL: http://dx.doi.org/10.1145/2824815.2824817.
  4. Hendrik Pieter Barendregt. The Lambda Calculus, Its Syntax and Semantics. North Holland, 1985. Google Scholar
  5. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In CONCUR, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15375-4_16.
  6. Ornela Dardha. Recursive session types revisited. In BEAT, 2014. URL: http://dx.doi.org/10.4204/EPTCS.162.4.
  7. Ornela Dardha. Type Systems for Distributed Programs: Components and Sessions. Phd thesis, Università degli studi di Bologna, May 2014. Google Scholar
  8. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. In PPDP, 2012. URL: http://dx.doi.org/10.1145/2370776.2370794.
  9. Romain Demangeon and Kohei Honda. Full abstraction in a subtyped pi-calculus with linear types. In CONCUR, 2011. Google Scholar
  10. Edsger W Dijkstra. Cooperating sequential processes. Springer, 1965. Google Scholar
  11. Juliana Franco and Vasco Thudichum Vasconcelos. A concurrent programming language with refined session types. In SEFM, 2013. URL: http://dx.doi.org/10.1007/978-3-319-05032-4_2.
  12. Simon Gay and Malcolm Hole. Types and subtypes for client-server interactions. In ESOP. Springer Berlin Heidelberg, 1999. URL: http://dx.doi.org/10.1007/3-540-49099-X_6.
  13. Simon Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 2005. URL: http://dx.doi.org/10.1007/s00236-005-0177-z.
  14. Simon J. Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1), January 2010. URL: http://dx.doi.org/10.1017/S0956796809990268.
  15. Philipp Haller and Martin Odersky. Capabilities for uniqueness and borrowing. In ECOOP, 2010. Google Scholar
  16. Philipp Haller, Aleksandar Prokopec, Heather Miller, Viktor Klang, Roland Kuhn, and Vojin Jovanovic. Futures and Promises. URL: http://docs.scala-lang.org/overviews/core/futures.html.
  17. Jiansen He, Philip Wadler, and Philip Trinder. Typecasting actors: From Akka to TAkka. In SCALA'14, 2014. URL: http://dx.doi.org/10.1145/2637647.2637651.
  18. Kohei Honda. Types for dyadic interaction. In CONCUR, 1993. URL: http://dx.doi.org/10.1007/3-540-57208-2_35.
  19. Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In ESOP, 1998. URL: http://dx.doi.org/10.1007/BFb0053567.
  20. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL, 2008. URL: http://dx.doi.org/10.1145/1328438.1328472.
  21. Raymond Hu, Dimitrios Kouzapas, Olivier Pernet, Nobuko Yoshida, and Kohei Honda. Type-safe eventful sessions in Java. In ECOOP, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14107-2_16.
  22. Raymond Hu and Nobuko Yoshida. Hybrid session verification through endpoint API generation. In FASE, 2016. Google Scholar
  23. Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-based distributed programming in Java. In ECOOP, 2008. URL: http://dx.doi.org/10.1007/978-3-540-70592-5_22.
  24. Shams M. Imam and Vivek Sarkar. Savina - an actor benchmark suite: Enabling empirical evaluation of actor libraries. In Proceedings of the 4th International Workshop on Programming Based on Actors Agents & Decentralized Control, AGERE!, 2014. URL: http://dx.doi.org/10.1145/2687357.2687368.
  25. Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. Session types for rust. In Proceedings of the 11th ACM SIGPLAN Workshop on Generic Programming, WGP, 2015. URL: http://dx.doi.org/10.1145/2808098.2808100.
  26. Roland Kuhn. Project G\aalbma, actors vs types, 2015. URL: http://slideshare.net/rolandkuhn/project-galbma-actors-vs-types.
  27. Lightbend, Inc. Actor paths, 2016. URL: http://doc.akka.io/docs/akka/2.4.4/general/addressing.html.
  28. Lightbend, Inc. The Akka toolkit and runtime, 2016. URL: http://akka.io/.
  29. Lightbend, Inc. Akka Typed, 2016. URL: http://doc.akka.io/docs/akka/2.4.4/scala/typed.html.
  30. Lightbend, Inc. The Scala IDE, 2016. URL: http://scala-ide.org/.
  31. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes. Inf. &Comput., 1992. URL: http://dx.doi.org/10.1016/0890-5401(92)90008-4.
  32. Matthias Neubauer and Peter Thiemann. An implementation of session types. In PADL, 2004. URL: http://dx.doi.org/10.1007/978-3-540-24836-1_5.
  33. Luca Padovani. A Simple Library Implementation of Binary Sessions. https://hal.archives-ouvertes.fr/hal-01216310, 2015.
  34. Riccardo Pucella and Jesse A. Tov. Haskell session types with (almost) no class. In Haskell, 2008. URL: http://dx.doi.org/10.1145/1411286.1411290.
  35. Tiark Rompf and Nada Amin. From F to DOT: Type soundness proofs with definitional interpreters. Technical report, Purdue University and EPFL, 2015. Unpublished. URL: http://arxiv.org/abs/1510.05216.
  36. Davide Sangiorgi and David Walker. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, 2003. Google Scholar
  37. K. C. Sivaramakrishnan, Karthik Nagaraj, Lukasz Ziarek, and Patrick Eugster. Efficient session type guided distributed interaction. In COORDINATION, 2010. URL: http://dx.doi.org/10.1007/978-3-642-13414-2_11.
  38. K. C. Sivaramakrishnan, Mohammad Qudeisat, Lukasz Ziarek, Karthik Nagaraj, and Patrick Eugster. Efficient sessions. Sci. Comput. Program., 78(2), 2013. URL: http://dx.doi.org/10.1016/j.scico.2012.03.004.
  39. Kaku Takeuchi, Kohei Honda, and Makoto Kubo. An interaction-based language and its typing system. In PARLE, 1994. URL: http://dx.doi.org/10.1007/3-540-58184-7_118.
  40. Bernardo Toninho, Luís Caires, and Frank Pfenning. Higher-order processes, functions, and sessions: a monadic integration. In ESOP, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37036-6_20.
  41. Matías Toro and Éric Tanter. Customizable gradual polymorphic effects for Scala. In OOPSLA, 2015. URL: http://dx.doi.org/10.1145/2814270.2814315.
  42. Vasco T. Vasconcelos. Fundamentals of session types. Inf. &Comput., 217, 2012. URL: http://dx.doi.org/10.1016/j.ic.2012.05.002.
  43. Philip Wadler. Propositions as sessions. In ICFP, 2012. URL: http://dx.doi.org/10.1145/2364527.2364568.
  44. Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. The scribble protocol language. In TGC, 2013. URL: http://dx.doi.org/10.1007/978-3-319-05119-2_3.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact