Re: Type substitutability [LONG] (Was: delegation vs. inheritance)

On 18 Aug 2006 09:04:31 -0700, Mark Nicholls wrote:

Dmitry A. Kazakov wrote:
On 18 Aug 2006 03:55:53 -0700, Mark Nicholls wrote:

Dmitry A. Kazakov wrote:
On 18 Aug 2006 02:17:29 -0700, Mark Nicholls wrote:

[...]
the next time you get a ellipse/circle problem maybe consider making
the objects immuatable rather than accepting a weaker type or weaker
subtype relation.

Nick it is a delusion that mutability is the problem. Generalization breaks
LSP in immutable methods. Don't you need generalization?

OK...I'm free wheeling largely....my feeling for this area has changed
radically over the last 12 months....so feel free to test my maive
feelings.

Mutability isn't the problem...but it is a huge constraint on
statically typed systems, that renders circle/ellipses either
inconsitent or massively weakened....remove mutability and we can
construct strong models of circles and ellipses that correspond to the
mathematical definitions.

Huh, construct me Resize that takes Ellipse and returns a Circle!

it will be a new circle...

Irrelevant, there is no such circle, old or new. Wherever you wished to
keep it is a second question. First you need to have it.

it will not be 'Resize'...it will be
'CreateCircleOfDimension'

CreateCircle (AxisX, AxisY);

Everything is immutable. "forall x,y exists Cricle ..." does not hold. End
of story.

not with this.

Circle is not universally substitutable for Ellipse under existence
quantifier.

I don't know what generalization is!......I used to....and then I
eradicated my knowledge...so I geniunely can't remember.....tell me in
10 works and I'll also look it up in Meyer...or another.

Integer is a generalized Positive

that doesn't really help

Integer is an extension of positive......extension in general is a very
weak relationship....substitutable in general is a very very very
strong relation.

How do you measure it? Based of Liskov, it is black and white. That's why
it does not work. When you start to talk about partial substitutability,
you start to return back to the reality.

Substitutability of objects is a relation.
is-X-ization is another. Validity of either Ellipse<:Circle or
Circle<:Ellipse is independent on which is derived from which.

I am not interested in the order in which they are derived.....just how
they 'behave'.

Right. Then observe that Circle is a specialized Ellipse and Ellipse is a
generalized Circle. So when you move from one to another you *inevitable*
break something [*]. This is why neither is a LSP subtype of another,
unconditionally, always and forever.
-----------
*)
generalization breaks in-methods
= substitution under a universal quantifier
specialization breaks out-methods
= substitution under a existential quantifier

This way or another, no chance.

this is a technicality....in a mathematical sense it is not proven as
it stands.......a contradiction in type definition renders the whole
system inconsistent....

That is exactly the problem. 0 = 1 does not renders mathematics
inconsistent. It is just a false statement in a consistent system.

a proof containing a contradiction is not a proof of the
theorem.

How so? Aren't proofs by reductio ad absurdum proofs?

If subtyping is *defined* in the sense of absolute substitutability, then
that type system will be inconsistent *IFF* S<:T were provable and S would
violate LSP. It is not, as Steve has pointed out.

It is not what? provable or consistent with LSP?

There exist consistent type systems with all subtypes being LSP ones. They
might be useless, but feasible.

Now, in that system Circle<:Ellipse would be wrong for any reasonable
application of geometry. So what?

I have given one that is correct.

You can"t, because you cannot construct a circle with two unequal axis.

It is still consistent, though I don't
want such a system, because geometry is more valuable to me. What to do?
Redefine <:! Program correctness is independent on that.

it *is* geometry.
if a program that is a model of geometry and is incorrect..i.e.
contains inconsitent....yet is provably a model of geometry then
geometry is inconsistent......booooom.....bye bye geometry.

You cannot disprove geometry this way. An inadequate model disproves
nothing but its adequateness.

Technically to disprove geometry you have to show an equivalence between
the model and geometry. But you can't.

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

Relevant Pages