Ptolemy II Type System

Ptolemy II has a sophisticated type system that supports extensive polymorphism. The basis for the type system is a complete partial order (CPO) representing the relationships between types. The ordering relationship is one of lossless convertibility. I.e., type a is less than type b if an instance of type a can be converted losslessly to an instance of type b. For example, type IntToken is less than type DoubleToken which is less than ComplexToken. However, BooleanToken is incomparable to all of these (it is neither less than nor greater than them). A lesser type is more specific than a greater type, or a greater type is more general. Type constraints in an actor are specified as inequalities with respect to this CPO. Thus, for example, an actor may declare that its output type is at least the type of one of its parameters. The type resolution mechanism finds the least types (the most specific types) in the CPO that satisfy all the constraints.

Backward type inference addresses the problem of inferring type specifications for dynamic data in Ptolemy II by leveraging its existing type inference mechanism. Ptolemy II is statically typed and therefore requires all ports to resolve to a type prior execution. When an actor mediates access to untyped data, or data is subject to unexpected changes, there is no way to reliably infer the type of its output from the actor itself. Manual annotations are tedious and make models more brittle than necessary. The basic idea is to let type constraints imposed by downstream actors determine the type of the otherwise underdetermined output ports of actors that mediate access to untyped resources. This is achieved using additional type constraints between and within actors. Backward inferred types serve the goal of achieving maximally permissive composition, as they are specific enough not to limit composability and general enough not to impose unnecessary constraints on the data. This solution has been implemented in Ptolemy II and the goal of this poster is to familiarize users with its function.

To enable backward type inference, set the enableBackwardTypeInference parameter to true at the top level of the model.

References

  1. Edward A. Lee, Marten Lohstroh, and Yuhong Xiong, "The Type System," a chapter from
    Claudius Ptolemaeus, Editor, "System Design, Modeling, and Simulation Using Ptolemy II", Ptolemy.org, 2014. (included in the release as $PTII/doc/books/systems/PtolemyII_DigitalV1_02.pdf)
  2. Marten Lohstroh, "Maximally Permissive Composition of Actors in Ptolemy II," Masters Thesis, EECS Department, University of California, Berkeley, Technical Report No. UCB/EECS-2013-19, March 20, 2013.