Computer Science Department
School of Computer Science, Carnegie Mellon University


Implementing the TILT Internal Language

Leaf Petersen, Perry Cheng, Robert Harper, Chris Stone

December 2000

Keywords: Singleton kinds, typed compilation, intensional polymorphism, type theory

The TILT compiler for Standard ML represents programs internally using a predicative lambda calculus based on Girard's Fw kind level, this language is notable for containing singleton kinds and dependent product and function kinds. Previous work (CMU-CS-99-155) established the decidability of type equivalence for this language.

This paper presents a typechecking algorithm for the full TILT internal language and discusses some of the more interesting features of the language. The particular use of intensional type analysis to handle arrays of unboxed floating point numbers is described. An extended calculus is also introduced which permits unlabelled singletons at higher kind, in order to allow for more compact program representation. The extended calculus is related to the restricted calculus via a transformation that eliminates the unlabelled singletons, and the decidability of the typechecking algorithms for both the original and extended calculus is shown.

47 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by