Re: Preventing type extensions

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

Dmitry A. Kazakov wrote:
> On Fri, 24 Sep 2010 16:30:29 +0300, Niklas Holsti wrote:
> 
>> Dmitry A. Kazakov wrote:
>>> On Tue, 21 Sep 2010 19:11:33 +0200, Georg Bauhaus wrote:
>>>
>>>> On 21.09.10 18:25, Dmitry A. Kazakov wrote:
>>>>
>>>>> horse /= animal
>>>> It will help immensely, I think, at least those of us who do
>>>> not do type theory on an every day basis, if we had a glossary
>>>> of terms for interpreting expression like "horse /= animal".
>>> 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."
>>>
>>> is-a /= is
>>> member /= set
>>>
>>> Moreover:
>>>
>>> is-a /= substitutable (greeting to the LSP!)
>>>
>>> Compare: "some animals have tentacles" and "some horses have tentacles."
>> Those are not properties of "horses" and "animals", but properties of 
>> the *set* of horses and the *set* of animals.
> 
> horses is set of horses.

Incomprehensible. What do you mean?

>> 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.

> forall x in horses, x has hooves

That is a universally ("forall") quantified formula that uses the 
predicate has_hooves. The LSP "properties" are implicitly universally 
quantified. To quote 
http://reports-archive.adm.cs.cmu.edu/anon/1999/CMU-CS-99-156.ps, with 
implicit quantification inserted in [] by me:

"/Subtype Requirement/: Let phi(x) be a property provable about [all] 
objects x of type T. Then phi(y) should be true for [all] objects of 
type S where S is a subtype of T."

The following paragraph makes universal quantification clearer:

"We focus on two kinds of properties, /invariants/, which are properties 
true of all states, and /history properties/ which are properties true 
of all sequences of states."

> exists x in animals, x has tentacles

So far as I understand LSP, existentially quantified formulas are not 
considered. Continuing the quote above:

"We do not address other kinds of safety properties of computations, 
e.g. the existence of an object in a state,...".

> [ if you dropped existential quantification, you would not be able to
> describe functions returning values ]

I don't think the LSP model of computation tries to, or needs to, 
describe functions in that sense; it uses postconditions which simply 
assume the existence of a return value and state properties of all 
possible return values.

By the way, note the inclusion of "history properties" in the LSP, this 
is an important point that (I think) has been ignored in this 
discussion. For example, in order to show that the class of Squares is 
not an LSP subtype of the class of Rectangles one must use history 
properties and consider what happens when the program changes the width 
of a Square, seen as a Rectangle, without also changing the height to 
the same new value.

A consequence is that LSP depends not only on the static properties of 
objects (has_hooves) but also on the set of "mutating" 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.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .