Computer Science Department
School of Computer Science, Carnegie Mellon University
Singleton Kinds and Singleton Types
Christopher Allan Stone
However, the decidability of typechecking in the presence of singletons is not obvious. In order to typecheck a term, one must be able to determine whether two type constructors are provably equivalent. But in the presence of singleton kinds, the equivalence of type constructors depends both on the typing context in which they are compared and on the kind at which they are compared.
In this dissertation I present MIL-0, a lambda calculus with singletons that is based upon the representation used by the TILT compiler. I prove important properties of this language, including type soundness and decidability of typechecking. The main technical result is decidability of equivalence for well-formed type constructors. Inspired by Coquand's result for type theory, I prove decidability of constructor equivalence for MIL-0 by exhibiting a novel -- though slightly inefficient -- type-directed comparison algorithm. The correctness of this algorithm is proved using an interesting variant of Kripke-style logical relations: unary relations are indexed by a single possible world (in our case, a typing context), but binary relations are indexed by two worlds. Using this result I can then show the correctness of a natural, practical algorithm used by the TILT compiler.