Poly* - Questions and Answers

In comparison with other type systems, we believe that, even when using the width and depth restrictions that guarantee principal typings, Poly* can express everything that can be expressed by any previously proposed type system for an ambient-like calculus that we know of, except for systems that track single-threadedness, as first introduced by Safe Ambients. For future work, we plan (1) to formally verify our belief about the relative power of Poly* and previous type systems and (2) to introduce a generalized version of single-threadedness to Poly*.

Otherwise, we do not have any simple independent characterisation of Poly*'s expressive power. In general, the more detailed types are, the better chance the types will contain enough information to verify that a term satisfies a desired safety policy. Poly*'s types can become so detailed that in practice we frequently find it useful to restrict Poly*'s expressiveness in various ways to get smaller and less informative typings.

One can also compare with the full unrestricted Poly* system. The existence of principal typings (and feasibility of type inference) depends on two separate restrictions: the depth and width restriction. We have not been able to construct natural examples where the depth restriction seriously limits the precision of our analysis. The width restriction can sometimes cause real limitations, which in some situations lead to loss of spatial polymorphism relative to the unrestricted system. The use of marks (discussed in the technical report) alleviates these restrictions significantly.

Type checking — verifying that a purported type is indeed a type for a given term — is very fast; it is simply a matter of checking that a number of local closure rules for the type graph are satisfied. The dominating part of the cost is the computation of which closure rules are relevant at each node of the graph; the complexity of this depends on the reduction rules of the calculus and so does not look nice in the general case. For most realistic calculi, a specialised type checking algorithm can probably run in sub-quadratic time (relative to the size of the type).

Type inference is a different matter. We have not determined a complexity upper bound for our generic type inference algorithm. This is partly because it will vary depending on the details of the calculus being analyzed. But it is also because the particular algorithm we have implemented for now favors generality and simplicity over efficiency guarantees. We plan in the future to look more closely at efficiency issues but so far have been focusing on making it more usable.

We imagine that in practical applications of Poly* one will use a type inference specialised to a particular calculus and a particular set of type-shape constraints. With sufficiently tight constraints, a low polynomial running time can be guaranteed, but that would come at the price of spatial polymorphism. Polymorphism in whatever shape tends to lead to type inference problems that are formally very hard; Poly* is no exception. One may hope that in practise it will behave like Hindley-Milner type inference, which though mathematically EXPTIME-complete tends to behave almost linearly on realistically structured programs.

Yes and no. A shape predicate (which is the underlying concept in our types) and an ambient logic formula both denote sets of terms, and the denotation of a shape predicate could be understood by viewing it as somewhat unconventional representation of a formula in a restricted ambient logic.

However, the expressive power of shape predicates is much weaker than that of any general tree logic worthy of being called a "logic" at all. Shape predicates do not allow general Boolean operations and their meanings are always prefix-closed sets of trees. This comparative weakness is an advantage from a practical point of view: it allows one to check in polynomial time whether a given term matches a given shape predicate. Unrestricted tree logics have much less favourable complexities.

Our theory could almost certainly be expressed as a special case of abstract interpretation, but it is not clear that it would make anything easier. All significant parts of our development would still need to be present, only now figuring as properties of (and efficient techniques to compute in) a particular abstract value domain.

As far as Poly* and Meta* is concerned, a (sub)term that does not match any reduction rules is just a normal form and is therefore considered not to be an error.

As a user of Poly*, you are of course free to consider it an error if something that does not match the syntax of the target calculus is produced, e.g. if values like booleans and integers turn up in a position where ordinarily a capability would be expected. For each concrete calculus, it is easy to see from the final Poly* type whether it allows terms that one does not want to have generated. We have chosen not to make the type system check for such malformed terms by default, because it does not need to be integrated in the computation of which futures are possible for a term. It is best done as a post-check on the final type, and therefore it is cleaner to omit it completely from the core theory.

Additionally, it would make the interface to the system more complex if one had to specify which terms are considered malformed. In simple cases it may be possible to derive this information from the reduction rules (if a form is generated that can never match any form template in any rule, chances are that it signifies an error), but even then one may still want to use "unknown" forms to abstract away from parts of the term that one is not interested in. And some kinds of syntactic constraints cannot readily be extracted from the reduction rules, for example the rule in Channeled Ambients that only channel names can occur to the left of the semicolon in an ambient.

