Variance and Structural Types

Variance is a sticky topic in programming language design. Here’s why variance is a problem, and how Grace will address it.

Consider a generic Sequence interface:

type Sequence<E> = {
   get(Number) -> E
   count -> Number
}

We can instantiate this sequence to make a list of objects (Sequence<Object>) or a list of books (Sequence<Book>). Assuming the Book type conforms to the Object type (Book <: Object) what is the relationship between these the two types of list?

In Grace, typing is structural, that is, we look at the structure of the types to decide, not (just) their declarations. The type Sequence<Object> expands to:

type Sequence<Object> = {
   get(Number) -> Object
   count -> Number
}

by replacing the parameter E with Object. Similarly a Sequence<Book> has the interface:

type Sequence<Book> = {
   get(Number) -> Book
   count -> Number
}

Now consider the method requests in both interfaces. The count request is the easiest — it’s exactly the same in both. The get method returns an Object in Sequence<Object> and a Book in Sequence<Book> — hopefully as we’d expect. Because the return types the book sequence requests are equal to or conform to the return types of the object sequence requests, Grace’s type system allows a sequence of books to be provided whenever sequence of objects is required: that is

Sequence<Book> <: Sequence<Object>.

So far so good. The trouble is, the Sequence type only lets you get things out of the list, not put them in. For that, we need an interface like the actual List interface:

type List<E;> = {
   get(Number) -> E
   add(Number, E)
   count -> Number
}

By comparing their expansions, Grace can show that, for any E, every List<E> <: Sequence<E> — whenever Grace needs a Sequence of something, you can give it a List of the same things. Fair enough, because any method requiring a Sequence isn’t going to use the add method, or they’d have to require a List instead.

The tricky question is: what’s the relationship between List<Book> and List<Object>? The expansion starts the same as for Sequence, but now we have “{ add(Number, Object) } ” in List<Object> and “{ add(Number, Book) }” in List<Book> — we can add anything to a List of Objects, but can only add Books to a list of Books. Considering the types of just the add methods, we must have this relationship:

{ add(Number, Object) } <: { add(Number, Book) }

a method requiring an Object argument is a subtype of a message requireing a Book argument! This is called contravariance because the methods vary in the opposite order to the types of their arguments.
In fact, the situation for Lists is even worse, because the get method is covariant — this is what lets the Sequence of Books be a subtype of the Sequence of Objects. So there is no subtype relationship in either direction between List<Book> and List<Object>.

All this Co/Contra/Bi/In/variance is quite confusing, which is why Eiffel and Dart use a covariant rule for everything, and insert dynamic checks that can fail at runtime. Java, Scala, C# provide wildcards and variance annotations to handle: the methods you are permitted to call depend on how the argument types are used.

Grace’s structrural types don’t need variance annotations, and we don’t plan to add them. (O’CAML also uses structural types, I’m not sure why it also has variannce annotations). In Grace, you can always write down whatever type you need when you need it, and you can use partially or completely dynamic types if you want to reply on dyanmic checking. If you don’t care, you can write

def listOfBooks : Dynamic := List<Object>.new

to say you explicitly don’t care about the type of this list. (Of course, this means that listOfBooks could now hold anything). If you at least want to be sure you have a list, but don’t mind what goes in or out, you can write:

def listOfBooks : List<Dynamic> := List<Object>.new

and that’s what you get: Eiffel or Dart style dynamic checking on what goes in or out of the list, and static checking of the list operations themselves.

If you’re sure you only want to read things out of a list of books, (or perhaps a list of some other things) then make the type a Sequence of objects: any kind of list can go in here, but you can’t add things to the box — because random objects won’t fit into a list of Books.

def listOfBooks : Sequence<Object> := List<Book>.new

But say (if you’re packing up your house) and you want a list you can put books (in to) perhaps just a list of books, perhaps a list of anything else, you can write a structural type that says just what you want:

def listOfBooks : { add(Book) } := List<Object>.new

And any list (or anyting else) to which a book can be added to will be compatible with that type.


Java variance is one of the things I’ve always found hard to teach: tangling together the underlying mathematical regularities (you can put a book into a box of anything, but you can only put books into a box of books) and the language features. It’s been interesting trying to explain this in Grace. Hopefully the types capture the underlying regularities, and the language offers engineering tradeoffs for programmers to make.

The basic principles of Grace’s type system — that types describe the structure of objects’ interfaces; that programmers can always write any type at any time; that type Dynamic gives run-time typing when and where you want it — hopefully add up to an understandable system that’s not too hard to learn and to use.

Structural types seem to be the key here: if a type isn’t in a library, structural typing means you can always write it down. Java and Scala’s nominal type systems need wildcards to say “which methods to leave out” of an existing type: programmers can’t usefully define new interfaces because, even if they do, the library classes won’t implement them.

The examples also show my current thinking about Collections for Grace. Following Clu the library will have both read-only (covariant) and read-write (invariant) interfaces for the main collection classes. Generally the read-only interface will have a more “mathematical” name (Bag; Set; Sequence; Map) and the read-write interface a more “pragmatic: name (Collection; List; Dictionary). I’m assuming the contravarint (write only) interface will be rarely used: programmers can write it as necessary — or perhaps even construct it by type subtraction or type division. And yes, I’d like to abbreviate “Sequence” to “Seq” or find another good three letter name!

5 thoughts on “Variance and Structural Types

  1. But wouldn’t it be more useful to have immutable vs. mutable collections? The line

    def listOfBooks : Sequence := List.new

    indicates that Sequence is indeed just read-only, not immutable.

  2. wouldn’t it be more useful to have immutable vs. mutable collections?

    Sure – and I expect to have both in the library. We haven’t started in on the library design properly, but I’d expect to have immutable and mutable collections — probably named for their data structure. So a HashMap and an ArraySet will be immutable, but a HashDictionary or an ArrayList would be mutable.

    … assuming you have aliasing in the language.

    We’re OO – of course we have aliasing! Uniqueness annotations, or ownership annotations should be able to be layered over the core language.

  3. > Considering the types of just the add methods, we must have this relationship:
    > { add(Number, Object) } <: { add(Number, Book) }

    man your post was such a tease. i thought it was my chance to totally once and for all completely grok variance!

    but then this is the kind of leap that dumb joes like me get frustrated with. you even made the word "must" be bold i think, but just shouting louder doesn't actually explain things any better to somebody who doesn't already get it.

    in other words, i think that part of the post would be better if you'd defined what it means to be a subtype and why that ordering is what *must* be done here. which i didn't glean really at all from reading the post.

    maybe at least a hyperlink out to something which tries to explain it more? or better? not that i've found the best explanation anywhere. partly it is because the terminology is all screwed up across languages. in one place they say that arrays are covariant and in another they say no they are contravariant, because it entirely depends on what the f the api is for array. so all in all oy veh.

    end-of-rant 🙂

  4. Hi Raoul – fair enough! Thanks for your comments — the definition of a subtype is in their but it’s in passing, it certainly isn’t explicit.

    So, I tried to write a short explanation, but it turned into a post on its own

    Hopefully if you read that one, this one might make more sense.

Leave a Reply

Your email address will not be published. Required fields are marked *