While there is a rich theory of universal/existential quantifiers, there are two important difficulties in practice. (1) Systems with these quantifiers generally do not have a strong principality property, i.e., there is no most general analysis for each program fragment. This makes it difficult to perform type analysis compositionally (i.e., where program fragments are analyzed independently) and sometimes even makes type analysis impossible. (2) These quantifiers hide information, making it hard to extend type analysis to flow analysis and to perform type/flow-directed program transformations.
To address these difficulties, I have designed type systems which support type polymorphism with intersection and union types instead of universal/existential types. In collaboration with my colleagues in the Church Project, I have developed analysis and transformation algorithms using these systems. Overcoming difficulty (1), we have used intersection type systems with strong principality properties to develop new type analysis algorithms which are compositional and also accept many safe programs rejected as ill-typed by earlier algorithms. Overcoming difficulty (2), we have shown how to use a system with intersection/union types to express polyvariant flow analyses and to guide a new style of program transformation and optimization: type/flow-directed compilation. This new technology is the foundation for an experimental compiler we are developing. I will discuss how our new approach to compilation will contribute to efficient, reliable, and modular compilation.