Compound types for Java

Abstract

Type compatibility can be defined based on name equivalence, that is, explicit declarations, or on structural matching. We argue that component software has demands for both. For types expressing individual contracts, name equivalence should be used so that references are made to external semantical specifications. For types that are composed of several such contracts, the structure of this composition should decide about compatibility. We introduce compound types as the mechanism to handle such compositions. To investigate the integrability into a strongly typed language, we add compound types to Java and report on a mechanical soundness proof of the resulting type system. Java users benefit from the higher expressiveness of the extended type system. We introduce compound types as a strict extension of Java, that is without invalidating existing programs. In addition, our proposal can be implemented on the existing Java Virtual Machine.