Abstract
While generalized algebraic datatypes (GADTs) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean for a GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subtyping relation that raise interesting design questions. We allow variance annotations in GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subtyping such as OCaml, or to languages with general subtyping constraints.
Part of this work has been done at IRILL.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abel, A.: Polarized subtyping for sized types. Mathematical Structures in Computer Science (2006); Goguen, H., Compagnoni, A. (eds.) Special issue on subtyping
Emir, B., Kennedy, A., Russo, C.V., Yu, D.: Variance and Generalized Constraints for C# Generics. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 279–303. Springer, Heidelberg (2006)
Garrigue, J.: Relaxing the Value Restriction. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004. LNCS, vol. 2998, pp. 196–213. Springer, Heidelberg (2004)
Kennedy, A., Russo, C.V.: Generalized algebraic data types and object-oriented programming. In: Proceedings of the 20th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (2005), http://research.microsoft.com/pubs/64040/gadtoop.pdf
Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: Proceedings of the 16th IEEE Symposium on Logic in Computer Science, LICS 2001, June 16-19. Boston University, USA (2001)
Simonet, V., Pottier, F.: A constraint-based approach to guarded algebraic data types. ACM Transactions on Programming Languages and Systems 29(1) (January 2007)
Scherer, G., Rémy, D.: GADTs meet subtyping. Long version, available electronically, http://gallium.inria.fr/~remy/gadts/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Scherer, G., Rémy, D. (2013). GADTs Meet Subtyping. In: Felleisen, M., Gardner, P. (eds) Programming Languages and Systems. ESOP 2013. Lecture Notes in Computer Science, vol 7792. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37036-6_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-37036-6_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37035-9
Online ISBN: 978-3-642-37036-6
eBook Packages: Computer ScienceComputer Science (R0)