Abstract
Session types statically describe communication protocols between concurrent message-passing processes. Unfortunately, parametric polymorphism even in its restricted prenex form is not fully understood in the context of session types. In this paper, we present the metatheory of session types extended with prenex polymorphism and, as a result, nested recursive datatypes. Remarkably, we prove that type equality is decidable by exhibiting a reduction to trace equivalence of deterministic first-order grammars. Recognizing the high theoretical complexity of the latter, we also propose a novel type equality algorithm and prove its soundness. We observe that the algorithm is surprisingly efficient and, despite its incompleteness, sufficient for all our examples. We have implemented our ideas by extending the Rast programming language with nested session types. We conclude with several examples illustrating the expressivity of our enhanced type system.
Chapter PDF
Similar content being viewed by others
References
Almeida, B., Mordido, A., Vasconcelos, V.T.: Deciding the bisimilarity of context-free session types. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12079, pp. 39–56. Springer (2020). https://doi.org/10.1007/978-3-030-45237-7_3, https://doi.org/10.1007/978-3-030-45237-7
Bergstra, J.A., Klop, J.W.: Acp\(\tau \) a universal axiom system for process specification. In: Wirsing, M., Bergstra, J.A. (eds.) Algebraic Methods: Theory, Tools and Applications. pp. 445–463. Springer Berlin Heidelberg, Berlin, Heidelberg (1989)
Bird, R.S., Meertens, L.G.L.T.: Nested datatypes. In: Jeuring, J. (ed.) Mathematics of Program Construction, MPC’98, Marstrand, Sweden, June 15-17, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1422, pp. 52–67. Springer (1998). https://doi.org/10.1007/BFb0054285
Bono, V., Padovani, L.: Polymorphic endpoint types for copyless message passing. In: Silva, A., Bliudze, S., Bruni, R., Carbone, M. (eds.) Proceedings Fourth Interaction and Concurrency Experience, ICE 2011, Reykjavik, Iceland, 9th June 2011. EPTCS, vol. 59, pp. 52–67 (2011). https://doi.org/10.4204/EPTCS.59.5
Bono, V., Padovani, L.: Typing copyless message passing. Log. Methods Comput. Sci. 8(1) (2012). https://doi.org/10.2168/LMCS-8(1:17)2012
Caires, L., Pérez, J.A., Pfenning, F., Toninho, B.: Behavioral polymorphism and parametricity in session-based communication. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. pp. 330–349. Springer, Berlin Heidelberg, Berlin, Heidelberg (2013)
Caires, L., Pfenning, F.: Session types as intuitionistic linear propositions. In: P. Gastin, F. Laroussinie (eds.) Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010). pp. 222–236. Springer LNCS 6269, Paris, France (Aug 2010)
Caires, L., Pfenning, F., Toninho, B.: Linear logic propositions as session types. Mathematical Structures in Computer Science 760 (11 2014)
Cervesato, I., Scedrov, A.: Relating state-based and process-based concurrency through linear logic (full-version). Information and Computation 207(10), 1044 – 1077 (2009). https://doi.org/10.1016/j.ic.2008.11.006, special issue: 13th Workshop on Logic, Language, Information and Computation (WoLLIC 2006)
Connelly, R.H., Morris, F.L.: A generalisation of the trie data structure. Mathematical Structures in Computer Science 5(3), 381–418 (1995)
Dardha, O.: Recursive session types revisited. In: Carbone, M. (ed.) Third Workshop on Behavioural Types (BEAT 2014). pp. 27–34. EPTCS 162 (Sep 2014)
Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Inf. Comput. 256, 253–286 (2017). https://doi.org/10.1016/j.ic.2017.06.002
Das, A., Derakhshan, F., Pfenning, F.: Rast implementation. https://bitbucket.org/fpfenning/rast/src/master/ (2019), accessed: 2019-11-11
Das, A., DeYoung, H., Mordido, A., Pfenning, F.: Nested polymorphic session types (2020), https://arxiv.org/abs/2010.06482
Das, A., Hoffmann, J., Pfenning, F.: Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang. 2(ICFP), 91:1–91:30 (Jul 2018). https://doi.org/10.1145/3236786
Das, A., Hoffmann, J., Pfenning, F.: Work analysis with resource-aware session types. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 305–314. LICS ’18, ACM, New York, NY, USA (2018). https://doi.org/10.1145/3209108.3209146
Das, A., Pfenning, F.: Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description). In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 167, pp. 33:1–33:17. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020). https://doi.org/10.4230/LIPIcs.FSCD.2020.33
Das, A., Pfenning, F.: Session Types with Arithmetic Refinements. In: Konnov, I., Kovács, L. (eds.) 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 171, pp. 13:1–13:18. Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2020). https://doi.org/10.4230/LIPIcs.CONCUR.2020.13
Das, A., Pfenning, F.: Verified linear session-typed concurrent programming. In: 22nd International Symposium on Principles and Practice of Declarative Programming. PPDP ’20, Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3414080.3414087
Derakhshan, F., Pfenning, F.: Circular Proofs as Session-Typed Processes: A Local Validity Condition. arXiv e-prints \({\rm arXiv{:}1908.01909}\) (Aug 2019)
Dyck: Gruppentheoretische studien. (mit drei lithographirten tafeln.). Mathematische Annalen 20, 1–44 (1882), http://eudml.org/doc/157013
Friedman, E.P.: The inclusion problem for simple languages. Theor. Comput. Sci. 1(4), 297–316 (1976). https://doi.org/10.1016/0304-3975(76)90074-8
Gay, S., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2), 191–225 (Nov 2005). https://doi.org/10.1007/s00236-005-0177-z
Gay, S.J.: Bounded polymorphism in session types. Math. Struct. Comput. Sci. 18(5), 895–930 (2008). https://doi.org/10.1017/S0960129508006944
Girard, J.Y., Lafont, Y.: Linear logic and lazy computation. In: Ehrig, H., Kowalski, R., Levi, G., Montanari, U. (eds.) TAPSOFT ’87. pp. 52–66. Springer Berlin Heidelberg, Berlin, Heidelberg (1987)
Griffith, D.: Polarized Substructural Session Types. Ph.D. thesis, University of Illinois at Urbana-Champaign (Apr 2016)
Henry, P., Sénizergues, G.: Lalblc a program testing the equivalence of dpda’s. In: International Conference on Implementation and Application of Automata. pp. 169–180. Springer (2013)
Hinze, R.: Generalizing generalized tries. Journal of Functional Pogramming 10(4), 327–351 (Jul 2010)
Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR’93. pp. 509–523. Springer, Berlin Heidelberg, Berlin, Heidelberg (1993)
Jančar, P.: Short decidability proof for DPDA language equivalence via 1st order grammar bisimilarity. CoRR abs/1010.4760 (2010), http://arxiv.org/abs/1010.4760
Jancar, P.: Bisimilarity on basic process algebra is in 2-exptime (an explicit proof). arXiv preprint \({\rm arXiv{:}1207.2479}\) (2012)
Johann, P., Ghani, N.: Haskell programming with nested types: A principled approach. Higher-Order and Symbolic Computation 22(2), 155–189 (Jun 2009)
Kobayashi, N.: Type systems for concurrent programs. In: Aichernig, B.K., Maibaum, T.S.E. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, March 18-20, 2002, Revised Papers. Lecture Notes in Computer Science, vol. 2757, pp. 439–453. Springer (2002). https://doi.org/10.1007/978-3-540-40007-3_26
Korenjak, A.J., Hopcroft, J.E.: Simple deterministic languages. In: 7th Annual Symposium on Switching and Automata Theory (swat 1966). pp. 36–46. IEEE (1966)
Lindley, S., Morris, J.G.: Talking bananas: Structural recursion for session types. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. p. 434–447. ICFP 2016, Association for Computing Machinery, New York, NY, USA (2016). https://doi.org/10.1145/2951913.2951921
Mycroft, A.: Polymorphic type schemes and recursive definitions. In: Paul, M., Robinet, B. (eds.) International Symposium on Programming. pp. 217–228. Springer Berlin Heidelberg, Berlin, Heidelberg (1984)
Okasaki, C.: Purely Functional Data Structures. Ph.D. thesis, Department of Computer Science, Carnegie Mellon University (1996)
Pérez, J.A., Caires, L., Pfenning, F., Toninho, B.: Linear logical relations and observational equivalences for session-based concurrency. Information and Computation 239, 254–302 (2014)
Pfenning, F., Griffith, D.: Polarized substructural session types. In: Pitts, A. (ed.) Foundations of Software Science and Computation Structures. pp. 3–22. Springer Berlin Heidelberg, Berlin, Heidelberg (2015)
Pierce, B.C., Turner, D.N.: Local type inference. ACM Trans. Program. Lang. Syst. 22(1), 1–44 (Jan 2000). https://doi.org/10.1145/345099.345100
Sénizergues, G.: L(a)=l(b)? A simplified decidability proof. Theor. Comput. Sci. 281(1-2), 555–608 (2002). https://doi.org/10.1016/S0304-3975(02)00027-0
Solomon, M.H.: Type definitions with parameters. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978. pp. 31–38. ACM Press (1978). https://doi.org/10.1145/512760.512765
Stirling, C.: Decidability of DPDA equivalence. Theor. Comput. Sci. 255(1-2), 1–31 (2001). https://doi.org/10.1016/S0304-3975(00)00389-3
Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Maritsas, D.G., Philokyprou, G., Theodoridis, S. (eds.) PARLE ’94: Parallel Architectures and Languages Europe, 6th International PARLE Conference, Athens, Greece, July 4-8, 1994, Proceedings. Lecture Notes in Computer Science, vol. 817, pp. 398–413. Springer (1994). https://doi.org/10.1007/3-540-58184-7_118
Thiemann, P., Vasconcelos, V.T.: Context-free session types. In: Garrigue, J., Keller, G., Sumii, E. (eds.) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Japan. pp. 462–475. ACM (2016). https://doi.org/10.1145/2951913.2951926, https://doi.org/10.1145/2951913
Thiemann, P., Vasconcelos, V.T.: Label-dependent session types. Proceedings of the ACM on Programming Languages 4(POPL), 67:1–67:29 (2020). https://doi.org/10.1145/3371135
Wadler, P.: Propositions as sessions. In: Thiemann, P., Findler, R.B. (eds.) ACM SIGPLAN International Conference on Functional Programming, ICFP’12, Copenhagen, Denmark, September 9-15, 2012. pp. 273–286. ACM (2012). https://doi.org/10.1145/2364527.2364568, https://doi.org/10.1145/2364527.2364568
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Das, A., DeYoung, H., Mordido, A., Pfenning, F. (2021). Nested Session Types. In: Yoshida, N. (eds) Programming Languages and Systems. ESOP 2021. Lecture Notes in Computer Science(), vol 12648. Springer, Cham. https://doi.org/10.1007/978-3-030-72019-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-72019-3_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72018-6
Online ISBN: 978-3-030-72019-3
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
