On the power of coercion abstraction
Abstract
Erasable 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 subtyping of known types and some displacement of quantifiers, but not subtyping assumptions nor certain forms of delayed type instantiation. We generalize F-eta by allowing abstraction over retyping functions. We follow a general approach where computing with coercions can be seen as computing in the lambda-calculus but keeping track of which parts of terms are coercions. We obtain a language where coercions do not contribute to the reduction but may block it and are thus not erasable. We recover erasable coercions by choosing a weak reduction strategy and restricting coercion abstraction to value-forms or by restricting abstraction to coercions that are polymorphic in their domain or codomain. The latter variant subsumes F-eta, F-sub, and MLF in a unified framework.
Supplementary Material
References
[1]
P. Baldan, G. Ghelli, and A. Raffaetà. Basic theory of F-bounded quantification. Inf. Comput., 153:173--237, September 1999. URL http://portal.acm.org/citation.cfm?id=320278.320285.
[2]
V. Breazu-Tannen, T. Coquand, C. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172--221, 1991.
[3]
P. Canning, W. Cook, W. Hill, W. Olthoff, and J. C. Mitchell. F-bounded polymorphism for object-oriented programming. In FPCA, 1989. URL http://doi.acm.org/10.1145/99370.99392.
[4]
L. Cardelli. An implementation of FSub. Research Report 97, Digital Equipment Corporation Systems Research Center, 1993. URL http://research.microsoft.com/Users/luca/Papers/SRC-097.pdf.
[5]
K. Crary. Typed compilation of inclusive subtyping. In ICFP, 2000. URL http://doi.acm.org/10.1145/351240.351247.
[6]
K. Crary, S. Weirich, and J. G. Morrisett. Intensional polymorphism in typeerasure semantics. Journal of Functional Programming, 12(6):567--600, 2002. URL http://dx.doi.org/10.1017/S0956796801004282.
[7]
D. Le Botlan and D. Rémy. Recasting MLF. Information and Computation, 207(6), 2009. URL http://dx.doi.org/10.1016/j.ic.2008.12.006.
[8]
D. Leijen. A type directed translation of MLF to System F. In ICFP, Oct. 2007. URL http://research.microsoft.com/users/daan/download/papers/mlftof.pdf.
[9]
D. Leijen and A. Löh. Qualified types for MLF. In ICFP, Sept. 2005. URL http://murl.microsoft.com/users/daan/download/papers/qmlf.pdf.
[10]
S. Lenglet and J. B. Wells. Expansion for forall-quantifiers. Available electronically, 2010. URL http://sardes.inrialpes.fr/~slenglet/papers/systemFs.pdf.
[11]
G. Manzonetto and P. Tranquilli. Harnessing MLF with the Power of System F. In MFCS, volume 6281, 2010.
[12]
J. C. Mitchell. Polymorphic type inference and containment. Information and Computation, 2/3(76), 1988.
[13]
D. Rémy and B. Yakobowski. A Church-Style Intermediate Language for MLF. In FLOPS, volume 6009, pages 24--39. 2010. URL http://dx.doi.org/10.1007/978-3-642-12251-4_4.
[14]
D. Vytiniotis and S. P. Jones. Practical aspects of evidence-based compilation in system FC. Available electronically, 2011. URL http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/.
[15]
S. Weirich, D. Vytiniotis, S. Peyton Jones, and S. Zdancewic. Generative type abstraction and type-level computation. In POPL, 2011. URL http://doi.acm.org/10.1145/1926385.1926411.
Index Terms
- On the power of coercion abstraction
Recommendations
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 ...
A church-style intermediate language for MLF
MLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System-F explicit first-class polymorphism. We present xMLF, a Church-style version of MLF with full type information that can easily be maintained during ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2012602 pages
Copyright © 2012 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 25 January 2012
Published in SIGPLAN Volume 47, Issue 1
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations9Total Citations
- 370Total Downloads
- Downloads (Last 12 months)5
- Downloads (Last 6 weeks)0
Reflects downloads up to 08 Feb 2025
Other Metrics
Citations
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