We're about to talk about...

A type system for:

• Generic Mutability
• Generic Nullity
• with flexible initialization
• soundness arguments
• and a simple runtime

We're about to talk about...

A type system for:

• Generic Mutability
• Generic Nullity (this is new!)
• with flexible initialization
• soundness arguments
• and a simple runtime (this isn't new, but it's notable)

We're about to talk about...

• We should motivate that,
• have a look at existing solutions, (plenty of cross-over between mutability and nullity),
• settle on a model for initialization,
• explore the technical details.
• Generic nullity?
• Runtime?
• Typing judgements?

Imagine the following world...

• We have people (people are good).
• Some people have pets.
• Pets have owners.
• Pets and owners are mutually loyal (I keep my pet forever...)

class Person {
    Pet pet;
}
                

class Turtle : Pet {
    Person owner;
}
                

How do we write the code?

I would like to be able to write code like the following: (this is still in Java world)

void main() {
    Person neil = new Person();  // Neil doesn't want a turtle (yet)

    Person peter = new Person(); // Peter loves turtles.
    Turtle tom = new Turtle();   // Tom needs an owner.
    peter.pet = tom;
    tom.owner = peter;

}
            

class Person {
    Pet pet;
}
            

class Turtle : Pet {
    Person owner;
}
            

This is far from expressive

void main() {
    Person neil = new Person();
    Person peter = new Person(); 
    Turtle tom = new Turtle();   
    /* What if we just forget to set these?
     * peter.pet = tom;
     * tom.owner = peter;
     */

}
                

This is what my project is about.

