Dependent Object-oriented Language, or DOL for short, is an imperative object-oriented programming language featuring a dependent type system based on index refinements. The language supports mutable objects and class-based inheritance with subtyping.

Conventional types can express many useful properties about data, but sometimes
you want to say more. Using dependent types you may, for example, sharpen the
type of a bank account with a natural number `b`

denoting its balance, written
`Account<b>`

. Any attempt to overdraft the account will by signalled by the
compiler as a type error. The binary search property may also be maintained
statically using dependent types. `BST<2,8>`

is a possible type of non-empty
tree where the abstraction is built upon the smallest and greatest keys
appearing in the tree.

Extending an imperative object-oriented language with types that provide additional guarantees is the purpose of DOL. This is the first implementation of a type system combining three very different features: dependent types, mutable objects, and class-based inheritance with subtyping.

To follow this tutorial and use DOL effectively, it will help if you have some general understanding of object-oriented programming and a notion of dependent types.

The main distinctive feature of DOL is the introduction of special "index" variables in types that can be used to express and statically enforce properties. DOL uses indices to constrain object types.

An index variable is a special variable that belongs to a quite limited type if we want to make the language decidable. DOL currently supports index types of the integer and boolean domains:

`integer`

, distinct from the class type`Integer`

, is the index type of integer numbers;`boolean`

, distinct from the class type`Boolean`

, is the index type of boolean values.

These types can be refined quite naturally writing subset types such as
`{x:integer | x<0 || x>0}`

that stands for all integers but zero. For
convenience, abbreviations are accepted for common types: `natural`

is
equivalent to `{x:integer | x>=0}`

, and `positive`

is short for ```
{x:integer |
x>0}
```

.

The simplest example of a DOL type is a class, declared as in Java, except that
it may have index variables introduced in the header. Other than that, a class
in DOL resembles a typical class in an object-oriented language, characterised
by fields and methods, including a constructor `init`

.

For example, a class declaration for a bank account may look like this:

```
class Account<b:natural> {
balance: Integer<b> // the only field
init(): Account<0> =
balance := 0
<m:natural>
[Account<b> ~> <b+m>]
deposit(amount: Integer<m>) =
balance := balance + amount
<m:natural{m<=b}>
[Account<b> ~> <b-m>]
withdraw(amount: Integer<m>) =
balance := balance - amount
getBalance(): Integer<b> =
balance // return balance
main() =
var acc := new Account();
acc.deposit(100);
acc.withdraw(30);
print(acc.getBalance())
}
```

Subsequent sections of this tutorial will explain the unfamiliar type features
step by step. For now, let's focus on the type of the single field `balance`

(line 2) indexed by some natural number `b`

which stands for the account's
current balance. The class also includes a constructor (line 4) that when invoked
by the new operator gives the proper (or concrete) type `Account <0>`

to the new object.

Note that classes introduce universally quantified index variables (the `all`

annotation being omitted).

Like classes, methods in DOL may declare index variables to constrain parameter types. Calling methods on an object may cause it to change; indices can be used to guarantee that after any such change the object remains in a consistent state.

We can give indexed signatures to methods. For example, the withdraw method is as follows:

```
<m:natural{m<=b}>
[Account<b> ~> <b-m>]
withdraw(amount: Integer<m>) =
balance := balance - amount
```

Methods in DOL differ from conventional Java-like methods in three ways:

- methods may declare index variables in angle brackets to constrain the types of parameters;
- methods that change state must describe that change in types. For example,
`[Account<b> ~> <b-m>]`

, read "`Account<b>`

becomes`Account<b-m>`

", describes the (implicit) receiver with the first type being the input type and the second one the output type; - methods may omit the return type; when omitted, the typechecker assumes
the supertype
`Top`

.

In practice, the DOL typechecker guarantees that if an object's input type is satisfied on method entry, then the object may assume the output type on method exit. Input and output types correspond to checks on method entry and exit. Moreover, the class invariant is enforced at all times.

DOL detects when a method implementation fails to meet its signature
specification. For example, a `withdraw`

method implementation that is not
consistent with its type produces an error. Try it:

