Deciding Type Equivalence in a Language with Singleton Kinds

摘要

Work on the TILT compiler for Standard ML led us to study a language with singleton kinds: S(A) is the kind of all types provably equivalent to the type A. singletons are interesting because they provide a very general form of definitions for type variables, allow fine-grained control of type computations, and allow many equational constraints to be expressed within the type system.