• We want to express nullity (Peter will definitely get a turtle)
• We want to express mutability (Peter will keep his turtle)
• We want it to be generic (Neil doesn't have to have a turtle)
• ... but he might get one later

We want to be able to express (and enforce) all of this through the type system.

And this is how it looks:

/* A Person is parametrized by its own mutability, and one more nullity constraint */ 
class Person[i]<,n1> {
    /* pet shares the Person's mutability, and has parametrized nullity */
    Pet[i, n1]<,> pet; 
}
            

/* A Turtle is parametrized by its own nullity, and nothing else */ 
class Turtle[i]<,> : Pet {
    /* A Turtle's owner must share its mutability */ 
    Person[i, NotNull]<,NotNull> owner;
}
            

And this is how it looks:

...
/* Neil has a Nullable pet, but can change */
neil = new Person[Mutable, NotNull]<,Nullable>;


/* Peter has a NotNull pet, and can't change */
peter = new Person[Immutable, NotNull]<,NotNull>;
/* Tom is an Immutable pet */
tom = new Turtle[Immutable, NotNull]<,>;

/* Type error: Didn't initialize peter.pet or tom.owner */
                

class Person[i]<,n1> {
    Pet[i, n1]<,> pet; 
}
                

class Turtle[i]<,> : Pet {
    Person[i, NotNull]<,NotNull> owner;
}
                

Context?

Type systems for nullity and mutability aren't a new thing.

Context?

Type systems for nullity and mutability aren't a new thing.

Context?

Type systems for nullity and mutability aren't a new thing.

Context?

Type systems for nullity and mutability aren't a new thing.

Context?

Type systems for nullity and mutability aren't a new thing.

class Person {
    Person() {
        this.pet = 
            new Pet(this);
        ...
        /* this.pet is still [Free]*/
    }
}
                

class Pet {
    Pet([Free] Person owner) {
        this.owner = owner;
    }
}
                

Commitment points

Type systems (for nullity or immutability) introduce commitment points

In immutability systems, this means the point at which we will begin enforcing constraints

In nullity systems, this means the point by which the programmer must initialize an object's not-null fields

Putting mutability and nullity together

We want to guarantee immutability as soon as possible

We want to be able to put off initialization until as late as possible

The natural solution is to enforce immutability constraints at the same time as we require the programmer to have fulfilled nullity constraints.

Putting mutability and nullity together

We want to guarantee immutability as soon as possible

We want to be able to put off initialization until as late as possible

Explicit commitment:

"delay the invariants..." (this is like Fähndrich & Haack's systems)

...
delay t { /* Enter an initialization scope, parametrized by t */ 
    neil = new <t> Person[Mutable, NotNull]<,Nullable>;


    peter = new <t> Person[Immutable, NotNull]<,NotNull>;
    tom = new <t> Turtle[Immutable, NotNull]<,>;

    /* Type error: Didn't initialize peter.pet or tom.owner by the end of their initialization scope */
}
            

Explicit commitment:

"delay the invariants..." (this is like Fähndrich & Haack's systems)

...
delay t { /* Enter an initialization scope, parametrized by t */ 
    neil = new <t> Person[Mutable, NotNull]<,Nullable>;


    peter = new <t> Person[Immutable, NotNull]<,NotNull>;
    tom = new <t> Turtle[Immutable, NotNull]<,>;

    /* Can still mutate the Immutable objects peter and tom while we finish their initialization */
    peter.pet = tom; tom.owner = peter;
}
            

Now after initialization:

Explicit commitment:

"delay the invariants..." (this is like Fähndrich & Haack's systems)

...
delay t { /* Enter an initialization scope, parametrized by t */ 
    neil = new <t> Person[Mutable, NotNull]<,Nullable>;


    peter = new <t> Person[Immutable, NotNull]<,NotNull>;
    tom = new <t> Turtle[Immutable, NotNull]<,>;

    /* Can still mutate the Immutable objects peter and tom while we finish their initialization */
    peter.pet = tom; tom.owner = peter;
}
            

Now after initialization:

/* Type error: neil is Mutable, and expects his pet to be...*/
neil.pet = tom;
            

Explicit commitment:

"delay the invariants..." (this is like Fähndrich & Haack's systems)

...
delay t { /* Enter an initialization scope, parametrized by t */ 
    neil = new <t> Person[Mutable, NotNull]<,Nullable>;


    peter = new <t> Person[Immutable, NotNull]<,NotNull>;
    tom = new <t> Turtle[Immutable, NotNull]<,>;

    /* Can still mutate the Immutable objects peter and tom while we finish their initialization */
    peter.pet = tom; tom.owner = peter;
}
            

Now after initialization:

/* This is okay though: neil is Mutable, neil.pet can be null */
neil.pet = null;
            

Explicit commitment:

"delay the invariants..." (this is like Fähndrich & Haack's systems)

...
delay t { /* Enter an initialization scope, parametrized by t */ 
    neil = new <t> Person[Mutable, NotNull]<,Nullable>;


    peter = new <t> Person[Immutable, NotNull]<,NotNull>;
    tom = new <t> Turtle[Immutable, NotNull]<,>;

    /* Can still mutate the Immutable objects peter and tom while we finish their initialization */
    peter.pet = tom; tom.owner = peter;
}
            

Now after initialization:

/* Type error: peter is Immutable: no field assignment please! */
peter.pet = ...
peter.pet.owner = ...
            

Explicit commitment:

"delay the invariants..." (this is like Fähndrich & Haack's systems)

...
delay t { /* Enter an initialization scope, parametrized by t */ 
    neil = new <t> Person[Mutable, NotNull]<,Nullable>;


    peter = new <t> Person[Immutable, NotNull]<,NotNull>;
    tom = new <t> Turtle[Immutable, NotNull]<,>;

    /* Can still mutate the Immutable objects peter and tom while we finish their initialization */
    peter.pet = tom; tom.owner = peter;
}
            

Now after initialization:

/* Type error: tom is Immutable */
tom.owner = ...

            

Something totally new: Generic Nullity

What do we gain?

Genericity! (of course)

We can make this more concrete...

What do we gain?

Genericity! (of course)

class List[i]<,n1> {
    /* The nullity of next is parametrized */
    next : List[i,n1]<,n1>
    ...
    void add, get, ...
}
            

What do we gain?

Genericity! (of course)

class List[i]<,n1> {
    /* The nullity of next is parametrized */
    next : List[i,n1]<,n1>
    ...
    void add, get, ...
}
            

delay t {
    /* Just a normal recursive list */ 
    normal = new <t> List[Mutable,NotNull]<,Nullable>
}
normal.add(...); normal.get(...); ...
            

What do we gain?

class List[i]<,n1> {
    /* The nullity of next is parametrized */
    next : List[i,n1]<,n1>
    ...
    void add(List[Mutable, NotNull]<,n1> this, ...) {
        ...
    }
}
            

delay t {
    /* Just a normal recursive list */ 
    normal = new <t> List[Mutable,NotNull]<,Nullable>
}
normal.add(...); normal.get(...); ...
            

What do we gain?

class List[i]<,n1> {
    /* The nullity of next is parametrized */
    next : List[i,n1]<,n1>
    ...
    void add(List[Mutable, NotNull]<,n1> this, ...) {
        ...
    }
}
            

delay t {
    cycliclist = new <t> List[Mutable,NotNull]<,NotNull>
    /* Type error! Cycles are enforced by the type system*/
}
            

What do we gain?

class List[i]<,n1> {
    /* The nullity of next is parametrized */
    next : List[i,n1]<,n1>
    ...
    void add(List[Mutable, NotNull]<,n1> this, ...) {
        ...
    }
}
            

delay t {
    cycliclist = new <t> List[Mutable,NotNull]<,NotNull>
    cycliclist.next = cycliclist;
}
cycliclist.add(...); cycliclist.get(...); ...
            

What do we gain?

class List[i]<,n1> {
    /* The nullity of next is parametrized */
    next : List[i,n1]<,n1>
    ...
    void add(List[Mutable, NotNull]<,n1> this, ...) {
        ...
    }
}
            

delay t {
    immutcycliclist = new <t> List[Immutable,NotNull]<,NotNull>
    cycliclist.next = cycliclist;
}
/* Type error! add expects a mutable list! */
immutcycliclist.add(...);
            

What do we gain?

class List[i]<,n1> {
    /* The nullity of next is parametrized */
    next : List[i,n1]<,n1>
    ...
    void get(List[i, NotNull]<,n1> this, ...) {
        ...
    }
}
            

delay t {
    immutcycliclist = new <t> List[Immutable,NotNull]<,NotNull>
    cycliclist.next = cycliclist;
}
/* Notice get is still fine... */
immutcycliclist.get(...); 
            

Generic Nullity

NotNull will not do in place of Nullable

(or, sometimes it won't do...)

In other systems for nullity this is fine

(this is a new problem for generic nullity)

Nullity parameters are not covariant

I say that I expect you to pass me either a cat or nothing:

void stroke(..., Cat[Immutable, Nullable]<,> cat, ...) {
    ...
}
            

(but I promise not to change it...)

It's fine if you pass me a cat that you definitely know is a cat!

Nullity parameters are not covariant

I say that I expect (definitely) a box that might contain a cat:

void quantum_box(..., Box[Mutable, NotNull]<,Nullable> box, ...) {
    ...
}
            

class Box[i]<,n1> {
    Cat[Mutable, n1]<,> cat;
}




            

delay t {
    box = new <t> 
        Box[Mutable, NotNull]<,NotNull>;
    box.cat = new <t> 
        Cat[Mutable, NotNull]<,>;
}
quantum_box(..., box, ...);
            

Nullity parameters are not covariant

It's not fine for you to pass me a box that you know definitely has a cat in it!

void quantum_box(..., Box[Mutable, NotNull]<,Nullable> box, ...) {
    /* Fine, since I see the box as having a Nullable cat */
    box.cat = null;
}
            

delay t {
    box = new <t> Box[Mutable, NotNull]<,NotNull>;
    box.cat = new <t> Cat[Mutable, NotNull]<,>;
}
quantum_box(..., box, ...);
                

Nullity parameters are not covariant

It's not fine for you to pass me a box that you know definitely has a cat in it!

void quantum_box(..., Box[Mutable, NotNull]<,Nullable> box, ...) {
    /* Fine, since I see the box as having a Nullable cat */
    box.cat = null;
}
            

delay t {
    box = new <t> Box[Mutable, NotNull]<,NotNull>;
    box.cat = new <t> Cat[Mutable, NotNull]<,>;
}
quantum_box(..., box, ...);
/* We expect box.cat to be NotNull! */ 
box.cat = ...?
                

Nullity parameters are not covariant

So while nullity of the reference itself is covariant, treating the parameters in the same way is not sound.

We create a least upper bound (<? extends Nullable>)

C[Immutable, NotNull]<,> /* can be used for */ C[Immutable, Nullable]<,>

C[Immutable, NotNull]<,NotNull> /* can't be used for */ C[Immutable, NotNull]<,Nullable>
                

Nullity parameters are not covariant

So while nullity of the reference itself is covariant, treating the parameters in the same way is not sound.

We create a least upper bound (<? extends Nullable>)

C[Immutable, NotNull]<,Nullable> /* can be used for */ C[Immutable, NotNull]<,<? extends Nullable>>

C[Immutable, NotNull]<,NotNull>/* can be used for */ C[Immutable, NotNull]<,<? extends Nullable>>
                

Nullity parameters are not covariant

So while nullity of the reference itself is covariant, treating the parameters in the same way is not sound.

We create a least upper bound (<? extends Nullable>)

C[Immutable, NotNull]<,> /* can be used for */ C[<? extends ReadOnly>, Nullable]<,>

C[Mutable, NotNull]<,> /* can be used for */ C[<? extends ReadOnly>, Nullable]<,>
                

Now let's talk about the formal system

I promised a simple runtime

I promised a simple runtime

The runtime semantics...

Runtime semantics are exactly how you'd imagine;

Judgements look like:

Typing judgements are a little more complex

So far everything is simple

But the tricky part of the project is developing the type rules

They're a bit more involved...

Typing judgements...

When an object is committed:

Typing judgements...

When an object is committed:

delay t {
    box = new <t> 
        Box[Immutable,NotNull]
            <,Nullable>
}
/* Type Error! box.cat isn't typed NotNull! */
box.cat.fur
                

Typing judgements...

When an object is committed:

delay t {
    box = new <t> 
        Box[Immutable,NotNull]
            <,NotNull>
}
/* This is fine */
box.cat.fur
                

Typing judgements...

When it's not committed, things are a bit more involved...

Typing judgements...

When it's not committed and the field is listed as uninitialized, the returned value might be null!

Typing judgements...

Typing judgements... (FieldType(...))

• Can't have < ? extends ReadOnly>
• or < ? extends Nullable>
• anywhere in the type

These types mean "we don't know"; they exist as upper bounds on other possibilities

Now let's discuss soundness

In terms of paths through the heap

Defining a well-formed heap...

This is hard to show

Paths through the heap

Field assignment

Field assignment

Field assignment

Field assignment

Evaluation

We saw at the start that we were able to expressively type data-structures and perform non-trivial initialization

We can also initialize e.g. arbitrarily sized cyclic structures without any problems

Paths typed as NotNull will not evaluate to null

Paths typed as Immutable will not have Mutable aliases

The soundness arguments presented in the report were incomplete:

• Did not formalize method call
• Made some (probably reasonable) assumptions (e.g. generation lemma)

Challenges

• Covariance (nullity and mutability)
• Commitment points (seems simple now)
• Keeping track of time (how to track future commitment points, passed between methods)

The result is...

an expressive type system for generic mutability and nullity in an object-oriented system, with flexible initialization.

There's still work to be done: e.g. we have the basic argument for method call, but I'd like to finish this off!

Maybe then I'll write a compiler...

The important bits:

• First time nullity has had a full generic treatment (found some interesting "gotchas").
• No erasable state / extra runtime constructs required to express and argue soundness
• Exploration of the cross-over between two concepts which both concern initialization

Questions?