Compiling Polymorphism Using Intensional Type Analysis
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
Types have been used to describe the size and shape of data structures at compile time. In polymorphic languages or languages with abstract types, this is not possible since the types of some objects are not known at compile time. Consequently, most implementations of polymorphic languages box data i.e., represent an object as a pointer, leading to inefficiencies. We introduce a new compilation method for polymorphic languages that avoids the problems associated with boxing data. The fundamental idea is to relax the requirement that code selection for primitive, polymorphic operations, such as pairing and projection, must be performed at compile time. Instead, we allow such operations to defer code selection until link- or even run-time when the types of the values are known. We formalize our approach as a translation into an explicitly-typed, predicative polymorphic delta-calculus with intensional polymorphism. By intensional polymorphism, we mean that constructors and terms can be constructed via structural recursion on types. The form of intensional analysis that we provide is sufficiently strong to perform non-trivial type- based code selection, but it is sufficiently weak that termination of operations that analyze types is assured.
- Computer Programming and Software