Orc will use a type system which is a subset of DOT (https://doi.org/10.1145/3022671.2984008). The restrictions will make it easier to type check and align with restrictions applied to Scala (http://dotty.epfl.ch/blog/2016/02/17/scaling-dot-soundness).

  1. Eliminate dependent method types by removing the rule TAppVar and allowing TApp to take over those cases, and eliminating the dependent methods from the type symtax.
  2. Paths for type selections can only contain branch bound variables. It is not clear how this change would affect the formal static semantics. I think the Scala work on the subject is based on the principle that path elements need to have the same properties as values in DOT, but other values do not, so as long as paths are only allowed to contain values that act like dot values things are OK.

Reintroducing Path Dependent Types#

The restrictions above are hopefully temporary. To reintroduce path dependent types, we will need to determine which values can safely be used as path elements. The key insight is that values do not need to exist when the path is used as long as the value is guaranteed to exist eventually. The restriction on path elements is basically that the future associated with that element must be filled without failing.

Dave and Arthur have both thought about the usefulness of type-level tracking of publication count on Orc expressions. For instance, an expression could have type T(1-2) (meaning publications are of type T and there will be one or two publications). Extending this graft variables and def parameters, results in variables which must be bound eventually. Such variables are legal elements of paths.

Checking these publication count types is undecidable. Undecidability is clear from the fact that publication counts subsume both null tracking and totality checking. Publication count types would require tracking stop the same way as null in other languages and handle recursive calls similarly to totality checking.

Publication count types may be possible to approximately check and even infer approximate bounds on the number of publications. A simple approximation may allow for path dependent types on enough values to cover the common cases of ML-style modules and similar things.

Implementing the Initial Subset of DOT#

DOT is surprisingly syntax directed. A naive implementation of the DOT type and subtype checking algorithms will probably fail to solve some cases. However, a naive implementation may well handle even large scale developments with some care. So the initial implementation will be as simple as possible with no optimization or "intelligence". It may require a simple constraint solver.

Add new attachment

Only authorized users are allowed to upload new attachments.
« This page (revision-5) was last changed on 29-Jan-2017 21:17 by Arthur Peters