Re: Clean Object Class Design -- Circle/Ellipse

On Tue, 14 Aug 2001 22:08:35 -0400, Peter Douglass wrote:

<snip>

>I think it is important to keep in mind that elegant as Liskov's theory is,
>it is only one theory among many.
 Absolutely (I listed a sample of 5 definitions).
>Thus, per Liskov, the subtyperelationship might require abstract types.
> I'm not sure that the same is true for Martin-Lof's theory.
I'd be interested in learning how the polymorphic M-L defines it (if you ordered the book).

<snip>

>>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.
What I meant was that there is no uniform interpretation of the result produced by a function defined in T that can be used in all functions of S.
IOW, mixed composition of is not commutative with interpretation: If f and g are rational functions, you can't guarantee that  int(g (f(rat(i)) = int(g(int(f(rat(i)))), where rat(i) is an interpretation of integer as rational -- upcast, and int(r) is an interpretation or rational as an integer -- downcast, no matter how you define int(r), be it floor(r), round(r), or anything else that you can think of.

>>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.
This is conflation of inheritance and subtyping, but let's go ahead

Suppose you defined in the supertype the following function rational average(rational x, rational y)

Can you call it in any function defined in the subtype, such as integer double(integer i) {

        return 2 * i;} ?

Not directly. So let's try to redefine the supertype definition: integer avarage(integer i, integer j) {

        return integer(super.avarage(i, j)); }
where integer(rational r) is a function that returns an integer corresponding to the rational argument (aka interpretation/cast). Presumably, the conversion from i and j to x and y is implicit.

Now the types match, so we can call double(average(1,2)). But what is the result? It will be 2 or 4 (depending on how you define downcast) but not 3.

<snip>

>
>I'm not sure what you mean here. See my comments above about C++. (Well
>actually C++ might be a bad example. Some may argue that the type system of
>C++ _is_ useles ;-).
I'd be among them.

>>(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"?
I would argue that it's a benefit of being in the subset relationship. But what exactly is this benefit? The only one that I can see is the ability to pass integers as arguments to real functions. You get neither specification nor code reuse (average number of boxes is code use, to get reuse you need to be able to compose real functions with integer functions).

>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.
Because we can't construct a definition of integer avarage(integer i) that conforms to the invariants specified in the superclass.

>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".
Actually, that's what led to type theory (although Russell may have used the word class in Principia Mathematica). My original reference to Martin-Lof was not to point out his definition of subtype (since the article was about the monomorphic TT), but rather to rebut Badour and others equating types with sets.

>>I believe your definition reduces to Date's.
>Perhaps. I'm not sure though.
Your proof is based on the idea that A implies B, if A is a subset of B (through some function mapping A to B). That's why I think is equivalent to Date's.
>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.
 Are you sure you didn't mean that F is a subtype of G?
> 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.
I think my mis-step was not making clear what my point was.

>To support my possibly wrong interpretation of the affinity between them, I
>offer the paper _Towards a Set-Theoretic Type Theory_ by Adrrzej
>Borzyszkowski, Ryszard Kubiak, Jacek Leszczylowski and Stefan Sokolowski,
>which I downloaded from Hypatia a short while ago.
>
>http://hypatia.dcs.qmw.ac.uk/author/BorzyszkowskiAM
I haven't had a chance to study this paper. In another paper, "Set-theoretic Model for a Typed Polymorphic Lambda Calculus",  they acknowledge that "the complexity of full polymorphism escapes set-theoretic description".
As far as I can tell, the problem is realizability ( implementation), and statements about size.
>The authors point out that among 5 different type theories, Girard and
>Reynold, early Martin-Lof, later Martin-Lof, Cardelli, and Nuprl, only later
>Martin-Lof has a sound set-theoretic model. My point, however, is that it
>does in fact have a set-theoretic model. (The authors go on to explain that
>the critical issue for the other theories seems to be self-application.
>Self-application leads to Russell like paradoxes in set-theoretic models).
Not always. You just have to disallow impredicative definitions.

>> 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.
What I consider important is not result type change, but rather  preservation of meaning (commutativity of composition and  interpretation).

>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.
But what kind of specification are you talking about? Signatures, or axiomatizations (invariants)?

>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.
That's why I think that there is little value to this definition of subtype. I have to declare all types, indicate how they relate to others, and all I get in return is a (potential) reprimand that some of my usage is not "safe". No code reuse. It would be much more useful if the compiler could look at two  specifications and determine if they are consistent, but that is not realistic.

>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.
But declaring it does not make it so, if the axiomatizations (or implementations) are inconsistent.
>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.
This is morphing ;-) into manifest vs latent types discussion.

Marc Gluch
Mindtap Inc. Received on Fri Aug 17 2001 - 09:03:23 CEST