The TIL compiler pioneered the idea of using typed intermediate languages for compilation. Instead of using standard syntax directed transformations, compilation in TIL proceeds via a series of type directed transformations mapping well-typed terms to well-typed terms. The compiler can use the type information and the invariants imposed by the type system to assist with optimization and verification. The TIL-Two (TILT) compiler extended this work to the full Standard ML '98 language including the module system. This extension required the use of significantly more powerful and complex intermediate languages.
This talk will focus on one of the intermediate languages used in TILT, called the MIL (Middle Intermediate Language). The MIL is a predicative lambda calculus with dependent kinds that serves as the main intermediate form for TILT. The MIL was designed to address both the theoretical requirements for serving as the target of the translation from SML '98 and the practical requirements imposed by the implementation. In this talk, I will first present a restricted mini-MIL calculus which contains the core constructs of the MIL. This restricted calculus is powerful enough to express the structural sharing of the module language, but suffers from some practical problems - most notably the inability to express some types compactly. To address this, I will present an extended mini-MIL calculus that solves the compactness problem of the restricted calculus by allowing undecorated singleton types at higher kinds - essentially introducing an element of type inference into type-checking. The extended calculus is related to the restricted calculus via a transformation that eliminates the undecorated singletons.