Fully reflexive intensional type analysis

Compilers for polymorphic languages can use runtime type in-spection to support advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data structures. Intensional type analysis is a type-theoretic frame-work for expressing and certifying such type-analyzing computa-tions. Unfortunately, existing approaches to intensional analysis do not work well on types with universal, existential, or fixpoint quantifiers. This makes it impossible to code applications such as garbage collection, persistency, or marshalling which must be able to examine the type of any runtime value. We present a typed intermediate language that supports fully reflexive intensional type analysis. By fully reflexive, we mean that type-analyzing operations are applicable to the type of any runtime value in the language. 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 show how to use reflexive type analysis to support type-safe marshalling and how to generate certified type-analyzing object code