DOL

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.

Motivation

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.

Usage

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.

Index 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}.

Classes

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())
}
Load in editor

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

State modifying methods

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:

  1. methods may declare index variables in angle brackets to constrain the types of parameters;
  2. 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;
  3. 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
}
Load in editor

Modifiable reference types

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)
}
Load in editor

Base types

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.

Inheritance

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.

Example: BST

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 (which is the type given to it by 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 vabout 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.

Other Features

Controlled aliasing

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)
}
Load in editor

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.

Limitations & Bugs

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!

Run
$