Implementing typed intermediate languages

Recent advances in compiler technology have demonstrated the benefits of us ing strongly typed intermediate languages to compile richly typed source la nguages (e.g., ML). A type-preserving compiler can use types to guide advan ced optimizations and to help generate provably secure mobile code. Types, unfortunately, are very hard to represent and manipulate efficiently; a nai ve implementation can easily add exponential overhead to the compilation an d execution of a program. This paper describes our experience with implemen ting the FLINT typed intermediate language in the SML/NJ production compile r. We observe that a type-preserving compiler will not scale to handle larg e types unless all of its type-preserving stages preserve the asymptotic ti me and space usage in representing and manipulating types. We present a ser ies of novel techniques for achieving this property and give empirical evid ence of their effectiveness.