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
[Research Report] RR-7587, INRIA. 2011, pp.59
Liste complète des métadonnées

https://hal.inria.fr/inria-00582570
Contributor : Didier Rémy <>
Submitted on : Monday, December 12, 2011 - 2:14:37 PM
Last modification on : Saturday, September 17, 2016 - 1:37:29 AM
Document(s) archivé(s) le : 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

249

Document downloads

155