Edit Page | Printable View

<< Classes, Refinement and Composition | Contents | Bindings >>

Dependent Types (dep.gen)

(dep.gen.1) Caesar supports all Java types and dependent types.

Def: A dependent type is a type of form exp.cls, where exp is an expression returning an object which is an instance of a cclass, and cls is a virtual class of the object. The object is also called family of the type, and expression exp is called family expression.

Def: A plain type is a normal Java type: a primitive type, an interface, a class (Java as well as Caesar class) or an array on another plain type.

Def: The static type of an expression in a certain context is the most specific class, which is known to be the supertype of all possible runtime types, which can take the expression in this context.

Def: The static type of a dependent type exp.cls is the inner class cls in the static type of the family expresion exp.

(dep.gen.2) Virtual class can be used as a dependent type if it is qualified with an expression, representing the path to its family object.

(dep.gen.3) Virtual class can be used as a plain type, if it is qualified by the names of its enclosing classes.

Family Expression (dep.famexp)

Family expression is the type declarations are limited only by the cases listed below.

(dep.famexp.1) Family expression may start from

• this reference
• reference to some outer object of this,
• a local variable, declared as final,
• a method argument (final),
• a static field (final).

(dep.famexp.2) Beginnings of form this and some outer of this may be also determined implicitly. The outer of this will be further denoted by this.outer(1), the outer of outer by this.outer(2) and so on.

Listing 1.

 
public cclass Graph {
   public boolean areConnected(Node n1, Node n2) { 
      ... 
   }
   public cclass Node { 
      ...
   }      
   public cclass Edge {
      Node n1, n2;
      Node getStart() { return n1; }
      ...
   }
}

Example: All types used in List. 1 are actually dependent types, but all family expressions are implicit. References to Node or Edge in the context of Graph are assumed as correspondingly this.Node and this.Edge. In the context of Edge, Node types are assumed to be properties of owner graph, i.e. this.outer(1).Node. With explicit annotations the same example will look as in List. 2.

Listing 2.

 
public cclass Graph {
   public boolean areConnected(this.Node n1, this.Node n2) { 
      ... 
   }
   public cclass Node { 
      ...
   }      
   public cclass Edge {
      this.outer.Node n1, n2;
      this.outer.Node getStart() { return n1; }
      ...
   }
}

(dep.famexp.3) Family expression may contain any number of accesses to final class fields.

(dep.famexp.4) In family expression exp.field, field must be visible in the static type of exp in the context of type declaration.

Example: In List.3 the family expression of variable a5 is this.map.roads. Here this is impicitly determined, map and road are final fields.

Listing 3.

  
public cclass Map { ...
   public final Graph roads = new Graph();   
   public roads.Edge findRoad(String name) { ... } 
}

public cclass MapTest {
   final Map map = buildMap();

   public void test() {
      map.roads.Edge a5 = map.findRoad(name);
   }
}

Places of Usage (dep.use)

(dep.use.1) Dependent types can be used as type declarations of

• class fields
• local variables
• method parameter types
• method return values

Type Checking (dep.check)

(dep.check.1) A type of an expression can be a plain type or a dependent type.

(dep.check.2) A dependent type of an expression is determined by its static type and its family. So a dependent type of an expression can be characterized by a pair <fam, cls>, where fam is the statically known family of the object returned by expression and cls is static type of the expression.

(dep.check.3) A dependent type <fam, cls> is a subtype of a plain type type if cls is a subtype of of type.

(dep.check.4) A dependent type <fam1, cls1> is a subtype of another dependent type if <fam2, cls2> if fam1 is equivalent to fam2 and cls1 is a subclass of cls2.

Example: In List 4. all variables belong to family this.map.roads, therefore they can accept values only from this family of corresponding static types (Graph.Edge or Graph.Node).

Initialization of variable a6 will fail because its initialization expression returns object of different family (this.map.rivers).

Initialization of startA6 will fail, because the variable has static type Graph.Node, but its initialization expression returns an object with static type Graph.Edge.

