Yanpeng Yang
Skip Abstract Section
Skip Supplemental Material SectionAbstract
In recent years dependent types have become a hot topic in programming language research. A key reason why dependent types are interesting is that they allow unifying types and terms, which enables both additional expressiveness and economy of concepts. Unfortunately there has been much less work on dependently typed calculi for object-oriented programming. This is partly because it is widely acknowledged that the combination between dependent types and subtyping is particularly challenging.
This paper presents λ I≤, which is a dependently typed generalization of System F≤. The resulting calculus follows the style of Pure Type Systems, and contains a single unified syntactic sort that accounts for expressions, types and kinds. To address the challenges posed by the combination of dependent types and subtyping, λ I≤ employs a novel technique that unifies typing and subtyping. In λ I≤ there is only a judgement that is akin to a typed version of subtyping. Both the typing relation, as well as type well-formedness are just special cases of the subtyping relation. The resulting calculus has a rich metatheory and enjoys of several standard and desirable properties, such as subject reduction, transitivity of subtyping, narrowing as well as standard substitution lemmas. All the metatheory of λ I≤ is mechanically proved in the Coq theorem prover. Furthermore, (and as far as we are aware) λ I≤ is the first dependently typed calculus that completely subsumes System F≤, while preserving various desirable properties.
Supplemental Material
Available for Download
- Andreas Abel and Dulma Rodriguez. 2008. Syntactic metatheory of higher-order subtyping. In CSL ’08. 446–460. Google Scholar
Digital Library
- Beniamino Accattoli and Giulio Guerrieri. 2016. Open Call-by-Value. In APLAS ’16. Springer, 206–226. Google ScholarCross Ref
- Thorsten Altenkirch, Nils Anders Danielsson, Andres Löh, and Nicolas Oury. 2010. ΠΣ: Dependent types without the sugar. In Functional and Logic Programming. Springer, 40–55. Google ScholarDigital Library
- 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. Springer, 249–272. Google ScholarCross Ref
- Nada Amin, Adriaan Moors, and Martin Odersky. 2012. Dependent object types. In FOOL ’12. ACM.Google Scholar
- Nada Amin, Tiark Rompf, and Martin Odersky. 2014. Foundations of path-dependent types. In OOPSLA ’14. ACM, 233–249. Google ScholarDigital Library
- David Aspinall and Adriana Compagnoni. 1996. Subtyping dependent types. In LICS ’96. 86–97. Google ScholarCross Ref
- Lennart Augustsson. 1998. Cayenne — a Language with Dependent Types. In ICFP ’98. ACM, 239–250.Google Scholar
- Henk Barendregt. 1991. Introduction to generalized type systems. Journal of Functional Programming 1, 2 (1991), 125–154.Google ScholarCross Ref
- Henk Barendregt. 1992. Lambda Calculi with Types. In Handbook of Logic in Computer Science, Vol. 2. 117–309.Google Scholar
- 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
- Kim B. Bruce, Luca Cardelli, and Benjamin C. Pierce. 1999. Comparing object encodings. Information and Computation 155, 1-2 (1999), 108–133.Google ScholarDigital Library
- Joana Campos and Vasco T. Vasconcelos. 2015. Imperative objects with dependent types. In FTfJP ’15. ACM, 2:1–2:6. Google ScholarDigital Library
- Luca Cardelli. 1986a. Amber. In Combinators and Functional Programming Languages. Springer Berlin Heidelberg, 21–47.Google Scholar
- Luca Cardelli. 1986b. A Polymorphic lambda-calculus with Type: Type. Digital Systems Research Center.Google Scholar
- Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov. 1994. An extension of system F with subtyping. Information and Computation 109, 1-2 (1994), 4–56.Google ScholarDigital Library
- Luca Cardelli and Peter Wegner. 1985. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys (CSUR) 17, 4 (1985), 471–523. Google ScholarDigital Library
- Chris Casinghino, Vilhelm Sjöberg, and Stephanie Weirich. 2014. Combining Proofs and Programs in a Dependently Typed Language. In POPL ’14. ACM, 33–45. Google ScholarDigital Library
- Giuseppe Castagna and Gang Chen. 2001. Dependent types with subtyping and late-bound overloading. Information and Computation 168, 1 (2001), 1–67. Google ScholarDigital Library
- Gang Chen. 1997. Subtyping calculus of construction. Mathematical Foundations of Computer Science 1997 (1997), 189–198.Google Scholar
- Gang Chen. 1998. Dependent type system with subtyping (I) type level transitivity elimination. Journal of Computer Science and Technology 13, 6 (1998), 564–578. Google ScholarCross Ref
- Gang Chen. 2003. Coercive Subtyping for the Calculus of Constructions. In POPL ’03. ACM, 150–159. Google ScholarDigital Library
- Adriana Compagnoni and Healfdene Goguen. 2003. Typed operational semantics for higher-order subtyping. Information and Computation 184, 2 (2003), 242–297. Google ScholarDigital Library
- Adriana Beatriz Compagnoni. 1995. Higher-order subtyping with intersection types. Ph.D. Dissertation. University of Nijmegen.Google Scholar
- Thierry Coquand and Gérard Huet. 1988. The Calculus of Constructions. Information and Computation 76 (1988), 95–120. Google ScholarDigital Library
- Karl Crary, Robert Harper, and Sidd Puri. 1999. What is a recursive module?. In PLDI ’99. ACM, 50–63. Google ScholarDigital Library
- Pierre-Louis Curien and Giorgio Ghelli. 1992. Coherence of subsumption, minimum typing and type-checking in F ≤. Mathematical structures in computer science 2, 01 (1992), 55–91. Google ScholarCross Ref
- Jean-Yves Girard. 1972. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph.D. Dissertation. Université Paris VII.Google Scholar
- Robert Harper. 2013. Practical foundations for programming languages (1st ed.). Cambridge University Press.Google Scholar
- DeLesley S. Hutchins. 2010. Pure Subtype Systems. In POPL ’10. ACM, 287–298.Google Scholar
- Jonas Kaiser, Tobias Tebbi, and Gert Smolka. 2017. Equivalence of System F and λ2 in Coq Based on Context Morphism Lemmas. In CPP ’17. ACM, 222–234. Google ScholarDigital Library
- Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, and Ki Yung Ahn. 2012. Equational Reasoning about Programs with General Recursion and Call-by-value Semantics. In PLPV ’12. 15–26. Google ScholarDigital Library
- Adriaan Moors, Frank Piessens, and Martin Odersky. 2008. Generics of a Higher Kind. In OOPSLA ’08. ACM, 423–438. Google ScholarDigital Library
- Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Chalmers University of Technology.Google Scholar
- Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth, Stéphane Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger. 2004. An Overview of the Scala Programming Language. Technical Report IC/2004/64. EPFL Lausanne, Switzerland.Google Scholar
- Martin Odersky, Vincent Cremet, Christine Röckl, and Matthias Zenger. 2003. A nominal theory of objects with dependent types. In ECOOP ’03. Springer, 201–224. Google ScholarCross Ref
- Luca Paolini and Simona Ronchi Della Rocca. 1999. Call-by-value Solvability. RAIRO-Theoretical Informatics and Applications 33, 6 (1999), 507–534. Google ScholarCross Ref
- Benjamin C. Pierce. 1992. Bounded quantification is undecidable. In POPL ’92. ACM, 305–315. Google ScholarDigital Library
- Benjamin C. Pierce. 2002. Types and programming languages. MIT press.Google ScholarDigital Library
- Benjamin C. Pierce and Martin Steffen. 1997. Higher-order subtyping. Theoretical computer science 176, 1 (1997), 235–282. Google ScholarDigital Library
- Benjamin C. Pierce and David N. Turner. 1994. Simple type-theoretic foundations for object-oriented programming. Journal of functional programming 4, 02 (1994), 207–247. Google ScholarCross Ref
- Benjamin C. Pierce and David N. Turner. 2000. Local type inference. ACM Transactions on Programming Languages and Systems (TOPLAS) 22, 1 (2000), 1–44. Google ScholarDigital Library
- Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). In OOPSLA ’16. ACM, 624–641. Google ScholarDigital Library
- David A. Schmidt. 1994. The Structure of Typed Programming Languages. MIT Press.Google Scholar
- Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, et al. 2010. Ott: Effective tool support for the working semanticist. Journal of functional programming 20, 1 (2010), 71–122. Google ScholarDigital Library
- Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, and Stephanie Weirich. 2012. Irrelevance, Heterogenous Equality, and Call-by-value Dependent Type Systems. In MSFP ’12. 112–162.Google Scholar
- Vilhelm Sjöberg and Stephanie Weirich. 2015. Programming Up to Congruence. In POPL ’15. ACM, 369–382. Google ScholarDigital Library
- Martin Steffen. 1998. Polarized Higher-Order Subtyping. Ph.D. Dissertation. Technische Fakultät, Friedrich-Alexander-Universität Erlangen-Nürnberg.Google Scholar
- Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, and Timothy Simpson. 2008. Verified Programming in Guru. In PLPV ’09. 49–58. Google ScholarDigital Library
- The Coq development team. 2016. The Coq proof assistant reference manual. https://coq.inria.fr/refman/ Version 8.6.Google Scholar
- Floris van Doorn, Herman Geuvers, and Freek Wiedijk. 2013. Explicit Convertibility Proofs in Pure Type Systems. In LFMTP ’13. ACM, 25–36. Google ScholarDigital Library
- Stephanie Weirich, Justin Hsu, and Richard A. Eisenberg. 2013. System FC with Explicit Kind Equality. In ICFP ’13. ACM, 275–286. Google ScholarDigital Library
- Andrew K. Wright and Matthias Felleisen. 1994. A syntactic approach to type soundness. Information and computation 115, 1 (1994), 38–94. Google ScholarDigital Library
- Hongwei Xi and Frank Pfenning. 1999. Dependent types in practical programming. In POPL ’99. ACM, 214–227. Google ScholarDigital Library
- Yanpeng Yang, Xuan Bi, and Bruno C. d. S. Oliveira. 2016. Unified Syntax with Iso-types. In APLAS ’16. Springer, 251–270. Google ScholarCross Ref
- Yanpeng Yang and Bruno C. d. S. Oliveira. 2017. Unifying Typing and Subtyping (Extended version). Available from https://bitbucket.org/ypyang/oopsla17 . (2017).Google Scholar
- Jan Zwanenburg. 1999. Pure type systems with subtyping. In TLCA ’99. 381–396. Google ScholarCross Ref
Index Terms
- Unifying typing and subtyping
Recommendations
Label dependent lambda calculus and gradual typing
Dependently-typed programming languages are gaining importance, because they can guarantee a wide range of properties at compile time. Their use in practice is often hampered because programmers have to provide very precise types. Gradual typing is a ...
Subtyping dependent types
The need for subtyping in type systems with dependent types has been realized for some years. But it is hard to prove that systems combining the two features have fundamental properties such as subject reduction. Here we investigate a subtyping ...
Coinductive Axiomatization of Recursive Type Equality and Subtyping
We present new sound and complete axiomatizations of type equality and subtype inequality for a first-order type language with regular recursive types. The rules are motivated by coinductive characterizations of type containment and type equality via ...
Comments