An Extended Type System for Component-Based Design

Researchers: Yuhong Xiong
Advisor:Edward A. Lee
Type systems in modern programming language are the most widely used and effective (semi)formal verification tools for software. The theory underlying type systems is simple, robust, and extremely powerful, based on fixed-point theorems in topology. The mathematical structure of a set of types is abstractly a lattice, and the theory can be applied to any property of the software that can be characterized using a lattice. It need not be restricted to classical data types.

In view of this, we have designed a set of Java classes in Ptolemy II that provide support for any type system that can be represented using such a lattice. This generic infrastructure has been first applied to the basic type system problem, that of ensuring consistent data typing, and supporting (polymorphic) type inference. But the infrastructure is designed to be extended to more sophisticated uses.

The basic type system combines static typing with run-time type checking. It supports polymorphic typing of system components, and allows automatic lossless type conversion at run-time. To achieve this, we use a lattice to model the lossless type conversion relation among types, and use inequalities defined over the type lattice to specify type constraints in components and across components. The system of inequalities can be solved efficiently, with existence and uniqueness of a solution guaranteed by fixed-point theorems. This type system increases the safety and flexibility of the design environment, promotes component reuse, and helps simplify component development and optimization.

We are currently developing two extensions. One extension is to add support for structured types such as array and record types. The goal is to allow the elements of arrays and records to contain data tokens of arbitrary types, including structured types, and be able to specify type constraints on them. Type constraints and type inference must propagate transparently across operators that construct and disassemble such structures. One of the major difficulties in this extension is that the type lattice becomes infinite, which raises questions on the convergence of type checks and inference.

A more innovative (and speculative) extension is to process-level types. These types represent dynamic properties of an application, rather than the static data types traditionally dealt with in a type system. We are developing methods to characterize the communication protocols used between system components, and some of the real-time properties of the system, as types in a type lattice. If we are successful, the same type system infrastructure can facilitate heterogeneous real-time modeling. This may potentially bring some of the benefit of modern type systems to the process level.

Last updated 11/05/99