Listing 4.

  
public cclass Map {
   public final Graph roads = new Graph();   
   public final Graph rivers = new Graph();
   
   public rivers.Edge findRiver(String name) { ... }   
   public roads.Edge findRoad(String name) { ... }   
}

public cclass MapTest {
   public final Map map = buildMap();

   public void test {
      map.roads.Edge a4 = map.findRoad("A4"); /* OK */
      map.roads.Node startA5 = map.findRoad("A5").getStart(); /* OK */
       
      map.roads.Edge a6 = map.findRiver("Elbe"); /* error */
      map.roads.Node startA6 = map.findRoad("A6"); /* error */
   }   
}

Equivalence of Family Identities (dep.fameq)

(dep.fameq.1)A cannonical family expression of a family expression exp

• has the form base.field1...fieldN,
• always refers to the family of exp at runtime
• and is valid at the context of exp.

Here base is this, this.outer(n), a local variable, a formal method argument or a static field.

(dep.fameq.2) The families of two expressions are equivalent, when they can be represented the same cannonical family expressions.

If one of the families cannot be reduced to a cannonical form it is not equivalent to any other family.

The cannonical family expression of an expression is determined by following rules:

• (dep.fameq.3) family expression of a local variable loc, is the family expression of the type declaration of the variable.

• (dep.fameq.4) family expression of a field access exp.field is an expression, obtained by substituting this with exp in the family expresion of the declared type of field.

• (dep.fameq.5) family expression of a method call exp.meth(..) is an expression,
  • obtained by substituting this with exp in the family expresion of the declared return type of meth, if the return type has this or this.outer(n) as base
  • obtained by substituting formal argument name with the corresponding argument expression in the family expression of the declared return type, if the return type has the argument as family base.
  • the declared family expression of the return type, in all other cases.

• (dep.fameq.6) expression of form exp.field.outer(n)... is reduced to expression exp2.outer(n-1).... Where exp2 is an expression, obtained by substituting this with exp in the family expresion of the declared type of field. Terms outer(0) are simply removed.

• (dep.fameq.7) expression of form exp.meth(..).outer(n)... is reduced to expression exp2.outer(n-1).... Where exp2 is an expression, obtained by substituting this with exp in the family expresion of the declared return type of meth.

• (dep.fameq.8) family expression of a static field, is the family expression of the type declaration of the field.

• (dep.fameq.9) family expression of a formal argument in the method call exp.meth(..) is an expression,
  • obtained by substituting this with exp in the family expresion of the declared argument type, if the argument type has this or this.outer(n) as base
  • obtained by substituting formal argument name with the corresponding argument expression in the family expression of the declared argument type, if the argument type has another argument as family base.
  • the declared family expression of the argument type, in all other cases.

Example: Let's consider initialization of variable startA5 in the List.4. We have to check if the type of its initialization expression this.map.findRoad("A5").getStart() is a subtype of the type of startA5.

The cannonical family expression of the variable startA5 is the family expression of its type declaration (dep.fameq.3), i.e. this.map.roads. So the type of startA5 is <this.map.roads, Graph.Node>.

To determine the family expression of this.map.findRoad("A5").getStart(), we first look at the declared type of getStart() in List.1. It is this.outer(1).Node. According dep.fameq.5 we substitute this in the family expression with this.map.findRoad("A5") and obtain this.map.findRoad("A5").outer(1).

Now we have to reduce this.map.findRoad("A5").outer(1) further according dep.fameq.7 The declared return type of findRoad() is this.roads.Edge. We take the family expression of this type and substitute this with this.map. So, we get this.map.roads. Now we can use the new expression to reduce outer access: this.map.roads.outer(0).

outer(0) is simply removed and we get, that the cannonical family expression of this.map.findRoad("A5").getStart() is this.map.roads and its type is <this.map.roads, Graph.Node>.

We have determined that the dependent type of the initialization expression of startA5 is the same as the type of startA5. So this assignment is type safe.

<< Classes, Refinement and Composition | Contents | Bindings >>