HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Contributor : Didier Rémy Connect in order to contact the contributor
Submitted on : Monday, December 12, 2011 - 2:30:45 PM
Last modification on : Friday, February 4, 2022 - 3:10:17 AM

Links full text




Julien Cretin, Didier Rémy. On the Power of Coercion Abstraction. POPL 2012: 39th ACM SIGPLAN-SIGACT Symposium on Principle Of Programming Languages, ACM, Jan 2012, Philadelphia, United States. ⟨10.1145/2103656.2103699⟩. ⟨hal-00650910⟩



Record views