Intensional Polymorphism in Type-Erasure Semantics

Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and flattened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks; it requires duplication of constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion. We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover a...

• Type: Conference
• Year: 1998
• Where: ICFP
• Authors: Karl Crary, Stephanie Weirich, J. Gregory Morrisett
• Keywords: Closure Conversion, ICFP 1998, Intensional Polymorphism, Programming Languages, Run Time