Pure Subtype Systems

This paper introduces a new approach to type theory called pure subtype systems. Pure subtype systems differ from traditional approaches to type theory (such as pure type systems) because the theory is based on subtyping, rather than typing. Proper types and typing are completely absent from the theory; the subtype relation is defined directly over objects. The traditional typing relation is shown to be a special case of subtyping, so the loss of types comes without any loss of generality. Pure subtype systems provide a uniform framework which seamlessly integrates subtyping with dependent and singleton types. The framework was designed as a theoretical foundation for several problems of practical interest, including mixin modules, virtual classes, and feature-oriented programming. The cost of using pure subtype systems is the complexity of -theory. We formulate the subtype relation as an abstract reduction system, and show that the theory is sound if the underlying reductions commute...

• Type: Conference
• Year: 2010
• Where: POPL
• Authors: DeLesley S. Hutchins
• Keywords: POPL 2010, Programming Languages, Pure Subtype Systems, Pure Type Systems, Subtype Relation