Atsushi Igarashi
Philip Wadler
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing.
We propose GradualGV as an extension of the functional session type system GV with dynamic types and casts. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.
Supplemental Material
Available for Download
zip
icfp17-main76-s.zip (301 KB)
This artifact contains programs in Haskell and Racket that implements the statics and the dynamics of the ICFP 2017 paper "Gradual Session Types". The Haskell program is a type checker for the language in the paper. It has various options to pretty print the output of the type checker documented in a separate README file. One option is to generate input terms suitable for use with the Racket program. The Haskell program was written by Hannes Saffrich. The PLT-Redex script implements the operational semantics presented in the paper. It's currently not well integrated with the type checker. The type checker's output has to be cut-and-pasted into Redex.
- Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. 2014. A theory of gradual effect systems. In International Conference on Functional Programming (ICFP). ACM, 283–295.Google Scholar
- H.P. Barendregt. 1984. The Lambda Calculus: Its Syntax and Semantics. North-Holland.Google Scholar
- Andrej Bauer and Matija Pretnar. 2015. Programming with algebraic effects and handlers. Journal of Logical and Algebraic Methods in Programming 84, 1 (2015), 108–123. Google ScholarCross Ref
- Gavin Bierman, Martin Abadi, and Mads Torgersen. 2014. Understanding TypeScript. In European Conference on ObjectOriented Programming (ECOOP) (LNCS), Vol. 8586. Springer, 257–281. Google ScholarDigital Library
- Gavin M. Bierman, Erik Meijer, and Mads Torgersen. 2010. Adding dynamic types to C#. In European Conference on Object-Oriented Programming (ECOOP) (LNCS). Springer, 76–100.Google Scholar
- Laura Bocchi, Tzu-Chun Chen, Romain Demangeon, Kohei Honda, and Nobuko Yoshida. 2017. Monitoring networks through multiparty session types. Theoretical Computer Science 699 (2017), 33–58. Google ScholarCross Ref
- Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. Journal of Functional Programming 23, 05 (2013), 552–593. Google ScholarCross Ref
- Luís Caires and Frank Pfenning. 2010. Session types as intuitionistic linear propositions. In International Conference on Concurrency Theory (CONCUR) (LNCS). Springer, 222–236. Google ScholarCross Ref
- Luis Caires, Frank Pfenning, and Bernardo Toninho. 2014. Linear logic propositions as session types. Mathematical Structures in Computer Science 26, 03 (2014), 367–423. Google ScholarCross Ref
- Adam Chlipala. 2013. Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press.Google Scholar
- Manuel Fähndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen C. Hunt, James R. Larus, and Steven Levi. 2006. Language support for fast and reliable message-based communication in Singularity OS. In European Conference on Computer Systems (EuroSys). ACM, 177–190. Google ScholarDigital Library
- Luminous Fennell and Peter Thiemann. 2012. The Blame Theorem for a Linear Lambda Calculus with Type Dynamic. In Trends in Functional Programming (LNCS), Vol. 7829. Springer, 37–52.Google Scholar
- Robert Bruce Findler and Matthias Felleisen. 2002. Contracts for Higher-Order Functions. In International Conference on Functional Programming (ICFP). ACM, 48–59. Google ScholarDigital Library
- Cormac Flanagan. 2006. Hybrid Type Checking. In Principles of Programming Languages (POPL). ACM, 245–256. Google ScholarDigital Library
- Simon Fowler. 2016. An Erlang Implementation of Multiparty Session Actors. In Interaction and Concurrency Experience. 36–50. Google ScholarCross Ref
- Juliana Franco and Vasco Thudichum Vasconcelos. 2013. A Concurrent Programming Language with Refined Session Types. In SEFM (LNCS), Vol. 8368. Springer, 15–28.Google Scholar
- Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting gradual typing. In Principles of Programming Languages (POPL). ACM, 429–442. Google ScholarDigital Library
- Simon Gay and Malcolm Hole. 2005. Subtyping for session types in the pi calculus. Acta Informatica 42, 2-3 (2005), 191–225.Google ScholarCross Ref
- Simon Gay and Vasco Vasconcelos. 2010. Linear type theory for asynchronous session types. Journal of Functional Programming 20, 01 (2010), 19–50. Google ScholarDigital Library
- Simon J. Gay, Vasco Thudichum Vasconcelos, António Ravara, Nils Gesbert, and Alexandre Z. Caldeira. 2010. Modular session types for distributed object-oriented programming. In Principles of Programming Languages (POPL). ACM, 299–312. Google ScholarDigital Library
- Jean-Yves Girard. 1987. Linear logic. Theoretical computer science 50, 1 (1987), 1–101. Google ScholarDigital Library
- Michael Greenberg, Benjamin C. Pierce, and Stephanie Weirich. 2010. Contracts Made Manifest. In Principles of Programming Languages (POPL). ACM, 353–364. Google ScholarDigital Library
- Kohei Honda. 1993. Types for Dyadic Interaction. In International Conference on Concurrency Theory (CONCUR) (LNCS), Vol. 715. Springer, 509–523. Google ScholarCross Ref
- K. Honda, A. Mukhamedov, G. Brown, T. Chen, and N. Yoshida. 2011. Scribbling Interactions with a Formal Foundation. In ICDCIT (LNCS), Vol. 6536. Springer, 55–75. Google ScholarCross Ref
- Kohei Honda, Vasco Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In European Symposium on Programming (ESOP) (LNCS). Springer, 122–138. Google ScholarCross Ref
- Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty asynchronous session types. In Principles of Programming Languages (POPL). ACM, 273–284. Google ScholarDigital Library
- Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2016. Multiparty asynchronous session types. J. ACM 63, 1 (2016), 9.Google ScholarDigital Library
- Raymond Hu, Dimitrios Kouzapas, Olivier Pernet, Nobuko Yoshida, and Kohei Honda. 2010. Type-safe eventful sessions in Java. In European Conference on Object-Oriented Programming (ECOOP) (LNCS), Vol. 6183. Springer, 329–353. Google ScholarCross Ref
- Raymond Hu and Nobuko Yoshida. 2016. Hybrid session verification through endpoint API generation. In Fundamental Approaches to Software Engineering (FASE) (LNCS), Vol. 9633. Springer, 401–418. Google ScholarDigital Library
- Raymond Hu, Nobuko Yoshida, and Kohei Honda. 2008. Session-based distributed programming in Java. In European Conference on Object-Oriented Programming (ECOOP) (LNCS), Vol. 5142. Springer, 516–541. Google ScholarDigital Library
- Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. 2015. Session types for Rust. In Workshop on Generic Programming (WGP). ACM, 13–22.Google ScholarDigital Library
- Dimitrios Kouzapas, Ornela Dardha, Roly Perera, and Simon J. Gay. 2016. Typechecking protocols with Mungo and StMungo. In Principles and Practice of Declarative Programming (PPDP). ACM, 146–159. Google ScholarDigital Library
- Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2017. Fencing off Go: liveness and safety for channelbased programming. In Principles of Programming Languages (POPL). ACM, 748–761. Google ScholarDigital Library
- Daan Leijen. 2017. Type Directed Compilation of Row-typed Algebraic Effects. SIGPLAN Not. 52, 1, 486–499. Google ScholarDigital Library
- Sam Lindley, Conor McBride, and Craig McLaughlin. 2017. Do Be Do Be Do. In Principles of Programming Languages (POPL). ACM, 500–514. Google ScholarDigital Library
- Sam Lindley and J. Garrett Morris. 2016a. Embedding session types in Haskell. In Symposium on Haskell. ACM, 133–145. Google ScholarDigital Library
- Sam Lindley and J Garrett Morris. 2016b. Talking bananas: structural recursion for session types. In International Conference on Functional Programming (ICFP). ACM, 434–447. Google ScholarDigital Library
- Sam Lindley and J. Garrett Morris. 2017. Behavioural Types: from Theory to Tools. River Publishers, Chapter Lightweight functional session types.Google Scholar
- Robin Milner, Joachim Parrow, and David Walker. 1992. A calculus of mobile processes, I. Information and Computation 100, 1 (1992), 1–40. Google ScholarDigital Library
- Dimitris Mostrous and Vasco T. Vasconcelos. 2011. Session typing for a featherweight Erlang. In Coordination Models and Languages (COORDINATION) (LNCS), Vol. 6721. Springer, 95–109. Google ScholarCross Ref
- Rumyana Neykova and Nobuko Yoshida. 2014. Multiparty session actors. In Coordination Models and Languages (COORDI-NATION) (LNCS), Vol. 8459. Springer, 131–146. Google ScholarDigital Library
- Rumyana Neykova and Nobuko Yoshida. 2017. Let it recover: multiparty protocol-induced recovery. In International Conference on Compiler Construction (CC). ACM, 98–108. Google ScholarDigital Library
- Rumyana Neykova, Nobuko Yoshida, and Raymond Hu. 2013. SPY: Local Verification of Global Protocols. In International Conference on Runtime Verification (RV) (LNCS), Vol. 8174. Springer, 358–363.Google Scholar
- Nicholas Ng and Nobuko Yoshida. 2016. Static deadlock detection for concurrent Go by global session graph synthesis. In International Conference on Compiler Construction (CC). ACM, 174–184. Google ScholarDigital Library
- Nicholas Ng, Nobuko Yoshida, and Kohei Honda. 2012. Multiparty Session C: Safe parallel programming with message optimisation. In International Conference on Modelling Techniques and Tools for Computer Performance Evaluation (TOOLS) (LNCS), Vol. 7304. Springer, 202–218.Google ScholarDigital Library
- Ulf Norell. 2009. Dependently typed programming in Agda. In Proceedings of the 4th International Workshop on Types in Language Design and Implementation (TLDI ’09). ACM, 1–2. Google ScholarCross Ref
- Dominic Orchard and Nobuko Yoshida. 2016. Effects as sessions, sessions as effects. In Principles of Programming Languages (POPL). ACM, 568–581. Google ScholarDigital Library
- Xinming Ou, Gang Tan, Yitzhak Mandelbaum, and David Walker. 2004. Dynamic Typing with Dependent Types. In IFIP International Conference on Theoretical Computer Science, Vol. 155. Springer, 437–450. Google ScholarCross Ref
- Luca Padovani. 2017. A simple library implementation of binary sessions. Journal of Functional Programming 27 (2017), e4. Google ScholarCross Ref
- Frank Pfenning and Dennis Griffith. 2015. Polarized substructural session types. In International Conference on Foundations of Software Science and Computation Structures (LNCS), Vol. 9034. Springer, 3–22. Google ScholarCross Ref
- Jeff Polakow. 2015. Embedding a full linear Lambda calculus in Haskell. In Symposium on Haskell. ACM, 177–188. Google ScholarDigital Library
- Riccardo Pucella and Jesse A Tov. 2008. Haskell session types with (almost) no class. In Symposium on Haskell. ACM, 25–36. Google ScholarDigital Library
- Matthew Sackman and Susan Eisenbach. 2008. Session types in Haskell: Updating message passing for the 21st century. (2008).Google Scholar
- Alceste Scalas and Nobuko Yoshida. 2016. Lightweight session programming in Scala. In European Conference on ObjectOriented Programming (ECOOP) (LIPIcs). Schloss Dagstuhl, 21:1–21:28.Google Scholar
- Jeremy G. Siek and Walid Taha. 2006. Gradual Typing for Functional Languages. In Scheme and Functional Programming Workshop (Scheme). 81–92.Google Scholar
- Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John T. Boyland. 2015. Refined criteria for gradual typing. In Summit on Advances in Programming Languages (SNAPL) (LIPIcs), Vol. 32. Schloss Dagstuhl, 274–293.Google Scholar
- The Dart Team. 2014. Dart Programming Lanuage Specification. (2014). Google, 1.2 edition.Google Scholar
- Peter Thiemann. 2014. Session Types with Gradual Typing. In TGC (LNCS), Vol. 8902. Springer, 144–158. Google ScholarCross Ref
- Bernardo Toninho, Luís Caires, and Frank Pfenning. 2013. Higher-Order Processes, Functions, and Sessions: A Monadic Integration. In European Symposium on Programming (ESOP) (LNCS), Vol. 7792. Springer, 350–369.Google ScholarDigital Library
- Jesse A. Tov and Riccardo Pucella. 2010. Stateful contracts for affine types. In European Symposium on Programming (ESOP) (LNCS), Vol. 6012. Springer, 550–569. Google ScholarDigital Library
- Vasco Thudichum Vasconcelos. 2012. Fundamentals of Session Types. Information and Computation 217 (2012), 52–70. Google ScholarDigital Library
- Julien Verlaguet. 2013. Facebook: Analysing PHP Statically. In Workshop on Commercial Uses of Functional Programming (CUFP).Google Scholar
- Philip Wadler. 2012. Propositions as sessions. In International Conference on Functional Programming (ICFP). ACM, 273–286. Google ScholarDigital Library
- Philip Wadler. 2014. Propositions as sessions. Journal of Functional Programming 24, 2-3 (2014), 384–418.Google ScholarCross Ref
- Philip Wadler. 2015. A Complement to Blame. In 1st Summit on Advances in Programming Languages (SNAPL) (LIPIcs), Vol. 32. Schloss Dagstuhl, 309–320.Google Scholar
- Philip Wadler and Robert Bruce Findler. 2009. Well-Typed Programs Can’t Be Blamed. In European Symposium on Programming (ESOP) (LNCS), Vol. 5502. Springer, 1–16. Google ScholarDigital Library
- David Walker. 2005. Advanced Topics in Types and Programming Languages. MIT Press, Chapter Substructural Type Systems, 3–43.Google Scholar
- Jack Williams, J. Garrett Morris, Philip Wadler, and Jakub Zalewski. 2017. Mixed Messages: Measuring Conformance and Non-Interference in TypeScript. In European Conference on Object-Oriented Programming (ECOOP) (LIPIcs), Vol. 74. Schloss Dagstuhl, Dagstuhl, Germany, 28:1–28:29.Google Scholar
- Max Willsey, Rokhini Prabhu, and Frank Pfenning. 2017. Design and Implementation of Concurrent C0. In International Workshop on Linearity (EPTCS), Vol. 238. 73–82. Google ScholarCross Ref
- Roger Wolff, Ronald Garcia, Éric Tanter, and Jonathan Aldrich. 2011. Gradual typestate. In European Conference on ObjectOriented Programming (ECOOP) (LNCS), Vol. 6813. Springer, 459–483. Google ScholarCross Ref
- Nobuko Yoshida, Raymond Hu, Rumyana Neykova, and Nicholas Ng. 2014. The Scribble protocol language. In International Symposium on Trustworthy Global Computing (LNCS), Vol. 8358. Springer, 22–41. Google ScholarDigital Library
- Nobuko Yoshida and Vasco Vasconcelos. 2007. Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. ENTCS 171, 4 (2007), 73–93. Google ScholarDigital Library
Index Terms
- Gradual session types
Recommendations
Context-free session types
ICFP '16Session types describe structured communication on heterogeneously typed channels at a high level. Their tail-recursive structure imposes a protocol that can be described by a regular language. The types of transmitted values are drawn from the ...
Partial Gradual Dependent Type Theory
SPLASH 2023: Companion Proceedings of the 2023 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for HumanityGradual typing supports imprecise types in the type system, allowing incremental migration from untyped code to typed in the same language. Through the gradual typing approach, our ongoing work proposes a new theory based on the Martin-Löf type theory ...
Context-free session types
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingSession types describe structured communication on heterogeneously typed channels at a high level. Their tail-recursive structure imposes a protocol that can be described by a regular language. The types of transmitted values are drawn from the ...
Comments