Compiling Polymorphism Using Intensional Type Analysis

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 - calculus with intensional polymorphism. By "intensional polymorphism", we mean that constructors and terms can be ..