Computer Science Department
School of Computer Science, Carnegie Mellon University
Deciding Type Equivalence in a Language with Singleton Kinds
Christopher A. Stone, Robert Harper
Internally, TILT represents programs using a predicative variant of Girard's F-omega enriched with singleton kinds, dependent product and function kinds (Sigma and Pi), and a sub-kinding relation. An important benefit of using a typed language as the representation of programs is that typechecking can detect many common compiler implementation errors. However, the decidability of typechecking for our particular representation is not obvious. In order to typecheck a term, we 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 paper we concentrate on the key issue for decidability of typechecking: determining the equivalence of well-formed type constructors. We show this problem decidable by presenting a sound, complete, and terminating decision algorithm. These properties are established by a novel Kripke-style logical relations argument inspired by Coquand's result for type theory.