```
class WrongAccount<b:natural> {
balance: Integer<b> // the only field
init(): WrongAccount<0> =
balance := 0
<m:natural>
[WrongAccount<b> ~> <b+m>]
deposit(amount: Integer<m>) =
balance := balance + amount
<m:natural{m<=b}>
[WrongAccount<b> ~> <b-m>]
withdraw(amount: Integer<m>) =
balance := amount - balance
getBalance(): Integer<b> =
balance // return balance
}
```

Client code is typechecked under class and method constraints. In class
`Account`

, we have included a `main`

method that unity tests the class.
Attempting to withdraw an amount that will result in a balance below zero
produces an error. Try also this one:

```
class Account<b:natural> {
balance: Integer<b> // the only field
init(): Account<0> =
balance := 0
<m:natural>
[Account<b> ~> <b+m>]
deposit(amount: Integer<m>) =
balance := balance + amount
<m:natural{m<=b}>
[Account<b> ~> <b-m>]
withdraw(amount: Integer<m>) =
balance := balance - amount
getBalance(): Integer<b> =
balance // return balance
main() =
var acc := new Account();
acc.deposit(1000);
acc.withdraw(3000); // an error is expected here!
acc.deposit(1000)
}
```

Constants and operators are used in the programmer’s language only to make arithmetic and logic operations look more familiar, since they are not part of DOL’s core language.

Constant `100`

can be used as an argument as follows:

```
acc.deposit (100)
```

The subtraction operator appears in the body of the `withdraw`

method, namely

```
balance := balance − amount
```

Formally, Integer and Boolean, implemented natively, are families of classes.
Here are some of the methods defined in the `Integer`

and `Boolean`

"interfaces":

```
class Integer<i:integer> {
init(): Integer<0>
<j:integer>+(value: Integer<j>): Integer<i+j>
<j:integer>-(value: Integer<j>): Integer<i-j>
<j:integer><=(value: Integer<j>): Boolean<i≤j>
<j:integer>=(value: Integer<j>): Boolean<i≥j>
...
}
class Boolean<b:boolean> {
init(): Boolean<true>
<a:boolean>&&(value: Boolean<a>): Boolean<b∧a>
<a:boolean>||(value: Boolean<a>): Boolean<b∨a>
}
```

Technically, constant `0`

, used in method bodies, distinct from the index `0`

used in types (as in `Integer<0>`

), is syntactic sugar for a fresh object
reference returned by `new Integer()`

. Subtraction is translated into the call
`balance.minus(amount)`

before typecheking.

Like Java, DOL supports single class inheritance. The `extends`

declaration is
optional. If omitted, the class is derived from the `Top`

default superclass provided by
DOL, similar to the `Object`

class in Java, except that `Top`

has no fields or
methods but for the `init`

constructor. Subtypes in DOL inherit fields and
methods from their supertypes, but also index constraints from its proper
supertypes.

For example, class `PlusAccount`

represents a class derived from `Account`

that
adds two additional index variables, `s`

and `c`

, and uses them to constrain two
new fields, `savings`

and `checking`

, that describe two portions of the balance.

```
class PlusAccount<s:natural, c:natural, b:natural> extends Account<b> {
savings: Integer<s> // two extra fields
checking: Integer<c>
...
}
```

We then relate the two new fields in the subclass with the superclass’s field by
enforcing that `b=s+c`

via method signatures. We override the `deposit`

method
as follows:

```
<m:natural>
[PlusAccount<s,c,b> ~> <s+m,c,b+m>]
deposit(amount: Integer<m>) =
super.deposit(amount);
savings := savings + amount
```

The `deposit`

method adds the amount to the account’s balance by calling the
superclass method, and then adds it to the savings field. The `withdraw`

method
must be redefined in order to take out the amount from each balance portion as
follows:

```
<m:natural{m<=b and b=s+c}>
[PlusAccount<s,c,b> ~> <max(s-m,0),min(c,c-m+s),b-m>]
withdraw(amount: Integer<m>) =
super.withdraw(amount);
if amount <= savings {
savings := savings - amount
} else {
checking := checking - amount + savings;
savings := 0
}
```

