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.

6 thoughts on “Type Conformance in Grace

  1. still pondering and trying to let it all sink in to the point where i can explain it to somebody else without looking at crib notes, i’m slow. but many thanks for expanding on the subject matter.

  2. p.s. i think Meyer’s Design By Contract talks about the same thing in terms of tightening or loosening the pre or post conditions, and in some ways that either makes more sense to me, or at least offers another take on it in addition to the co/contra variance words like you have here and like i’ve seen for java, scala, et. al., and having more than one take on the same idea helps me begin to ah hah a little.

  3. a few questions i had along the way of reading that. i’m not saying i haven’t figured out the answers to all of them, but that slow folks like me appreciate it when you can really show how the ends tie together.
    (a) how does this directly relate to your previous post about the set() call?
    (b) you say “or Chicken” etc. but natural language sucks, so that could read like Cat.eats(Chicken) which presumably also is a no-no. i’m not sure what better english to use. maybe don’t say that part, but instead say that it has to take something more general / less specific than cat food, like just simply Food.
    (c) so i think the final example code should be something like Cat.eats(f:Food) to show the contravariance?

  4. p.p.s. i like your Cat.set() example overall vs. the others i’ve read about this topic matter. it helps me grok the whole Collection.set() thing better.

    i think part of the trickyness for people struggling with it all can also be the static vs. dynamic type checking times. like i can send Cat.eats(new Chicken()) and it works just fine, i just can’t make the static API of Cat.eats() be only Chicken.

    and then if we’re talking about how to grok it in (i shudder, but it *is* my day job) things like Java with generics and erasure and arrays vs. collections and all that jazz, then all bets are off again! which is probably one of the things that has led you to try to come up with Grace. but it means i might grok it here and then go do java and get confused again and then come back to Grace and fail to swap out the java badness and then be all screwed up in Grace or whatever other sane programming language e.g. scala (ok i use the word ‘sane’ very lightly there) i then try to use.

    [i think i should be able to shut up now, btw. :-]

  5. Hi Raoul – this is all good stuff. Answering your questions:

    (b) you say “or Chicken” etc. but natural language sucks, so that could read like Cat.eats(Chicken) which presumably also is a no-no. i’m not sure what better english to use. maybe don’t say that part, but instead say that it has to take something more general / less specific than cat food, like just simply Food.

    yes, you’re right there.

    (c) so i think the final example code should be something like Cat.eats(f:Food) to show the contravariance?

    Indeed! If you’ve got that, you’ve got the idea.

    (a) how does this directly relate to your previous post about the set() call?

    So: the underlying rules don’t change for collections or anything else – in Grace there are no wildcards, variance annotations, erasure etc. There’s just the fact that a mutable collection of Pets will have the type:

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

    and a mutable collections of Cats have the type

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

    and neither of these types are the subtype of each other…

  6. Good Morning, All,

    First, let me applaud you for your efforts to create a new standard for a teaching programming language — Haskell is good but certainly not for the n00b.

    That said, let me say that as a 20+ year professional programmer who has always sought a better way to express program logic, I have always been very put off by language examples that use non-realistic models, such as the ubiquitous ‘Cars’ and ‘Animals’ object hierarchies.

    May I very humbly suggest that perhaps you should put a little strategy together about the kinds of examples you will use. Computer Science has done so horribly in attacking real-world problems, such as file types and their handlers and file system navigation in general, that perhaps you can whet the students’ appetites for learning by giving them insight into how such real-world situations can be modeled and why, perhaps, such problems are actually difficult.

    But, please, I think that you should very seriously consider leaving the ‘Cars’ and ‘Animals’ for non-serious endeavors. And, BTW, by thinking of how to demonstrate/discuss the features of Grace (great name, BTW) beforehand, it would also be somewhat in line with what is turning out to be a useful program development process methodology: TDD.

    In any event, I apologize for being a bit orthogonal to this exact discussion, but seeing as how you are young in this endeavor, I thought it an opportunity to give a bit of perspective from a seeker of ‘the Ultimate Language’. I wish you all great success!

    Sincerely,
    Robert McCall
    Lasting peace and happiness for *ALL* human beings.

Leave a Reply

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