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

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 :
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download

Contributor : Didier Rémy Connect in order to contact the contributor
Submitted on : Monday, December 12, 2011 - 2:14:37 PM
Last modification on : Friday, February 4, 2022 - 3:08:10 AM
Long-term archiving on: : Sunday, December 4, 2016 - 2:46:00 PM


Files produced by the author(s)


  • HAL Id : inria-00582570, version 3



Julien Cretin, Didier Rémy. On the Power of Coercion Abstraction. [Research Report] RR-7587, INRIA. 2011, pp.59. ⟨inria-00582570v3⟩



Record views


Files downloads