Cited By
View all- Abel ADanielsson NEriksson O(2023)A Graded Modal Dependent Type Theory with a Universe and Erasure, FormalizedProceedings of the ACM on Programming Languages10.1145/36078627:ICFP(920-954)Online publication date: 31-Aug-2023
A theory of higher-order subtyping with type intervals
Article No.: 69, Pages 1 - 30
Abstract
The calculus of Dependent Object Types (DOT) has enabled a more principled and robust implementation of Scala, but its support for type-level computation has proven insufficient. As a remedy, we propose F··ω, a rigorous theoretical foundation for Scala’s higher-kinded types. F··ω extends F<:ω with interval kinds, which afford a unified treatment of important type- and kind-level abstraction mechanisms found in Scala, such as bounded quantification, bounded operator abstractions, translucent type definitions and first-class subtyping constraints. The result is a flexible and general theory of higher-order subtyping. We prove type and kind safety of F··ω, as well as weak normalization of types and undecidability of subtyping. All our proofs are mechanized in Agda using a fully syntactic approach based on hereditary substitution.
Supplementary Material
Extended version. This version of the paper has a number of appendices containing detailed human-readable descriptions of metatheoretic results that have been omitted from the paper, and an overview of the Agda formalization, establishing the connection to the theory presented in the paper.
- Download
- 913.39 KB
Extended version. This version of the paper has a number of appendices containing detailed human-readable descriptions of metatheoretic results that have been omitted from the paper, and an overview of the Agda formalization, establishing the connection to the theory presented in the paper.
- Download
- 68.45 MB
Presentation Videos
- Download
- 52.64 MB
References
[1]
Andreas Abel. 2008. Polarized Subtyping for Sized Types. Mathematical Structures in Computer Science, 18 (2008), 10, 797–822. issn:1469-8072 https://doi.org/10.1017/S0960129508006853
[2]
Andreas Abel and Dulma Rodriguez. 2008. Syntactic Metatheory of Higher-Order Subtyping. In Proceedings of the 22nd International Workshop on Computer Science Logic (CSL 2008), 17th Annual Conference of the EACSL, Bertinoro, Italy, Michael Kaminski and Simone Martini (Eds.) (LNCS, Vol. 5213). Springer, Berlin, Heidelberg. 446–460. isbn:978-3-540-87531-4 https://doi.org/10.1007/978-3-540-87531-4_32
[3]
Robin Adams. 2006. Pure type systems with judgemental equality. Journal of Functional Programming, 16, 2 (2006), 219–246. https://doi.org/10.1017/S0956796805005770
[4]
Nada Amin. 2016. Dependent Object Types. Ph.D. Dissertation. School of Computer and Communication Sciences, École polytechnique fédérale de Lausanne. Lausanne, Switzerland. https://doi.org/10.5075/epfl-thesis-7156 EPFL thesis no. 7156.
[5]
Nada Amin, Samuel Grütter, Martin Odersky, Tiark Rompf, and Sandro Stucki. 2016. The Essence of Dependent Object Types. In A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella (Eds.) (LNCS, Vol. 9600). Springer International Publishing, Cham. 249–272. isbn:978-3-319-30936-1 https://doi.org/10.1007/978-3-319-30936-1_14
[6]
Nada Amin, Tiark Rompf, and Martin Odersky. 2014. Foundations of Path-dependent Types. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA 2014), Portland, Oregon, USA. ACM, New York, NY, USA. 233–249. isbn:978-1-4503-2585-1 https://doi.org/10.1145/2660193.2660216
[7]
David Aspinall and Adriana Compagnoni. 2001. Subtyping dependent types. Theoretical Computer Science, 266, 1-2 (2001), 273–309. issn:0304-3975 https://doi.org/10.1016/S0304-3975(00)00175-4
[8]
Hendrik P. Barendregt. 1992. Lambda Calculi with Types. In Handbook of Logic in Computer Science, Samson Abramsky, Dov M. Gabbay, and Thomas S. E Maibaum (Eds.). 2, Oxford University Press, Oxford, UK. 117–309. isbn:0-19-853761-1
[9]
Luca Cardelli. 1988. Structural Subtyping and the Notion of Power Type. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1988), San Diego, California, USA. ACM, New York, NY, USA. 70–79. isbn:0-89791-252-7 https://doi.org/10.1145/73560.73566
[10]
Luca Cardelli. 1990. Notes about F^ω. October, Unpublished manuscript.
[11]
Luca Cardelli and Giuseppe Longo. 1991. A Semantic Basis for Quest. Journal of Functional Programming, 1, 4 (1991), 417–458. https://doi.org/10.1017/S0956796800000198
[12]
Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. 1991. An extension of system F with subtyping. In Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS 1991), Sendai, Japan, Takayasu Ito and Albert R. Meyer (Eds.). Springer, Berlin, Heidelberg. 750–770. isbn:978-3-540-47617-7 https://doi.org/10.1007/3-540-54415-1_73
[13]
Luca Cardelli and Peter Wegner. 1985. On Understanding Types, Data Abstraction, and Polymorphism. Comput. Surveys, 17, 4 (1985), Dec., 471–523. issn:0360-0300 https://doi.org/10.1145/6041.6042
[14]
Simon Castellan, Pierre Clairambault, and Peter Dybjer. 2015. Undecidability of Equality in the Free Locally Cartesian Closed Category. In 13th International Conference on Typed Lambda Calculi and Applications, (TLCA 2015), Warsaw, Poland, Thorsten Altenkirch (Ed.) (LIPIcs, Vol. 38). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany. 138–152. https://doi.org/10.4230/LIPIcs.TLCA.2015.138
[15]
Adriana Compagnoni and Healfdene Goguen. 1999. Anti-Symmetry of Higher-Order Subtyping. In Proceedings of the 13th International Workshop on Computer Science Logic (CSL 1999), 8th Annual Conference of the EACSL Madrid, Spain, Jörg Flum and Mario Rodriguez-Artalejo (Eds.) (LNCS, Vol. 1683). Springer, Berlin, Heidelberg. 420–438. isbn:978-3-540-48168-3 https://doi.org/10.1007/3-540-48168-0_30
[16]
Adriana Compagnoni and Healfdene Goguen. 2003. Typed operational semantics for higher-order subtyping. Information and Computation, 184, 2 (2003), 242–297. issn:0890-5401 https://doi.org/10.1016/S0890-5401(03)00062-2
[17]
Adriana B. Compagnoni. 1995. Decidability of higher-order subtyping with intersection types. In Computer Science Logic, 8th International Workshop, (CSL 1994), Kazimierz, Poland, September 25–30, 1994, Selected Papers, Leszek Pacholski and Jerzy Tiuryn (Eds.) (LNCS, Vol. 933). Springer, Berlin, Heidelberg. 46–60. isbn:978-3-540-49404-1 https://doi.org/10.1007/BFb0022246
[18]
Karl Crary. 1997. Foundations for the Implementation of Higher-order Subtyping. In Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming (ICFP 1997), Amsterdam, The Netherlands. ACM, New York, NY, USA. 125–135. isbn:0-89791-918-1 https://doi.org/10.1145/258948.258961
[19]
Karl Crary. 2009. A Syntactic Account of Singleton Types via Hereditary Substitution. In Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, Theory and Practice (LFMTP 2009), Montreal, Quebec, Canada. ACM, New York, NY, USA. 21–29. isbn:978-1-60558-529-1 https://doi.org/10.1145/1577824.1577829
[20]
Julien Cretin and Didier Rémy. 2014. System F with Coercion Constraints. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL 2014) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2014), Vienna, Austria. ACM, New York, NY, USA. Article 34, 10 pages. isbn:978-1-4503-2886-9 https://doi.org/10.1145/2603088.2603128
[21]
Pierre-Louis Curien and Giorgio Ghelli. 1992. Coherence of Subsumption, Minimum Typing and Type-checking in F≤. Mathematical Structures in Computer Science, 2, 1 (1992), March, 55–91. https://doi.org/10.1017/S0960129500001134
[22]
The Dotty Team. 2020. Scala 3 – A next-generation compiler for Scala –. http://dotty.epfl.ch Source code available from.
[23]
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, and Robbert Krebbers. 2020. Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris. PACMPL, 4, ICFP (2020), Article 114, Aug., 29 pages. https://doi.org/10.1145/3408996
[24]
Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph.D. Dissertation. Université Paris VII.
[25]
Robert Harper and Daniel R. Licata. 2007. Mechanizing Metatheory in a Logical Framework. Journal of Functional Programming, 17, 4-5 (2007), July, 613–673. issn:0956-7968 https://doi.org/10.1017/S0956796807006430
[26]
Robert Harper and Mark Lillibridge. 1994. A Type-theoretic Approach to Higher-order Modules with Sharing. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1994), Portland, Oregon, USA. ACM, New York, NY, USA. 123–137. isbn:0-89791-636-0 https://doi.org/10.1145/174675.176927
[27]
Robert Harper and Frank Pfenning. 2005. On Equivalence and Canonical Forms in the LF Type Theory. ACM Transactions on Computational Logic, 6, 1 (2005), Jan., 61–101. issn:1529-3785 https://doi.org/10.1145/1042038.1042041
[28]
Jason Z. S. Hu and Ondřej Lhoták. 2019. Undecidability of D: And Its Decidable Fragments. PACMPL, 4, POPL (2019), Article 9, Dec., 30 pages. https://doi.org/10.1145/3371077
[29]
Chantal Keller and Thorsten Altenkirch. 2010. Hereditary Substitutions for Simple Types, Formalized. In Proceedings of the Third ACM SIGPLAN Workshop on Mathematically Structured Functional Programming (MSFP 2010), Baltimore, Maryland, USA. ACM, New York, NY, USA. 3–10. isbn:978-1-4503-0255-5 https://doi.org/10.1145/1863597.1863601
[30]
Daniel K. Lee, Karl Crary, and Robert Harper. 2007. Towards a Mechanized Metatheory of Standard ML. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), Nice, France. ACM, New York, NY, USA. 173–184. isbn:1-59593-575-4 https://doi.org/10.1145/1190216.1190245
[31]
Adriaan Moors, Frank Piessens, and Martin Odersky. 2008. Generics of a Higher Kind. In Proceedings of the 23rd ACM SIGPLAN Conference on Object-oriented Programming Systems Languages and Applications (OOPSLA 2008), Nashville, TN, USA. ACM, New York, NY, USA. 423–438. isbn:978-1-60558-215-3 https://doi.org/10.1145/1449764.1449798
[32]
Adriaan Moors, Frank Piessens, and Martin Odersky. 2008. Safe type-level abstraction in Scala. In Proceedings of the International Workshop on Foundations of Object-Oriented Languages (FOOL 2008), San Francisco, CA, USA. 1–13. https://www.cs.cmu.edu/~aldrich/FOOL/fool08/moors.pdf
[33]
Bengt Nordström, Kent Petersson, and Jan M. Smith. 1990. Programming in Martin-Löf’s type theory. 200, Oxford University Press, Oxford, UK.
[34]
Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology. Göteborg, Sweden.
[35]
Martin Odersky, Guillaume Martres, and Dmitry Petrashko. 2016. Implementing Higher-kinded Types in Dotty. In Proceedings of the 7th ACM SIGPLAN Symposium on Scala (SCALA@SPLASH 2016), Amsterdam, Netherlands. ACM, New York, NY, USA. 51–60. isbn:978-1-4503-4648-1 https://doi.org/10.1145/2998392.2998400
[36]
Lionel Parreaux, Aleksander Boruch-Gruszecki, and Paolo G. Giarrusso. 2019. Towards Improved GADT Reasoning in Scala. In Proceedings of the Tenth ACM SIGPLAN Symposium on Scala (Scala 2019), London, United Kingdom. ACM, New York, NY, USA. 12–16. isbn:9781450368247 https://doi.org/10.1145/3337932.3338813
[37]
Benjamin Pierce and Martin Steffen. 1997. Higher-order subtyping. Theoretical Computer Science, 176, 1–2 (1997), 235–282. issn:0304-3975 https://doi.org/10.1016/S0304-3975(96)00096-5
[38]
Benjamin C. Pierce. 1992. Bounded Quantification is Undecidable. In Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1992), Albuquerque, NM, USA. Association for Computing Machinery, New York, NY, USA. 305–315. isbn:0897914538 https://doi.org/10.1145/143165.143228
[39]
Benjamin C. Pierce. 2002. Types and programming languages. MIT Press, Cambridge, MA, USA.
[40]
Marianna Rapoport and Ondřej Lhoták. 2019. A Path to DOT: Formalizing Fully Path-Dependent Types. PACMPL, 3, OOPSLA (2019), Article 145, Oct., 29 pages. https://doi.org/10.1145/3360571
[41]
Tiark Rompf and Nada Amin. 2016. Type Soundness for Dependent Object Types (DOT). In Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2016), Amsterdam, Netherlands. ACM, New York, NY, USA. 624–641. isbn:978-1-4503-4444-9 https://doi.org/10.1145/2983990.2984008
[42]
Gabriel Scherer and Didier Rémy. 2015. Full Reduction in the Face of Absurdity. In Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems (ESOP 2015), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2015), London, UK, Jan Vitek (Ed.) (LNCS, Vol. 9032). Springer, Berlin, Heidelberg. 685–709. isbn:978-3-662-46669-8 https://doi.org/10.1007/978-3-662-46669-8_28
[43]
Christopher A. Stone and Robert Harper. 2000. Deciding Type Equivalence in a Language with Singleton Kinds. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2000), Boston, MA, USA. ACM, New York, NY, USA. 214–227. isbn:1-58113-125-9 https://doi.org/10.1145/325694.325724
[44]
Sandro Stucki. 2017. Higher-Order Subtyping with Type Intervals. Ph.D. Dissertation. School of Computer and Communication Sciences, École polytechnique fédérale de Lausanne. Lausanne, Switzerland. https://doi.org/10.5075/epfl-thesis-8014
[45]
Sandro Stucki and Paolo G. Giarrusso. 2021. A Theory of Higher-order Subtyping with Type Intervals – Agda Formalization. https://doi.org/10.5281/zenodo.4775731
[46]
Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. 2004. A Concurrent Logical Framework: The Propositional Fragment. In International Workshop on Types for Proofs and Programs (TYPES 2003), Torino, Italy, April 30–May 4, 2003, Revised Selected Papers, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.) (LNCS, Vol. 3085). Springer, Berlin, Heidelberg. 355–377. isbn:978-3-540-24849-1 https://doi.org/10.1007/978-3-540-24849-1_23
[47]
Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation, 115, 1 (1994), Nov., 38–94. issn:0890-5401 https://doi.org/10.1006/inco.1994.1093
[48]
Yanpeng Yang and Bruno C. d. S. Oliveira. 2017. Unifying Typing and Subtyping. PACMPL, 1, OOPSLA (2017), Article 47, Oct., 26 pages. https://doi.org/10.1145/3133871
[49]
Jan Zwanenburg. 1999. Pure Type Systems with Subtyping. In Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA 1999), L’Aquila, Italy, Jean-Yves Girard (Ed.) (LNCS, Vol. 1581). Springer, Berlin, Heidelberg. 381–396. isbn:978-3-540-65763-7 https://doi.org/10.1007/3-540-48959-2_27
Index Terms
- A theory of higher-order subtyping with type intervals
Recommendations
On the power of coercion abstraction
POPL '12Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model ...
On the power of coercion abstraction
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesErasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model ...
System F with coercion constraints
CSL-LICS '14: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)We present a second-order λ-calculus with coercion constraints that generalizes a previous extension of System F with parametric coercion abstractions by allowing multiple but simultaneous type and coercion abstractions, as well as recursive coercions ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2021 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 19 August 2021
Published in PACMPL Volume 5, Issue ICFP
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- European Research Council (ERC)
- Swedish Research Council (Vetenskapsrådet)
- Swedish Research Council (Vetenskapsrådet)
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 390Total Downloads
- Downloads (Last 12 months)110
- Downloads (Last 6 weeks)13
Reflects downloads up to 11 Dec 2024
Other Metrics
Citations
Cited By
View all- Abel ADanielsson NEriksson O(2023)A Graded Modal Dependent Type Theory with a Universe and Erasure, FormalizedProceedings of the ACM on Programming Languages10.1145/36078627:ICFP(920-954)Online publication date: 31-Aug-2023
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in