Deciding type equivalence in a language with singleton kinds
C. Addison Stone, Robert W. Harper · 2000
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.