The complete example of `PlusAccount`

can be found in the Examples page.

Binary search trees can naturally be described by the discipline of dependent types. We implement the binary search tree in an imperative style, allowing subtrees to be modified in place, and use types to enforce statically the standard binary search tree property.

We define `BST`

as the "public" family of classes that creates and manages both
empty and nonempty trees using `Nil`

(a proper class) and `Node`

(a family of
classes). Our binary search tree contains integer numbers included in a loose
pair of bounds `<l:integer,u:integer>`

declared in the header of `BST`

that can
be used to define an interval [l,u]. Any element in a tree can find a place
within the minimum (`l`

) and maximum (`u`

) keys.

Nullable references are commonly used in Java-like languages to build data structures, but have been a recurring source of error (Hoare's billion dollar mistake). DOL enables programmers to build imperative linked data structures in a null-free style using union types.

The `BST`

has a single field root that is either `Nil`

or `Node`

. We declare it
as follows:

```
class BST<l:integer,u:integer> {
root: Nil + Node<l,k,u> where k:integer{l<=k<=u} // the only field
...
}
```

A dependent existential quantified constructor (denoted by `where ...`

) is
used to keep track of the key, hidden in the field type, so that the binary
search tree invariant can be enforced at compile time.

The special `init`

method creates an empty binary search tree to which we give
type `BST<2,1>`

, making `root`

an instance of `Nil`

.

```
class BST<l:integer,u:integer> {
root: Nil + Node<l,k,u> where k:integer{l<=k<=u} // the only field
init(): BST<2,1> =
root := new Nil()
...
}
```

On the other hand, the `Node`

class defines a field key, which holds the node value,
and fields `left`

and `right`

that may represent the two subtrees. We use union and
existential types, again pushing the data requirements inward to the types of
the `left`

and `right`

fields.

```
class Node<l:integer, k:integer, u:integer{l<=k<=u}> {
key: Integer<k> // fields
left: Nil + Node<l,k1,u1> where k1:integer, u1:integer{l<=k1<=u1<=k}
right: Nil + Node<l1,k1,u> where l1:integer, k1:integer{k<=l1<=k1<=u}
...
}
```

Notice that the type of the `left`

field enforces the fact that all the values
appearing in the left subtree must be in the interval defined by [l,k], so that
the binary search tree invariant can be enforced. Similarly, the type of the
`right`

field enforces the fact that all the values appearing in this subtree
must be included in [k,u].

By definition, leaf nodes are such that `l=k=u`

. Here's the constructor
signature:

```
class Node<l:integer, k:integer, u:integer{l<=k<=u}> {
key: Integer<k> // fields
left: Nil + Node<l,k1,u1> where k1:integer, u1:integer{l<=k1<=u1<=k}
right: Nil + Node<l1,k1,u> where l1:integer, k1:integer{k<=l1<=k1<=u}
init(x: Integer<v>): Node<v,v,v> =
key := x;
left := new Nil();
right := new Nil()
...
}
```

Now, let's insert an element into the BST tree. The method takes as argument an integer value and provides a useful demonstration of a case discrimination construct that looks at the type structure of the root field:

```
<v:integer>
[BST<l,u> ~> <min(l,v),max(u,v)>]
insert(value: Integer<v>) =
case root {
Nil => root := new Node(value)
Node => root.add(value)
}
```

It's actually the `Node`

class that implements the main insertion algorithm.
Its method `add`

takes an argument similar to the one above, and also uses a
case discrimination construct to look at the type structure of the two subtree
fields:

```
<v:integer>
[Node<l,k,u> ~> <min(l,v),k,max(u,v)>]
add(value: Integer<v>) =
if value < key {
case left {
Nil => left := new Node(value)
Node => left.add(value)
}
} else {
if value > key {
case right {
Nil => right := new Node(value)
Node => right.add(value)
}
}
}
```

We add an element to the tree by comparing the value to the key stored at each node, and recursively descending into the appropriate subtree until a leaf is reached that allows adding the new node.

The precise types given to the `BST`

and `Node`

classes allow the typechecker to
detect a number of common programming errors. For example, the compiler will
report a type error if we try to call the add method as follows:

```
<v:integer>
[BST<l,u> ~> <min(l,v),max(u,v)>]
insert(value: Integer<v>) =
root.add(value)
```

Because `root`

declares a union type, we cannot call a method directly on it;
first, we must use a case construct to analyse the type of the field and
discover whether the object is an instance of `Nil`

or `Node`

.

Similarly, the compiler will object to the wrong conditional test below:

```
<v:integer>
[Node<l,k,u> ~> <min(l,v),k,max(u,v)>]
add(value: Integer<v>) =
if value > key {
case left {
Nil => left := new Node(value)
...
}
}
```

Here, the compiler will report inconsistent constraints. The `case`

construct is
correctly used to find out that left is a `Nil`

. Then, the assignment changes
the type of the left field to Node`init`

). However, the compiler assumes `v > k`

