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


Dmitry A. Kazakov wrote:
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.

I'm not with you...


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.

please give example.


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.

It depends on how strong your type definition is.


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 [*].

correct....but not everything.

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.

Not too sure what 'in/out methods' are
can you give a simple example


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?

yes....they are proofs that the premise is *false*.

to prove A I assume not A and derive a contradiction => not not A => A


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.

they also might not be useless.


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.

?

I don't need to...I've missed this point.


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.

a model that is provably a model of a theory yet is inconsist......says
something fundamental about the theory.


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


?

that is what a model is.

.

Relevant Pages

  • Re: Type substitutability [LONG] (Was: delegation vs. inheritance)
    ... LSP in immutable methods. ... Don't you need generalization? ... construct me Resize that takes Ellipse and returns a Circle! ... because geometry is more valuable to me. ...
    (comp.object)
  • Re: The falsity of Einsteins continuum
    ... >>>rolling without friction on the inside of a great circle, ... loop of string and two push-pins to draw an ellipse. ... >> an ellipse with an eccentricity of 0.0. ... the whole geometry incuding Euclidean ...
    (sci.physics.relativity)
  • Re: The falsity of Einsteins continuum
    ... >>rulers at a right angle, and a third ruler with a central ... > loop of string and two push-pins to draw an ellipse. ... The circle is also ... the whole geometry incuding Euclidean ...
    (sci.physics.relativity)
  • Re: The falsity of Einsteins continuum
    ... >>rolling without friction on the inside of a great circle, ... > the cases of being an ellipse. ... Eccentricity 1 is a straight line of a length ... the whole geometry incuding Euclidean ...
    (sci.physics.relativity)
  • This week in the mathematics arXiv (7 Mar - 11 Mar)
    ... A generalization of the Kuga-Satake construction ... On the simpleness of zeros of Stokes multipliers ... DG: Differential Geometry ... Derivation into duals of ideals of Banach algebras ...
    (sci.math.research)