We are of course doing both. Any sound type system expresses a data flow analysis. Classical type safety results for functional and imperative languages can readily be expressed as data-flow properties, for example, "there is no flow from any of these constructors (all data constructors other than nil and cons) to any of these destruction points (all instances of car and cdr)". From the data-flow point of view, most type systems express a quite crude flow analysis where, for example, any Boolean value is conservatively predicted to flow to every program location that tests a Boolean. By adding flow labels, any type system can be easily extended to provide a more precise flow analysis that tracks the construction and use points of data items rather than just their syntactic form.

Similarly, nearly any data flow analysis can be expressed as a type system. In practice, for most data flow analyses, expressing them as type systems requires using intersection and union types. See the work of Palsberg & Pavlopoulou and also the work of Amtoft & Turbak for more details.

In this view, a type system is a data-flow analysis framework that has additional nice properties, such as subject reduction or the fact that it is less expensive to verify that an analysis result (respectively, a typing) applies to a program than to discover it from scratch. Because Poly* is also a type system, it does have these nice properties.

Unfortunately no, or at least not straightforwardly within the current formalism. The problem is that the movement actions in Dπ are non-local; a single action can move a process (or a location subtree) to anywhere else in the location tree, with the destination given by name. This means that we cannot write its reduction axioms as local reduce{...} schemes in Meta* if we want to represent the spatial structure as term structure, and that is currently our only way to get a handle on the spatial structure at all.

We are planning future work to add the possibility of such non-local reductions to Poly*/Meta*. This ought to be fairly straightforward in principle, though we are not yet certain how to present such an extended system in a non-confusing way. That is, the difficulties are primarily in devising a good notation for instantiating Meta* to such systems.

Dπ also has atomic Boolean tests on the structure of the location tree. It would probably not be difficult to hard-code the interpretation of this condition language into a Poly*-inspired type system specifically for Dπ, but it is not yet clear to us how to allow it directly in the Meta* framework in a smooth way that does not reek of being an ad-hoc feature solely meant for being able to implement Dπ.

Because Poly* is meant to work with a wide range of calculi with different application domains, we did not want to fix a specific property and declare that to be the fundamental safety property that Poly* analyses for. Instead, a Poly* typing gives enough information for the user of the system to check whichever property he wants to use.

Not having an explicit safety property attached is not an uncommon phenomenon for a bare-bones presentation of a type system. Consider, for example, the pure λ-calculus without constants, but possibly with let bindings or some recursion primitive. Its typeless semantics offer no way of "going wrong" that one would want a type system for a programming language to guarantee against. The classical type systems for pure λ calculus (simple types, System F, Hindley-Milner, etc) only acquire a useful notion of safety when one extends them to a more complex setting where run-time errors are conceivable. Yet nobody would suggest that the classical systems should not be thought of as type systems until one introduces constants.

Types often resemble the structure of the items that is being passed around between different pieces of the program. A well-known example of this is the notation for list and tuple types in Haskell, or records in ML. In mobility calculi, what is being passed around while the system evolves are entire processes, so it is natural that they would have types that resemble the structure of processes.

There may be some confusion because in type systems for λ-calculus-based languages, there are usually type forms that correspond to each value-creation form, but there are usually not any type forms that correspond to value-use forms. For example, the function-formation form (λx.M) has a corresponding type form σ → τ and the tuple-formation form (M,N) has a corresponding type form σ × τ. In contrast, the function-use form (M N) usually has no corresponding type form. Given a function M of type σ → τ and an argument N of type σ, instead of building a type of the form ((σ → τ) σ) for the application (M N), instead one directly uses the type τ of the function result. This is reasonable because the type τ predicts all useful properties of the result of the application.

For sequential languages, this way of handling types is reasonable, because once a function has been applied to an argument, the function and argument can not interact with other functions and arguments. However, for concurrent languages, once potentially interacting forms are joined by parallel composition, it is not uniquely determined that the forms will in fact interact exclusively with each other. The type assigned to a parallel composition (M | N) must of course predict the possible result of M and N interacting. However, because of the possibility that (M | N) will be put in parallel composition with another process P, forming ((M | N) | P) = (M | (N | P)) = ((P | M) | N), the type of (M | N) must also remember the types of M and N in order to be able to predict the possible interactions of M with P and also of N with P. So for concurrent languages, there is no neat division into value-creation forms which must have corresponding type constructors and value-use forms which do not need to have corresponding type constructors.