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:
[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;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 Nodeinit
). 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!