On the Power of Coercion Abstraction

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

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00582570
Contributeur : Didier Rémy <>
Soumis le : lundi 12 décembre 2011 - 14:14:37
Dernière modification le : samedi 17 septembre 2016 - 01:37:29
Document(s) archivé(s) le : dimanche 4 décembre 2016 - 14:46:00

Fichier

RR-7587.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de
la notice

281

Téléchargements du document

172