Fully reflexive intensional type analysis

Compilers for polymorphic languages can use runtime type inspection to supp ort advanced implementation techniques such as tagless garbage collection, polymorphic marshalling, and flattened data structures. Intensional type an alysis is a type-theoretic framework for expressing and certifying such typ e-analyzing computations. 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 persistence, or marshalling which must be able to examine the t ype of any runtime value. We present a typed intermediate language that supports fully reflexive inte nsional type analysis. By fully reflexive, we mean that type-analyzing oper ations are applicable to the type of any runtime value in the language. In particular, we provide both type-level and term-level constructs for analyz ing quantified types. Our system supports structural induction on quantifie d types yet type checking remains decidable. We show how to use reflexive t ype analysis to support type-safe marshalling and how to generate certified type-analyzing object code.