Compilers for polymorphic languages can use run-time type inspection to support
advanced implementation techniques such as tagless garbage collection,
polymorphic marshalling, and flattened data structures. Intensional type
analysis is a type-theoretic framework for expressing and certifying such
type-analyzing computations. Unfortunately, existing approaches to
intensional analysis do not work well on quantified types such as existential
or polymorphic types. This makes it impossible to code (in a type-safe
language) applications such as garbage collection, persistency, or marshalling
which must be able to examine the type of any run-time value.
We present a typed intermediate language that supports the analysis
of quantified types. In particular, we provide both type-level and
term-level constructs for analyzing quantified types. Our system
supports structural induction on quantified types
yet type checking remains decidable. We also show that our system
is compatible with a type-erasure semantics.
To appear in ACM Transactions on Programming Languages
and Systems (TOPLAS)
, 51 pages, 2002.