Fully Reflexive Intensional Type Analysis
Last modified: Thu Oct 4 02:41:42 2001 GMT.
AbstractCompilers for polymorphic languages can use runtime 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 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.
PublishedIn Proc. 2000 ACM SIGPLAN International Conference on Functional Programming (ICFP'00), Montreal, Canada, pages 82-93, September 2000. ©2000 ACM.
Copyright © 1996-2022 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science