Re: Preventing type extensions

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

On Fri, 24 Sep 2010 20:47:28 +0300, Niklas Holsti wrote:

> Dmitry A. Kazakov wrote:

>>> The property "all horses have hooves" expresses a universal property of 
>>> horses: if X is a horse, then X has hooves. The statement "some horses 
>>> have tentacles" says nothing about any given horse X.
>> 
>> Both are predicates:
> 
> No, they are formulas. "has_hooves(X)" is a predicate that can be true 
> or false for a given object X.

The objects there are types.

> A consequence is that LSP depends not only on the static properties of 
> objects (has_hooves) but also on the set of "mutating" operations.

It depends on the properties of the set as a whole. Properties of
individual objects cannot be contained they leak into the whole set and
other types involved in the operations.

> If we 
> were to define a Rectangle class that did not allow independent setting 
> of width and height, but only a uniform size scaling, Squares would be 
> an LSP subtype of these Rectangles.

which would be

forall s in Size, exists r in Rectangle,
    such that Height(r)=s and Width(r)=s

Existential quantification cannot be avoided. Using mutators instead of
results does not help.

One could possibly limit LSP by narrowing the set of properties under
consideration in an attempt to make it working. However, my impression is
that the point where it starts working, is exactly one, where the
corresponding subtype becomes useless. I considered LSP in a usable form,
where, inevitably, nothing is a subtype of anything but itself. The other
end is: anything is substitutable when types are OK (no properties beyond
type membership).

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