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...

• Type: Conference
• Year: 2008
• Where: FOSSACS
• Authors: Nathan Mishra-Linger, Tim Sheard
• Keywords: Erasure, FOSSACS 2008, Parametric Polymorphism, Pure Type Systems, Software Engineering