Abstract
Subtyping of Bounded Polymorphism has long been known to be undecidable when coupled with contra-variance. While decidable forms of bounded polymorphism exist, they all sacrifice either useful properties such as contra-variance (Kernel F\(_{<:}\)), or useful metatheoretic properties (F\(_{<:}^\top \)). In this paper we show how, by syntactically separating contra-variance from the recursive aspects of subtyping in System F\(_{<:}\), decidable subtyping can be ensured while also allowing for both contra-variant subtyping of certain instances of bounded polymorphism, and many of System F\(_{<:}\)’s desirable metatheoretic properties. We then show that this approach can be applied to the related polymorphism present in D\(_{<:}\), a minimal calculus that models core features of the Scala type system.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Syntactically restricting bounded polymorphism for decidable subtyping. Technical report (2020). https://doi.org/10.5281/zenodo.4039832
Amin, N., Moors, A., Odersky, M.: Dependent object types. In: 19th International Workshop on Foundations of Object-Oriented Languages (2012)
Amin, N., Rompf, T., Odersky, M.: Foundations of path-dependent types. In: Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2014 (2014)
Cardelli, L., Martini, S., Mitchell, J.C., Scedrov, A.: An extension of system F with subtyping. In: Ito, T., Meyer, A.R. (eds.) Theor. Aspects Comput. Softw., pp. 750–770. Springer, Berlin Heidelberg, Berlin, Heidelberg (1991)
Castagna, G., Pierce, B.C.: Decidable bounded quantification. In: Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1994 (1994)
Castagna, G., Pierce, B.C.: Corrigendum: decidable bounded quantification. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1995 (1995)
Greenman, B., Muehlboeck, F., Tate, R.: Getting F-bounded polymorphism into shape. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014 (2014)
Grigore, R.: Java generics are turing complete. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 (2017)
Hu, J.Z.S., Lhoták, O.: Undecidability of D\(<\): and its decidable fragments. In: Proceedings of the ACM on Programming Languages (POPL) (2019)
Mackay, J., Potanin, A., Aldrich, J., Groves, L.: Decidable subtyping for path dependent types. In: Proceedings of the ACM on Programming Languages (POPL) (2019)
Nistor, L., Kurilova, D., Balzer, S., Chung, B., Potanin, A., Aldrich, J.: Wyvern: a simple, typed, and pure object-oriented language. In: Proceedings of the 5th Workshop on MechAnisms for SPEcialization, Generalization and inHerItance. MASPEGHI 2013 (2013)
Omar, C., Kurilova, D., Nistor, L., Chung, B., Potanin, A., Aldrich, J.: Safely composable type-specific languages. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 105–130. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44202-9_5
Pierce, B.C.: Bounded quantification is undecidable. In: Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1992 (1992)
Pierce, B.C.: Types and Programming Languages. The MIT Press, Massachusetts (2002)
Rapoport, M., Kabir, I., He, P., Lhoták, O.: A simple soundness proof for dependent object types. In: Proceedings of the ACM on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) (2017)
Rompf, T., Amin, N.: 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 (2016)
Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1989 (1989)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Mackay, J., Potanin, A., Aldrich, J., Groves, L. (2020). Syntactically Restricting Bounded Polymorphism for Decidable Subtyping. In: Oliveira, B.C.d.S. (eds) Programming Languages and Systems. APLAS 2020. Lecture Notes in Computer Science(), vol 12470. Springer, Cham. https://doi.org/10.1007/978-3-030-64437-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-64437-6_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-64436-9
Online ISBN: 978-3-030-64437-6
eBook Packages: Computer ScienceComputer Science (R0)