Abstract
We introduce Erasure Pure Type Systems, an extension to Pure Type Systems with an erasure semantics centered around a type constructor ∀ indicating parametric polymorphism. The erasure phase is guided by lightweight program annotations. The typing rules guarantee that well-typed programs obey a phase distinction between erasable (compile-time) and non-erasable (run-time) terms.
The erasability of an expression depends only on how its value is used in the rest of the program. Despite this simple observation, most languages treat erasability as an intrinsic property of expressions, leading to code duplication problems. Our approach overcomes this deficiency by treating erasability extrinsically.
Because the execution model of EPTS generalizes the familiar notions of type erasure and parametric polymorphism, we believe functional programmers will find it quite natural to program in such a setting.
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
The Coq proof assistant, http://coq.inria.fr
Abadi, M., Cardelli, L., Curien, P.-L.: Formal parametric polymorphism. Theoretical Computer Science 121(1–2), 9–58 (1993)
Augustsson, L.: Cayenne – A language with dependent types. In: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, pp. 239–250 (1998)
Barendregt, H.P.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 2, Oxford University Press, Oxford (1992)
Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 460–475. Springer, Heidelberg (2006)
Brady, E.: Practical Implementation of a Dependently Typed Functional Programming Language. PhD thesis, University of Durham (2005)
Chen, C., Xi, H.: Combining programming with theorem proving. In: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, pp. 66–77 (2005)
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proceedings of the 33rd ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 42–54 (2006)
Lin, C., McCreight, A., Shao, Z., Chen, Y., Guo, Y.: Foundational typed assembly language with certified garbage collection. In: First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, pp. 326–338. IEEE Computer Society Press, Los Alamitos (2007)
Luo, Z.: Computation and reasoning: A type theory for computer science. Oxford University Press, New York, USA (1994)
Mairson, H.G.: Outline of a proof theory of parametricity. In: Hughes, J. (ed.) FPCA 1991. LNCS, vol. 523, pp. 313–327. Springer, Heidelberg (1991)
McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming 14(1), 69–111 (2004)
Miquel, A.: The implicit calculus of constructions. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 344–359. Springer, Heidelberg (2001)
Miquel, A.: Le Calcul des Constructions Implicite: Syntaxe et Sémantique. PhD thesis, Université Paris 7 (2001)
Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 106–119 (1997)
Peyton-Jones, S., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. In: Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (2006)
Pfenning, F.: Intensionality, extensionality, and proof irrelevance in modal type theory. In: LICS 2001: Proceedings of the 16th Annual Symposium on Logic in Computer Science, pp. 221–230. IEEE Computer Society Press, Los Alamitos (2001)
Plotkin, G.D., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 361–375. Springer, Heidelberg (1993)
Sheard, T.: Languages of the future. In: Proceedings of the Nineteenth ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA Companion Volume, pp. 116–119 (2004)
Sheard, T., Pašalić, E.: Meta-programming with built-in type equality. In: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages (LFM 2004), pp. 106–124 (2004), http://cs-www.cs.yale.edu/homes/carsten/lfm04/
Wadler, P.: Theorems for free! In: Functional Programming Languages and Computer Architecture, pp. 347–359. ACM Press, New York (1989)
Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN Symposium on Principles of Programming Languages, pp. 214–227 (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mishra-Linger, N., Sheard, T. (2008). Erasure and Polymorphism in Pure Type Systems. In: Amadio, R. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2008. Lecture Notes in Computer Science, vol 4962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78499-9_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-78499-9_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78497-5
Online ISBN: 978-3-540-78499-9
eBook Packages: Computer ScienceComputer Science (R0)