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
Reports

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

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/inria-00582570
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

File

RR-7587.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00582570, version 3

Collections

Citation

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

Share

Metrics

Record views

218

Files downloads

368