Erasure and Polymorphism in Pure Type Systems

8 years 11 months ago
Erasure and Polymorphism in Pure Type Systems
We introduce Erasure Pure Type Systems, an extension to Pure Type Systems with an erasure semantics centered around a type constructor indicating parametric polymorphism. The erasure phase is guided by lightweight program annotations. The typing rules guarantee that well-typed programs obey a phase distinction between erasable (compile-time) and non-erasable (run-time) terms. The erasability of an expression depends only on how its value is used in the rest of the program. Despite this simple observation, most languages treat erasability as an intrinsic property of expressions, leading to code duplication problems. Our approach overcomes this deficiency by treating erasability extrinsically. Because the execution model of EPTS generalizes the familiar notions of type erasure and parametric polymorphism, we believe functional programmers will find it quite natural to program in such a setting. 1 Background and Motivation Statically typed programming languages have evolved ever more exp...
Nathan Mishra-Linger, Tim Sheard
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Authors Nathan Mishra-Linger, Tim Sheard
Comments (0)