Grace After Splash

We had a productive meeting at the SPLASH conference last month – but then as often seems to be the case, ended up in various teaching and admin tasks once we got back.

The Grace BOF before the start of the conference proper was well attended, with a robust discussion on language principles, features, and syntax. We also managed to catch up with some of our supporters during conference sessions, in particular regarding concurrency support, and general ambiguity of language design.

The Grace Design workshop was held at Portland State – Yossi Gil, Daniel Zimmerman, Brian Foote and Dave Ungar were kind enough to share their expertise. We talked a lot about the big things: objects vs classes vs generics vs types, and certainly gained some confidence that the design would hold together. Towards the end we also covered a number of secondary topics quickly: annotations, reflection & meta-objects, assertions, type brands, and type-safe builder notations — and it seems most of our sketched ideas about how to address these points held up so far.

And finally, Microsoft Channel9’s Charles Torre interviewed Andrew and James about Grace along with many other interesting people at SPLASH.

We’re making progress finishing the first cut of the whole language design, but it’s fair to say our efforts at documentation are a little behind or efforts in design. But there should be more details soon.

Type Conformance in Grace

Following from comments on the variance post, here’s an attempt at explaining the rules for type conformance in Grace.

In Grace, we say “type B conforms to another type A” when every object of type B can be supplied whenever an object of type A is expected. B conforms to A is written B <: A; or we may say B is a subtype of A or A is a supertype of B. I’ll try and stick to “conforms to” because hopefully it is the least confusing.

Now – what does “B conforms to A” mean? In other words, given two types A and B, when can we say that we know that “B conforms to A”?

In Grace there are three rules, and only the last one is sometimes difficult. The key idea is that if B conforms to A, or B can be supplied whenever an A is required, then every request for a method that is valid on an A must also be acceptable on a B. The rules are:

  1. B must respond to every method request that A responds to
  2. The types of the results returned by B’s messages must conform to the types of the results returned by A’s messages
  3. The types of the formal parameters expected by A’s messages must conform to the types of the formal parameters expected by B’s messages

If you’ve survived this far, the first rule is, I hope, noncontroversial. If A responds to some method “m”, then B must also respond to that method. The second rule, too, hopefully makes sense: if calling “m” on A returns some other type C, then calling “m” on B must return a C, or rather something that is acceptable when C is required — something that conforms to C.

The third rule is the tricky case: what it says is that if method m on A expects a formal parameter of type D, method m on B must also work if a D is supplied or it can accept more objects than A — methods on B can be less selective than A, but they cannot be more selective. This rule seems backwards to the other two rules, which is where the “contra” comes from.

Let’s try a more concrete example. Say I have a Pet type like this:

type Pet = {
sleeps -> Boolean
eats(f : PetFood) -> Unit // doesn’t return anything
}

I want to make a Cat class that conforms to the Pet type — what does that say about the Cat class’s interface? Well by rule 1, the Cat class has to have to have all the methods included in the Pet type — “sleeps” and “eats” — although it may have more — “purrs” say. I say by rule 1, but really it will be required by the design: if part of the program needs an object meeting the Pet interface, then presumably the sleeps and eats methods will be requested on that object.

Considering rule two, the methods can return the same or more specific types – if my cat sleeps all the time, I could make a “sleeps’ method that returns “true” and it would still conform to the Pet type. Again this comes from the design of the program — some code presumably calls the sleeps method and expects to get a Boolean in return.

Then finally rule three: argument types: the Cat class has to have an “eats” method that accepts PetFood. Again presumably this is because a program that uses the Pet type will feed that Pet some PetFood. What this means is that we can’t make our Cat class fussier than any other kind of Pet. A Cat that insisted on CatFood rather than PetFood, or GourmetCatExtreme rather than anything else, wouldn’t conform to the Pet interface. On the other hand, a Cat that is less choosy, a Cat that is happy to eat DogFood, or Chicken, or any kind of Food, will conform to the Pet interface.

So the type of a Cat would look alike this:

type CatType = {
sleeps -> Boolean
eats(f : PetFood) -> Unit //Doesn’t return anything
purrs -> Unit //Doesn’t return anything either
}

and we would be able to say Cat <: Pet.