Genericity through Constrained Types

Modern object-oriented languages such as X10 require a rich framework for types capable of expressing value- dependency, type-dependency and supporting pluggable, application-specific extensions. In earlier work, we presented the framework of con- strained types for concurrent, object-oriented languages, parametrized by an underlying constraint system C. Con- straint systems are a very expressive framework for partial information. Types are viewed as formulas C{c} where C is the name of a class or an interface and c is a constraint in C on the immutable instance state of C (the properties). Many (value-)dependent type systems for object-oriented languages can be viewed as constrained types. This paper extends the constrained types approach to handle type-dependency ("genericity"). The key idea is to extend the constraint system to include predicates over types such as X is a subtype of T. Generic types are supported by introducing parameters and properties that range over types and permitting the user program to impose constraints on such variables. Type-valued properties are required to have a run-time representation—the run-time semantics is not defined through erasure. Run-time casts are permitted through dynamic code generation. To illustrate the underlying theory, we develop a formal family FX(C) of programming languages with a common set of sound type-checking rules. By varying C and extend- ing the type system, we obtain languages with the power of FJ, FGJ, dependent types, and new object-oriented lan- guages that uniformly support value- and type-dependency. Concretely, we illustrate with the design and implementa- tion of the type system for X10. The type system integrates and extends the features of nominal types, virtual types, and path-dependent types.