Re: Clean Object Class Design -- Circle/Ellipse
Date: Tue, 14 Aug 2001 22:08:35 -0400
Message-ID: <3b7995b9_at_tobjects.newsource.com>
Marc Gluch wrote:
>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.
I understand completely.
> Consequently I had to postpone my reply
>until the weekend (BTW, where are you vacationing?).
Florida, but I'm back now. Went to my step-son's graduation.
>I understand that you may have felt ignored and (consequently)
>frustrated.
not to worry.
>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.
[snip of a very lucid exposition of Liskov's theory]
>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.
I think it is important to keep in mind that elegant as Liskov's theory is, it is only one theory among many. Thus, per Liskov, the subtype relationship might require abstract types. I'm not sure that the same is true for Martin-Lof's theory.
>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).
(actually, rather than putting this theory forward as my own, I was speculating that it was the logical extension of the theory put forward by the authors of _Martin-Lof's theory of types_.)
>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.
[snip]
>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.
Yes we do. They are whatever the return values would be inhabitants of T were passed to the function.
>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).
I agree with the main conclusion, but am confused by the parenthetical remark. In C++ at least, the return type of an inherited method is the same for both parent and child. One can _overload_ a method name to return a different type, but that is something else. I can see that there may be occassions where inheritance of a function where the result type changes, might be useful. However, the type of inheritence that is found in C++ seems to have it's uses as well.
>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.
I really don't see this. I write a general math library, that works with "real" numbers. Then I have occasion to deal with some quantities that I wish to constrain to natural numbers. For example, number of items of a given sort in a shopping basket. My contraint of holding number of items to be a natural number is a data integrity constraint. We don't sell half boxes of cereal, although we do sell bananas by the pound. The constraint reduces the frequency of input errors. On the other hand, it is perfectly legal for me to ask for the average number of boxes of cereal purchased per customer per visit. I get a rational number (or a "real") as a result, but I don't need to write a specific math library that deals with natural numbers, I can "re-use" that. Isn't this "drawing beneifs from two types being in 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.
Why do we need to forbid taking the multiplicative inverse of a non-zero natural number? I would think we would want to do this, and often. Witness average, which involves the multiplicative inverse of the cardinality of the bag we are averaging.
>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).
Oops. Should have been "there exists an integer N such that (X*N) and (Y*N) are equal integers."
>I guess defining appropriate two functions is not a trivial task.
I made it harder than it needs to be ;-( Really though you are right. Constructive math is often not trivial. On the other hand, it is free of those nasty paradoxes that come about when you bind words to things you can't construct. "Let R be the set of all sets that do not contain themselves" might be valid English, but when the dust settles, we really haven't bound anything meaningful to "R".
>I believe your definition reduces to Date's.
Perhaps. I'm not sure though. Consider the set of total functions from {1,2,3} to {4,5}. Call it F. If I have some way to determine whether a function is defined over the set{1,2,3} and its image is a subset of {4,5,6}, and I further have some way to determine whether two functions yield the same results when applied to the values within the domain {1,2,3} then I can asssert that F is a Martin-Lof type (per the paper I cited). Now if I have another set of total functions from {0,1,2,3} to {4,5}, call it G, then I think I can assert under my speculative version of Martin-Lof's theory that G is a subtype of F. I'm not sure this is true of Date's theory, but again, I'm lacking sources at the moment, so it is just a guess.
However, I agree that the two theories are quite similar. That is one of the issues that prompted my jumping into this thread. I don't see the conflict between Martin-Lof's theory and Date's, and I'm not sure if it is just ignorance on my part, or whether your citing of Martin-Lof was a mis-step in your argument against Date.
> 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.
There is no reason why I would expect that I would always get an integer result. I can use rational numbers as arguments to transcendental functions, and get transcendental results. What I fail to see is why yourself, and some other posters, find it so important that the result type change (covariantly) with changes in the argument types. You don't seem to value sub-sets as being sub-types. I'm not sure why. For me, a key value of types is the ability to include specification information within a program, and to have the type-checker reject programs for which the included type specifications do not match the program functionality. Types used in this way are just useful decoration of programs, and may be erased without altering the semantics of the program, which could otherwise be written in an untyped language. Subtyping allows one to avoid duplication of type specifications. If a type can be constructed by declaring it to be a subtype of multiple different types, it would seem to add additional flexibility. The point of type systems is to have them sufficiently strong that they reject programs you don't want, but sufficiently flexible so that they do not over-burden the programmer.
>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.
I couldn't find it online either.
>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.
Take care. And thanks for your thoughtful answers.
--PeterD Received on Wed Aug 15 2001 - 04:08:35 CEST