Name
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1145/2103656.2103699 | POPL |
Keywords | Field | DocType |
subtyping assumption,weak reduction strategy,coercion abstraction,delayed type instantiation,system f-eta,certain form,known type,general approach,erasable coercion,retyping function,system f,polymorphism,coercion,lambda calculus,conversion,type,subtyping,bounded polymorphism | Reduction strategy,Programming language,Codomain,Abstraction,Computer science,System F,Bounded quantification,Theoretical computer science,Subtyping | Conference |
Volume | Issue | ISSN |
47 | 1 | 0362-1340 |
Citations | PageRank | References |
4 | 0.47 | 8 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Julien Cretin | 1 | 87 | 3.76 |
| Didier Rémy | 2 | 682 | 49.82 |