<< 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(n1)...
. 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(n1)...
. 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 >>