Re: Preventing type extensions

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 24 Sep 2010 11:10:57 +0200, Georg Bauhaus wrote:

> On 9/23/10 10:49 PM, Dmitry A. Kazakov wrote:
>> On Thu, 23 Sep 2010 21:00:01 +0100, Simon Wright wrote:
>>
>>> "Dmitry A. Kazakov"<mailbox@dmitry-kazakov.de>  writes:
>>>
>>>> Gosh, it was no more than just this: if horse is an animal that does
>>>> not imply they are interchangeable. Compare: "all horses have hoofs"
>>>> and "all animals have hoofs."
>>>
>>> I don't see your point.
>>
>> It was: the type /horse/ is not the type /animal/. That is not because of
>> Ada's choice to keep them apart, it is because they are behaviorally
>> (semantically) different.
>>
>>> You could make a near-infinity of operations on Animal like has-hooves,
>>> has-tentacles etc but that would be silly. The only ops that make sense
>>> at the Animal level are ones shared by all animals.
>>
>> All primitive operations are already shared, if it were only about type
>> checks there would be nothing to discuss. Ada checks types.
>>
>> Beyond nominal checks, comparing two related types like horse and animal
>> one considers substitutability. S is substitutable for T when any predicate
>> P(T) remains true after substitution S for T. LSP subtype as defined by
>> Liskov&  Wang
> 
> Wing, Jeanette M.

Yes, I typed the name from my head without checking.

>> are those maintaining substitutability. (All possible
>> predicates exhaustively determine what in OO is called behavior. This is
>> why Liskov&  Wang named it "behavioral notion of subtype.") My example
>> illustrated existence of predicates turning false. Thus horse is not animal
>> and animal is not horse (yet *a* horse is *an* animal). It is a tautology:
>> a subset which is the whole set is not the whole set.
> 
> [Just trying to follow.]
> 
> "Subtype Requirement: Let οΏ½(x) be a property provable about objects
> x of type T. Then οΏ½(y) should be true for objects y of type S where
> S is a subtype of T."
> 
> (Where "property" is defined a little later.)
> 
> The authors emphasize that while Stack and Queue may share operations,
> this type checked sharing of operations is not enough.
> It does not guarantee that the programs will work the same way if
> either is used, and likely not as expected. Not working correctly.

The word "provable" leaves much space for that. E.g. when the computing
system has more power than the framework of proving.

> "Properties of an object's behavior" refers to states and
> to sequences of states, as effected by prim ops:
> 
> Invariants:
>    P(state) = True for all states.
> 
> History properties:
>     P(state_1, state_2) = True for pairs of states.
> 
> I think that in your example, Horse (S) is not a subtype of Animal (T),
> since Has-Hooves(x) cannot be proved for any x of type Animal.
> A Horse object can substitute an Animal object IFF all prim ops
> of Horse, including "extra methods", can all be expressed in terms
> of Animal's prim ops *and* respecting the conditions placed on
> the objects states and state sequences.

Horse may have operations of its own.

> The programs must behave
> the same, for Animals and Horses.
> (That's how I have understood the model so far.)
> Correct?

Depends on what is meant under "can be substituted," we have to distinguish
an act of substitution in some given program and a set of programs, some of
them non-existing, where substitution might happen. The former is much
weaker. For example, in a concrete FORTRAN program you could substitute
INTEGER for REAL and get away with that. L&W considered the latter case,
there exist programs where such substitution would not work.

> That is, when I assign an object of type Horse to a variable
> of type Animal, then what matters is that the Animal program still
> behaves as would be correct for an Animal program. But not necessarily
> for a Horse program:  The "apparent" type (L&W) of objects will be
> Animal, a specific type in Ada, and neither aliasing nor objects being
> used in a different context (view conversions in another partition, for
> example) will produce a state not correct for Animals.
> If the program behaves differently when I use a Horse object where
> an Animalis expected, then Horse is not a behavioral subtype of Animal.
> Correct?

Yes, but more than that: if exists a program such that ... then it is not a
LSP-subtype.

[ However, the exemption of non-provable predicates may in the end mean
anything. You could define "provable" in a way excluding predicates you
didn't like. And that would not be just a cheat. For example, you would
like to exclude predicates containing physical memory addresses of the
objects, in some cases, and in some cases you would not. ]

> So, up to here, nothing in Liskov & Wing's Subtype Requirement
> (as quoted above) corresponds to Ada's Animal'Class. [Just to
> make sure I get the words right.]
> Correct?

Hmm, there are 16 subtyping relations (<:) to consider here. You have
horse, horse'Class, animal, animal'Class. There are more of them because we
have to consider in-, out-, in out- "subtypes" of them, e.g. "in horse" and
"return animal". Then come anonymous access types. They too can be
substituted when the prefix notation used. E.g. Horse_Ptr.Feed.

[ I presume that substitution = the language accepts usage of S, a
type/subtype distinguishable from T, which was originally used in the
operation profile.]

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de