Typo in the "is a superclass" relation

[kmillikin]

@gbracha In section 10.9 (3rd edition), we have:

It is a compile-time error if a class C is a superclass of itself.

And just above that is the definition of the "is a superclass" relation:

A class S is a superclass of a class C iff either: • S is the superclass of C, or • S is a superclass of a class S0 and S0 is a superclass of C.

This admits reflexive relations. An implementation that tries to check if C is a superclass of itself using the second case of the definition will get that C is a superclass of itself iff. C is a superclass of itself (by choosing C for the class S0).

We should disallow such compile-time errors unless there is really a transitive chain of "the superclass" from C to C. The second clause should be changed to:

• S is a superclass of a class S0 and S0 is the superclass of C.

[lrhn]

I agree that the change makes everything easier to understand.

I'm not sure the current version is actually wrong.

If you use inductive reasoning, you cannot infer that a class is a superclass of itself unless it actually occurs in the superclass chain of its own declaration - to derive that S is a superclass of C, the proof is a non-empty sequence of X_n is the superclass of X_{n+1} predicates that start with S as X_0 and ends with C as X_{k} (k > 0). The change enforces that the inference tree is a spine, but the provable statements are the same.

(Co-inductively you do get a problem when S0 can be C).

[kmillikin]

It is wrong in the sense that it looks to be defining a relation but it is not a definition (not unique).

I think the intent is that "is a superclass" is the transitive closure of "is the superclass" and the fix is to revise the spec to be explicit.

[lrhn]

I'm not sure what it means for a definition of a relation to not be unique - do you mean that the definition is ambiguous and can be used to define two different relations for the same program?

If treated inductively (as such rules are usually interpreted), and assuming that S0 is (implicitly) existentially quantified, then it does define a single specific relation. That's some assumptions, and it would be better if they were made explicit, but I do believe they are reasonable.

More precisely, the relation being defined is the transitive closure of the "is the superclass of" relation, which is a well-defined relation for any Dart program (each defined class has at most a single superclass).

There may be more than one way to infer that two elements are related, but the rules do uniquely define the "is a superclass of" relation.

[kmillikin]

Sorry, I meant that it does not define a unique relation. I agree that it is trying to define the transitive closure of "is the superclass", which is the least relation satisfying this definition. Perhaps you are right that it should reasonably be assumed.

[eernstg]

We obtain 'the superclass' from a with clause or an extends clause (so they're the base cases for this induction).

In the second item, induction is invoked with both 'S is a superclass of S0' and 'S0 is a superclass of C'. I think the simplest fix would be to invoke induction only once and make the second item 'S is a superclass of a class S0, and S0 is the superclass of C'.

Looking again this is exactly what you just proposed in the chat, @kmilikin, I just didn't notice the + and -. So I support your proposal. ;-)

Here's a CL for it.

[kmillikin]

Fixed in https://github.com/dart-lang/sdk/commit/ba7748302259e47f40e3838c6b7e729539984aa2