A Typed Lambda Calculus with Gradual Intersection Types
Article No.: 9, Pages 1 - 13
Abstract
Intersection types have the power to type expressions which are all of many different types. Gradual types combine type checking at both compile-time and run-time. Here we combine these two approaches in a new typed calculus that harness both of their strengths. We incorporate these two contributions in a single typed calculus and define an operational semantics with type cast annotations. We also prove several crucial properties of the type system, namely that types are preserved during compilation and evaluation, and that the refined criteria for gradual typing holds.
References
[1]
Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner. 2018. Tight typings and split bounds. Proc. ACM Program. Lang. 2, ICFP (2018), 94:1–94:30.
[2]
Amal Ahmed, Robert Bruce Findler, Jeremy G. Siek, and Philip Wadler. 2011. Blame for All. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Austin, Texas, USA) (POPL ’11). Association for Computing Machinery, New York, NY, USA, 201–214. https://doi.org/10.1145/1926385.1926409
[3]
Sandra Alves, Delia Kesner, and Daniel Ventura. 2019. A Quantitative Understanding of Pattern Matching. In 25th International Conference on Types for Proofs and Programs, TYPES 2019(LIPIcs, Vol. 175). 3:1–3:36.
[4]
Pedro Ângelo and Mário Florido. 2018. Gradual Intersection Types. In Ninth Workshop on Intersection Types and Related Systems, ITRS 2018, Oxford, U.K., 8 July 2018. https://pedroangelo.github.io/gradual-intersection-types.pdf
[5]
Pedro Ângelo and Mário Florido. 2020. Type Inference for Rank 2 Gradual Intersection Types. In Trends in Functional Programming, William J. Bowman and Ronald Garcia (Eds.). Springer International Publishing, Cham, 84–120. https://doi.org/10.1007/978-3-030-47147-7_5
[6]
Pedro Ângelo and Mário Florido. 2022. A Typed Lambda Calculus with Gradual Intersection Types. Technical Report. Faculdade de Ciências & LIACC, Universidade do Porto. 28 pages. https://raw.githubusercontent.com/pedroangelo/papers/master/angelo2022typed_complete.pdf
[7]
Steffen van Bakel. 1996. Rank 2 Intersection Type Assignment in Term Rewriting. Fundam. Inf. 26, 2 (May 1996), 141–166.
[8]
Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic 48, 4 (1983), 931–940. https://doi.org/10.2307/2273659
[9]
Lorenzo Bettini, Viviana Bono, Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. 2018. Java & Lambda: a Featherweight Story. Logical Methods in Computer Science Volume 14, Issue 3 (Sept. 2018). https://doi.org/10.23638/LMCS-14(3:17)2018
[10]
Viviana Bono, Betti Venneri, and Lorenzo Bettini. 2008. A Typed Lambda Calculus with Intersection Types. Theor. Comput. Sci. 398, 1–3 (May 2008), 95–113. https://doi.org/10.1016/j.tcs.2008.01.046
[11]
Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. 2017. Non-idempotent intersection types for the Lambda-Calculus. Log. J. IGPL 25, 4 (2017), 431–464.
[12]
Sébastien Carlier and J.B. Wells. 2005. Expansion: the Crucial Mechanism for Type Inference with Intersection Types: A Survey and Explanation. Electronic Notes in Theoretical Computer Science 136 (2005), 173 – 202. https://doi.org/10.1016/j.entcs.2005.03.026 Proceedings of the Third International Workshop on Intersection Types and Related Systems (ITRS 2004).
[13]
Giuseppe Castagna and Victor Lanvin. 2017. Gradual Typing with Union and Intersection Types. Proc. ACM Program. Lang. 1, ICFP, Article 41 (Aug. 2017), 28 pages. https://doi.org/10.1145/3110285
[14]
Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek. 2019. Gradual Typing: A New Perspective. Proc. ACM Program. Lang. 3, POPL, Article 16 (Jan. 2019), 32 pages. https://doi.org/10.1145/3290329
[15]
Avik Chaudhuri. 2016. Flow: Abstract Interpretation of JavaScript for Type Checking and Beyond. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security(Vienna, Austria) (PLAS ’16). Association for Computing Machinery, New York, NY, USA, 1. https://doi.org/10.1145/2993600.2996280
[16]
Matteo Cimini and Jeremy G. Siek. 2016. The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg, FL, USA) (POPL ’16). ACM, New York, NY, USA, 443–455. https://doi.org/10.1145/2837614.2837632
[17]
Matteo Cimini and Jeremy G. Siek. 2017. Automatically Generating the Dynamic Semantics of Gradually Typed Languages. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Paris, France) (POPL 2017). ACM, New York, NY, USA, 789–803. https://doi.org/10.1145/3009837.3009863
[18]
M. Coppo and M. Dezani-Ciancaglini. 1980. An extension of the basic functionality theory for the λ-calculus.Notre Dame Journal of Formal Logic 21, 4 (10 1980), 685–693. https://doi.org/10.1305/ndjfl/1093883253
[19]
Mario Coppo, Mariangiola Dezani-Ciancaglini, and Patrick Sallé. 1979. Functional Characterization of Some Semantic Equalities inside Lambda-Calculus. In Automata, Languages and Programming, 6th Colloquium, July 16-20, 1979(Lecture Notes in Computer Science, Vol. 71). Springer, 133–146.
[20]
M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. 1981. Functional Characters of Solvable Terms. Mathematical Logic Quarterly 27, 2-6 (1981), 45–58. https://doi.org/10.1002/malq.19810270205 arXiv:https://onlinelibrary.wiley.com/doi/pdf/10.1002/malq.19810270205
[21]
Vincent Cremet, François Garillot, Sergueï Lenglet, and Martin Odersky. 2006. A Core Calculus for Scala Type Checking. In Mathematical Foundations of Computer Science 2006, Rastislav Královičand Paweł Urzyczyn (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 1–23.
[22]
Ferruccio Damiani. 2003. Rank 2 Intersection Types for Local Definitions and Conditional Expressions. ACM Trans. Program. Lang. Syst. 25, 4 (July 2003), 401–451. https://doi.org/10.1145/778559.778560
[23]
Mariangiola Dezani-Ciancaglini, Paola Giannini, and Betti Venneri. 2019. Intersection Types in Java: Back to the Future. Springer International Publishing, Cham, 68–86. https://doi.org/10.1007/978-3-030-22348-9_6
[24]
Ronald Garcia and Matteo Cimini. 2015. Principal Type Schemes for Gradual Programs. In Proceedings of the 42Nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Mumbai, India) (POPL ’15). ACM, New York, NY, USA, 303–315. https://doi.org/10.1145/2676726.2676992
[25]
Ronald Garcia, Alison M. Clark, and Éric Tanter. 2016. Abstracting Gradual Typing. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg, FL, USA) (POPL ’16). ACM, New York, NY, USA, 429–442. https://doi.org/10.1145/2837614.2837670
[26]
T. Jim. 1995. Rank 2 Type Systems and Recursive Definitions. Technical Report. Cambridge, MA, USA.
[27]
Trevor Jim. 1996. What Are Principal Typings and What Are They Good for?. In Proceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (St. Petersburg Beach, Florida, USA) (POPL ’96). ACM, New York, NY, USA, 42–53. https://doi.org/10.1145/237721.237728
[28]
Matthias Keil and Peter Thiemann. 2015. Blame Assignment for Higher-Order Contracts with Intersection and Union. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Vancouver, BC, Canada) (ICFP 2015). Association for Computing Machinery, New York, NY, USA, 375–386. https://doi.org/10.1145/2784731.2784737
[29]
Delia Kesner and Pierre Vial. 2020. Non-idempotent types for classical calculi in natural deduction style. Log. Methods Comput. Sci. 16, 1 (2020).
[30]
A.J. Kfoury and J.B. Wells. 2004. Principality and type inference for intersection types using expansion variables. Theoretical Computer Science 311, 1 (2004), 1 – 70. https://doi.org/10.1016/j.tcs.2003.10.032
[31]
A. J. Kfoury and J. B. Wells. 1999. Principality and Decidable Type Inference for Finite-rank Intersection Types. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Antonio, Texas, USA) (POPL ’99). ACM, New York, NY, USA, 161–174. https://doi.org/10.1145/292540.292556
[32]
Daniel Leivant. 1983. Polymorphic Type Inference. In Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (Austin, Texas) (POPL ’83). Association for Computing Machinery, New York, NY, USA, 88–98. https://doi.org/10.1145/567067.567077
[33]
Luigi Liquori and Simona Ronchi Della Rocca. 2007. Intersection-types à la Church. Information and Computation 205, 9 (2007), 1371 – 1386. https://doi.org/10.1016/j.ic.2007.03.005
[34]
Luigi Liquori and Claude Stolze. 2019. The Delta-calculus: Syntax and Types. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 131), Herman Geuvers (Ed.). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 28:1–28:20. https://doi.org/10.4230/LIPIcs.FSCD.2019.28
[35]
Yuki Nishida and Atsushi Igarashi. 2019. Manifest Contracts with Intersection Types. In Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings(Lecture Notes in Computer Science, Vol. 11893), Anthony Widjaja Lin (Ed.). Springer, 33–52. https://doi.org/10.1007/978-3-030-34175-6_3
[36]
G. Pottinger. 1980. A Type Assignment for the Strongly Normalizable Lambda-Terms. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. Hindley and J. Seldin (Eds.). Academic Press, 561–577.
[37]
John C. Reynolds. 1997. Design of the Programming Language Forsythe. Birkhäuser Boston, Boston, MA, 173–233. https://doi.org/10.1007/978-1-4612-4118-8_9
[38]
Simona Ronchi Della Rocca. 2003. Intersection Typed λ-calculus. Electronic Notes in Theoretical Computer Science 70, 1 (2003), 163 – 181. https://doi.org/10.1016/S1571-0661(04)80496-1 ITRS ’02, Intersection Types and Related Systems (FLoC Satellite Event).
[39]
Jeremy G Siek and Walid Taha. 2006. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, Vol. 6. 81–92.
[40]
Jeremy G. Siek and Manish Vachharajani. 2008. Gradual Typing with Unification-based Inference. In Proceedings of the 2008 Symposium on Dynamic Languages (Paphos, Cyprus) (DLS ’08). ACM, New York, NY, USA, Article 7, 12 pages. https://doi.org/10.1145/1408681.1408688
[41]
Jeremy G. Siek, Michael M. Vitousek, Matteo Cimini, and John Tang Boyland. 2015. Refined Criteria for Gradual Typing. In 1st Summit on Advances in Programming Languages (SNAPL 2015)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 32). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 274–293. https://doi.org/10.4230/LIPIcs.SNAPL.2015.274
[42]
Stephanus Johannes Van Bakel. 1993. Intersection type disciplines in lambda calculus and applicative term rewriting systems. Amsterdam: Mathematisch Centrum.
[43]
Panagiotis Vekris, Benjamin Cosman, and Ranjit Jhala. 2016. Refinement Types for TypeScript. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (Santa Barbara, CA, USA) (PLDI ’16). Association for Computing Machinery, New York, NY, USA, 310–325. https://doi.org/10.1145/2908080.2908110
[44]
Joe B. Wells and Christian Haack. 2002. Branching Types. In Proceedings of the 11th European Symposium on Programming Languages and Systems(ESOP ’02). Springer-Verlag, London, UK, UK, 115–132. http://dl.acm.org/citation.cfm?id=645396.651968
[45]
Jack Williams, J. Garrett Morris, and Philip Wadler. 2018. The Root Cause of Blame: Contracts for Intersection and Union Types. Proc. ACM Program. Lang. 2, OOPSLA, Article 134 (Oct. 2018), 29 pages. https://doi.org/10.1145/3276504
Index Terms
- A Typed Lambda Calculus with Gradual Intersection Types
Recommendations
Gradual typing: a new perspective
We define a new, more semantic interpretation of gradual types and use it to ``gradualize'' two forms of polymorphism: subtyping polymorphism and implicit parametric polymorphism. In particular, we use the new interpretation to define three gradual type ...
Gradual typing with union and intersection types
We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...
A typed lambda calculus with intersection types
Intersection types are well known to type theorists mainly for two reasons. Firstly, they type all and only the strongly normalizable lambda terms. Secondly, the intersection type operator is a meta-level operator, that is, there is no direct logical ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
September 2022
187 pages
ISBN:9781450397032
DOI:10.1145/3551357
Copyright © 2022 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 ACM 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]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 20 September 2022
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
PPDP 2022
PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming
September 20 - 22, 2022
Tbilisi, Georgia
Acceptance Rates
Overall Acceptance Rate 230 of 486 submissions, 47%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 98Total Downloads
- Downloads (Last 12 months)48
- Downloads (Last 6 weeks)7
Reflects downloads up to 13 Nov 2024
Other Metrics
Citations
View Options
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML FormatGet Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in