Re: Clean Object Class Design -- Circle/Ellipse

From: Marc Gluch <marc.gluch_at_mindtap.com>
Date: Sun, 12 Aug 2001 16:58:17 GMT
Message-ID: <3b769e09.3207460634_at_news.grpvine1.tx.home.com>


On Mon, 6 Aug 2001 23:32:20 -0400,
 "peter_douglass" <baisly_at_gis.net> wrote:

>Marc,
> I'm having difficulty following your argument.
 <big snip>
> Any help clarifying this would be appreciated.

Peter,

Since you asked politely, I feel an obligation to respond in kind. However, I had to balance that obligation against my family and work obligations. Consequently I had to postpone my reply until the weekend (BTW, where are you vacationing?).

I understand that you may have felt ignored and (consequently) frustrated.

I will try to address the concerns you raised in the post that I am responding to, as well as thw next two of your subsequent posts (but may temporarily run out ofd time).

Before I get to specifics, I think that future discussion will benefit from some consideration of general questions regarding types.

In "A History of CLU", Barbara Liskov describes *abstract type* as: "a group of related functions whose joint actions completely define the abstraction as far as the users are concerned. The irrelevant details of how the abstraction is supported are completely hidden from the users.
Furthermore, the language should support a syntactic unit that can be used to implement abstract types, and the language must be strongly typed so that it is not possible to make use of an object in any other way except by calling its operations."

Note that this definition has a category-theoretic flavour a lot more than set-theoretic. There is no concern about type inhabitation. Instead, the focus is on the arrows (functions) and their properties (axioms) that define the abstraction.
The primary concern is that the axioms be preserved under composition (writing programs is composing new functions from the base ones (primitives) and other, previously defined ones). IOW, type definitions are intensional (specification), not extensional (implementation).

Now we can consider a notion of subtype.

If we have two sets with different cardinalities that inhabitate a particular abstract type, then both sets are valid *implementations" of the same abstract type. We can only observe that one implementation (the set of lesser cardinality) is "more efficient" than the other one (the elements of the smaller set are equivalence classes of the other set).

In order to define the *subtype* relationship we have to consider at least two abstract types with the same "base" operations, but different axiomatizations of these operations. Furthermore, while the abstract types are defined intensionally, we'd like the definition of subtype to be consistent with the extensional definition of subset, so that our theories have well-behaved models.

Definition 1 (Gluch)
S is a subtype of T iff S has all axioms of T plus some additional one(s).
Comments:
a) the two axiomatizations are consistent, otherwise the added constraint is not an axiom
b) I have no idea if someone proposed such definition before me

Definition 2
S is a subtype of T iff S has less axioms than T.

Definition 3 (Liskov)
S is a subtype of T iff for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms ofT, the behaviour of P is unchanged when o1 is substituted for o2 .

Definition 4 (Date -- per his Circle/Elipse article on dbdebunk.com) S is a subtype of T iff Inhabitant(S) is a subset of Inhabitant(T).

Definition 5 (Peter Douglas)
S is a subtype of T when (iff?) we know the conditions for asserting whether a given object x is of type S and we know the conditions for asserting when two objects are equal within that type, AND we have 2 functions. One function takes a proof of the judgement x is object of type S and returns a proof of the judgement x is an object of type T. The other function takes a proof of the judgement that x and y are equal under type S and returns a proof of the judgement that x and y are equal under type T.

Analysis
All definitions are (self) consistent. Which one to choose is a question of utility (practical benefits) of each definition.

Definition 1.
The addition of more axioms (constraints) may eliminate some inhabitants of T, and make Inhabitant(S) a subset of Inhabitant(T), but as long as the new set of axioms is consistent, we can substitute inhabitants of S for expressions in T.
Consider a definition of Integers as such Rationals that r = floor(r). The new axiom is inconsistent with the original axioms, therefore Integers are not a subtype of Rationals. However, (assuming common axiomatization as fields) Rationals are a subtype of Reals, and further a subtype of Complex numbers.

IOW, Specialization by Constraint can produce a "well behaved" subtype (if the constraint is an axiom independent of the original set of axioms of the supertype).

