On the Power of Coercion Abstraction - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Reports (Research Report) Year : 2011

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.
Les coercions effaçables dans le Système F-eta, aussi connues sous le nom de fonctions de retypage, sont des eta-expansions de l'identité. Elles peuvent changer le type des termes sans en changer leur comportement et peuvent donc être effacées avant la réduction. Les coercions de F-eta peuvent modéliser le sous-typage entre types connus ou le déplacement de quantificateurs, mais elles ne permettent pas certaines formes d'instanciation retardée ni de raisonner sous des hypothèses de sous-typage. Nous généralisons F-eta en introduisant l'abstraction des fonctions de retypage. Nous suivons une approche générale où le calcul avec des coercions peut être vu comme une réduction dans le lambda-calcul gardant trace de la partie des termes qui sont des coercions. Nous obtenons un langage où les coercions ne contribuent pas au calcul, mais peuvent le bloquer et ne sont donc pas effaçables. Nous retrouvons des coercions effaçables en choisissant une stratégie de réduction faible et en restreignant l'abstraction de coercions aux valeurs ou bien en restreignant l'abstraction aux coercions qui sont polymorphes en leur domaine ou en leur codomaine. Cette seconde variante généralise F-eta, MLF et F-sub dans un cadre unifié.
Fichier principal
Vignette du fichier
RR-7587.pdf (813.56 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00582570 , version 1 (04-04-2011)
inria-00582570 , version 2 (13-07-2011)
inria-00582570 , version 3 (12-12-2011)

Identifiers

  • HAL Id : inria-00582570 , version 3

Cite

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

Share

Gmail Facebook X LinkedIn More