ajs@prg.ox.ac.uk (Adolfo Socorro) (10/23/90)
In article <668@caliban.mrcu> Tony Clark remarks that the rules in Eiffel
concerning the redefinition of signatures make the type system unsafe. I agree
with this. The rule he proposes is called ``contra-variance'' by some, and
implemented in a few languages, like Trellis/Owl (articles in various
OOPSLAs). Contra-variance, unfortunately, limits expressiveness. Note,
however, that preconditions in Eiffel are required to observe this ``reverse''
behaviour. (Why, then, wasn't contra-variance adopted in Eiffel?)
I guess the choice of one rule of signature compatibility over the other
depends on whether you want absolute type security (required for the
implementation of so-called ``safety-critical systems''), or flexibility in
defining a class hierarchy.
A MUST article by Peter Wegner and Stanley Zdonik called ``Inheritance as an
Incremental Modification Mechanism'' (ECOOP 87), explores the different kinds
of redefinition possible with inheritance and their impact on the type-safety
of systems. They argue at one point that it is the ``subset relation rather
than the subtype relation that corresponds to the classical is-a relation'',
and that the fact that an A is always a B is in many contexts more important
than the fact that certain operations on As are inappropriate when performed
on Bs. Substitutability implies indistinguishability and is often
unreasonable.
Adolfo Socorro bertrand@eiffel.UUCP (Bertrand Meyer) (10/24/90)
From <752@culhua.prg.ox.ac.uk> by ajs@prg.ox.ac.uk (Adolfo Socorro): > In article <668@caliban.mrcu> Tony Clark remarks that the rules in Eiffel > concerning the redefinition of signatures make the type system unsafe. > [...] Note, however, that preconditions in Eiffel are required to observe > this ``reverse'' behaviour. > (Why, then, wasn't contra-variance adopted in Eiffel?) I certainly disagree with Mr. Socorro that the covariance rules (which most people, when confronted with actual examples, will agree are the only practical ones, e.g. to write a good data structure class library) make the type system unsafe. They simply make typing more difficult to explain and type checking more difficult to implement. (This argument will of course carry much more strength when our compiler does catch the type error cases that it currently misses. Keep posted.) [Anyone new to the discussion may want to look at the archive of this newsgroup, where the typing question has been amply discussed, although the last word certainly remains to be said.] Mr. Socorro's comment about preconditions is correct: one can consider the weakening rule as a form of contravariance. Here is how the apparent contradiction can be justified: 1 - Covariance is often the desirable property. This is true for types, as mentioned above; in practice it is often true for preconditions as well (when a new, better algorithm will work under more restrictive conditions). 2 - The key difference, however, is that a type system with covariance rules yields a language that can still be type-checked statically (although less trivially than with contravariance, as mentioned above). This is the justification for using a type system based on covariance: make it easy on application programmers, even if it means complicating the compiler writer's job. With contravariance, type checking is a piece of cake for the compiler writer, but the expressive powers of application programmers are severely limited. 3 - For preconditions, nothing could be checked statically without the weakening rule. For anyone who forgot the reason for this rule, it is quite simple: if a client calls x.r (...) in a context that ensures the precondition of r, the client must be guaranteed a correct result (this is part of the contract theory of software construction). But if x is polymorphic and r is redefined in a descendant class, this will only be the case if the new version's precondition is no stronger than the original precondition. 4 - In cases in which the weakening rule appears to restrictive, there is an easy way out, based on the following important observation: all that matters in the contract theory is to enable the client to guarantee that the call will succeed. This is the role of the precondition. Two schemes that ensure this are if x.pre then x.r (...) else ... and x.s (...); x.r (...) where the postcondition of s implies the precondition of r (called pre in the first form). But in either case THE PRECONDITION CAN BE ABSTRACT: for example pre could be a function of the class, which may be redefined freely along with r and s. Then both schemes remain valid. This is not a trick but a perfectly valid refinement technique (frequently used in the Basic Libraries). Remember, all that matters is to give the client ``its money's worth'', that is to say, a precise statement of what the client has to do to get the results of the contract (the postcondition). -- Bertrand Meyer bertrand@eiffel.com