from the conditional test, after
which will not be able to assert `v <= k`

issued from the new type of the left
field.

Deletion from the binary search tree may involve removing a key not only from
the tree’s leaf nodes but also from an interior node. Unlike insertion, in which
`min`

and `max`

could be used to issue the new value’s standing vis-à-vis the
minimum and maximum keys existing in the tree, deletion delivers the same binary
search tree where the new minimum or maximum may be hidden in the subtrees.

However, we can still establish that the implementation is type correct, ensuring that the tree after deletion is within the bounds, no matter where the key removal occurs (from a fringe or the middle of the tree).

The remove method in the BST class requires the value `v`

about to be removed,
if it exists, to be within the tree bounds (`l≤v≤u`

). The method is implemented
as usual:

```
<v:integer>
remove(value: Integer<v>) =
case root {
Nil => skip
Node =>
if root.isLeaf(value) {
root := new Nil()
} else {
root.deleteChild(value)
}
}
```

We check if root is a `Nil`

, in which case we are done as the tree is empty.
Otherwise, root is a `Node`

, and we determine if it is a leaf holding the value
to be removed. Deletion is accomplished either by setting root to a fresh `Nil`

object, or by calling the recursive method `deleteChild`

on it in order to run
the algorithm. As we will see, the `deleteChild`

method may change locally the
type of the root field. However, the ordering constraint is hidden in the field
type, which means that the type of the receiver as viewed from outside does not
change, so we simply omit it in the `remove`

method signature.

The task of deleting a child can basically be divided in three stages: finding
the key to remove, looking for a minimum key (guaranteed via types to be within
bounds) to replace the one being deleted, and applying deleteChild to remove the
node whose key we took. This is implemented in class `Node`

- the code can be
found in the Examples page.

Shared state can be tricky to handle in a type system such as that of DOL. The reason for this is that if two variables contain references to the same object, the state of the object can be modified using one, but the altered state cannot be observed through the type of the other variable.

The two potential sources of aliasing problems in the language are assignment and parameter passing. A simple linear discipline is implemented to prevent inconsistencies between an object's type and its state.

As an example, the following code should produce an error:

```
class Account<b:natural> {
balance: Integer<b> // the only field
init(): Account<0> =
balance := 0
<m:natural>
[Account<b> ~> <b+m>]
deposit(amount: Integer<m>) =
balance := balance + amount
<m:natural{m<=b}>
[Account<b> ~> <b-m>]
withdraw(amount: Integer<m>) =
balance := balance - amount
getBalance(): Integer<b> =
balance // return balance
main() =
var acc := new Account();
acc.deposit(70);
var alias := acc;
acc.withdraw(30)
}
```

However, when a class is type invariant, because all its methods are type invariant, i.e. the input and output types coincide (or are omitted), linearity is not imposed, allowing objects to be freely shared.

DOL is a prototype, lacking some useful features. For example, DOL provides
support for base types such as `Integer`

and `Boolean`

objects, but does not
come with strings. Some constructs, such as the `while`

loop, are available, but
have limited usefulness. As an active research project, we are gradually working
on improvements and fixing bugs. Stay tuned!