A type system for:
A type system for:
class Person {
Pet pet;
}
class Turtle : Pet {
Person owner;
}
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;
}
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;
*/
}
final
doesn't cut it)
We want to be able to express (and enforce) all of this through the type system.
/* 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;
}
...
/* 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;
}
Type systems for nullity and mutability aren't a new thing.
Type systems for nullity and mutability aren't a new thing.
final
?Type systems for nullity and mutability aren't a new thing.
Ownership Immutability Generic Java (Zibin, Potanin)
Immutable objects can be initialized until the end of their owner's constructor
Support for initializing heterogeneous cyclic structures
Mutability constraints are generic (this is the system on which we model our own)
(but doesn't have to tackle definite assignment)
Type systems for nullity and mutability aren't a new thing.
In systems for each, we have the challenge of initialization
Ownership Immutability Generic Java (Zibin, Potanin)
Immutable objects can be initialized until the end of their owner's constructor
Support for initializing heterogeneous cyclic structures
Mutability constraints are generic (this is the system on which we model our own)
(but doesn't have to tackle definite assignment)
Type systems for nullity and mutability aren't a new thing.
In systems for each, we have the challenge of initialization
class Person {
Person() {
this.pet =
new Pet(this);
...
/* this.pet is still [Free]*/
}
}
class Pet {
Pet([Free] Person owner) {
this.owner = owner;
}
}
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
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.
We want to guarantee immutability as soon as possible
We want to be able to put off initialization until as late as possible
"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 */
}
"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:
"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;
"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;
"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 = ...
"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 = ...
Genericity! (of course)
Can use the same (class) definition in different of ways
This is what we saw with Peter and Neil
We can make this more concrete...
Genericity! (of course)
class List[i]<,n1> {
/* The nullity of next is parametrized */
next : List[i,n1]<,n1>
...
void add, get, ...
}
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(...); ...
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(...); ...
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*/
}
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(...); ...
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(...);
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(...);
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)
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!
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, ...);
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, ...);
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 = ...?
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>
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>>
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]<,>
We just define a standard heap/stack-based runtime.
null
Runtime semantics are exactly how you'd imagine;
Judgements look like:
So far everything is simple
But the tricky part of the project is developing the type rules
They're a bit more involved...
When an object is committed:
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
When an object is committed:
delay t {
box = new <t>
Box[Immutable,NotNull]
<,NotNull>
}
/* This is fine */
box.cat.fur
When it's not committed, things are a bit more involved...
When the field isn't in the list of those that might be uninitialized, do as before, but:
When it's not committed and the field is listed as uninitialized, the returned value might be null!
A lot like field lookup...
But what's that at the bottom?
< ? extends ReadOnly>
< ? extends Nullable>
These types mean "we don't know"
; they exist as upper bounds
on other possibilities
We basically want all the types for these different paths to be in some way compatible.
(what this means is not intuitive)
This is hard to show
We assume all these paths are fine (consistent) to begin with (they are), then have to show that all operations preserve them...
Most cases are trivial induction
But field assignment and method call are not
We basically need to show that:
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:
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: