Wizard of TILT: Efficient, Convenient, and Abstract Type Representations

摘要

TILT is a certifying compiler for Standard ML. Its major distinguishing feature is the use of Typed Intermediate Languages throughout the phases of compilation. Because each of the code transformations that the compiler performs also transforms the types, we preserve type information that is normally discarded after typechecking the source language in traditional compilers. This allows us to typecheck the results of these transformations (catching compiler bugs), perform data representation optimizations, and do nearly tag-free garbage collection. We eventually intend for TILT to generate proof-carrying code. Unfortunately, storing and processing types at compile- time imposes a performance penalty on the compiler. With type-checking enabled after each transformation and optimization, TILT is slow. This paper recounts our experience in attempting to implement a more e cient type representation strategy into the substantial existing code base. Though the abstraction and optimizations are successful, in the end we are overwhelmed by the overhead necessary to implement them.