The utility of such subtype definition lies in the efficiency gained by specialized implementations of the base operations in the subtypes, combined with type safety. We get specification reuse (since the subtype extends the supertype's specification) and code reuse (ability to use all functions/programs defined in T, except the specialized primitives).

Definition 2.
Clearly every statement valid in S is also valid in T, so we can substitute inhabitants of S for expressions in T. But if Inhabinant(S) is a superset of Inhabitant(T), can we pass these additional inhabitants of S to functions written in T? Sure. We redefine in S the promitives defined in T, so any composite function defined in T will use subtype definitions  when it deals with inhabitants of S.

Practical utility is debatable (we get most but not full specification reuse). We do get code reuse.

According to this definition Rationals are a subtype of Integers (so are Reals and Complex). This seems counter-intuitive.  What's the problem?
This definition is a definition of generalization. We are building super-theories instead of sub-theories. I have a feeling (though I haven't thought it through) that this definition is equivalent to lambda abstraction.

In (mathematical) reality, that Date likes so much, Rationals can be a *derived* type, but its' not a derivation through specialization, but rather through composition (cartesian product). I've included this definition in my analysis, because I've seen plenty of people trying to inherit 3D points from 2D points, or Rectanges from Squares.

Definition 2 is obviously in conflict with definition 1 (inverse order), so one has to choose between them.

Definition 3 (Liskov)
How does one go about proving the if part? Inspect *all* programs written in T?
Fortunately, Liskov has restated LSP as: "S is a subtype of T iff any property proved about inhabitants of T also holds for inhabitants of S".
She also provides two definitions of subtype relationship such that: "one can prove whether a subtype relationship holds by proving a small number of simple lemmas based on the specifications of the two types".

This definition appears similar to definition 1. Again, its utility lies in ability to use all composite functions defined in T. See www.cs.cmu.edu/afs/cs.cmu.edu/project/venari/www/subtype-tr.html for details.

Definition 4 (Date)
Peter wrote:
>By his (Date's) definition, the type Integer is a subtype of
>the type Rational. To undermine this very clear position,
>one would need to show that

 <snip>
>b) that even if internally consistant, it leads to unacceptable practical problems.
We can pass inhabitants of S as parameters to functions defined in T (whether primitive or composite), but we don't know what to do with the return values.
Even if we override the primitives of the supertype in the subtype, we can't use all programs written in T and expect the results to inhabitate the subtype (IOW, we can't "inherit" any functions defined in the supertype).

This yields definition 4 useless for programming with types (again, it may be useful in the database world), since we can't draw any benefits (such as specification or code reuse) from two types being in the the subtype relationship.

Specifically, even if we override rational + and * as integer + and *, we can't call all Rational functions defined in terms of + and * (Rational programs) with integer parameters and expect to get an integer result. Witness average(1, 2).
We can't even decide which programs we can reuse -- based on *their* specifications alone. We have to go into program implementations to see if the computation makes any use of the existence of the multiplicative inverse, and how that use affects the result.

Definition 5.
Peter writes:
> Integer is a subtype of Rational. Witness the following two functions.
>Take a proof that X is an integer and append the phrase "or there exists a
>non-zero integer Y such that multiplying X by Y yields an integer". Take a
>proof that X and Y are equal Integers and append the phrase "or there exists
>non-zero integers M and N such that (X*M) and (Y*N) are equal integers.
You just proved that 2 = 1/2 , for M = 1 and N = 4 (sorry, I couldn't help myself).
I guess defining appropriate two functions is not a trivial task. I believe your definition reduces to Date's. You can prove that Integers are a subset of Rationals, but the utility of that proof is limited, since you can't pass integer parameters to rational functions and expect an integer result.

Conclusion
My answer to the circle/elipse question is -- show me the specs so I can make a judgement.

This whole analysis could have been avoided if we notice that abstract types don't have extent (abstract classes can't be instantiated). As soon as we consider two concrete types, we have inconsistent axiomatizations (the additions to their common abstract supertype axiomatization are the two respective *representations*). However this is as it should be.

Furthermore, the abstract supertype can establish conversion axioms, so that any concrete subtype can safely use all functions defined in the abstract supertype without worrying about yielding incorrect (out of type) results.

I wonder how my definition relates to:
John C. Reynolds, "Polymorphism is not set-theoretic", LNCS 173, 1984, but don't have the access to the content of the article.

Note that polymorphism *can* be set theoretic in specific instances, when the axiomatizations are consistent and the representations are transparent. That's was the case in the example of Rationals, Reals and Complex presented in the analysis of Definition 1.

By now my family obligations are back on top of the stack.

TTYL, Marc Gluch
Mindtap Inc. Received on Sun Aug 12 2001 - 18:58:17 CEST

Original text of this message