Most formal accounts of object-oriented languages have focussed on type soundness: the safety that type checking provides with respect to term-level computation and abstractions. However, with type-level abstraction mechanisms becoming increasingly more sophisticated, bringing this guarantee to the level of types has become quite pressing.We call this property kind soundness: kind checking ensures that type constructors are never applied to unexpected type arguments. We present Scalina, a purely object-oriented calculus that employs the same abstraction mechanisms at the type level as well as at the kind level. Soundness for both levels can thus be proven by essentially the same arguments. Kind soundness finally allows designers of type-level abstractions to join their term-level colleagues in relying on the compiler to catch deficiencies before they are discovered by their clients.
Presented at FOOL'08; Sunday, 13 January 2007; San Francisco, California, USA.