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.
Type de document :
Communication dans un congrès
POPL 2012: 39th ACM SIGPLAN-SIGACT Symposium on Principle Of Programming Languages, Jan 2012, Philadelphia, United States. ACM, 2012, Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. <10.1145/2103656.2103699>
Liste complète des métadonnées

https://hal.inria.fr/hal-00650910
Contributeur : Didier Rémy <>
Soumis le : lundi 12 décembre 2011 - 14:30:45
Dernière modification le : jeudi 8 octobre 2015 - 01:03:58

Identifiants

Collections

Citation

Julien Cretin, Didier Rémy. On the Power of Coercion Abstraction. POPL 2012: 39th ACM SIGPLAN-SIGACT Symposium on Principle Of Programming Languages, Jan 2012, Philadelphia, United States. ACM, 2012, Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. <10.1145/2103656.2103699>. <hal-00650910>

Partager

Métriques

Consultations de la notice

104