Extensions to the Ptolemy II Type System
Yuhong Xiong and Edward A. Lee, UC Berkeley
yuhong@eecs.berkeley.edu
We will present two extensions to the basic type system in Ptolemy II. 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.
One extension we have developed is to add support for structured types such as array and record types. We 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.