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


S Perryman wrote:
"Mark Nicholls" <Nicholls.Mark@xxxxxxxxx> wrote in message
news:1155828294.267139.88980@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

S Perryman wrote:

[ Circle/Ellipse example snipped ]

OK I'm only just with the syntax....your abstraction is mutable?

That is the problem, this is not true of a mathematical definition of
circles and ellipses.

Mathematical objects are all immutable.....always.

Which properties of ellipse and circle have caused the conflict ??
The foci.

The mutability of the foci.

mutability is evil (well at least a signicant constraint on either
state or the strength of the type).

This is quite a lazy mindset. The problem is due to mutability.
Bit like me saying being infected with SARS is due to breathing air.

OK...fair enough....one way of eradicating the mismatch of the
mathematical model and the OO absraction is to eradicate
mutability....it is my prefered route.



For ellipse and circle, what is the relationship between the foci ??
The set of values that a circle can define is a *subset* of the values
that
an ellipse can.

Subset relationship ??
Problem suggested in advance by Wegner and Zdonik. QED. :-)

So what Wegner and Zdonik are stating is that if you look at the details,
you may pre-empt the grief. If you have a proof tool, or perhaps DBC, you
may find the problem quickly.

if you drop the mutability then you do not have the closure of your
object states obey the type definition....(well you do, it just doesn't
change).....then you export the new state.....(I've been here before
talking about the problems of the state pattern and how it inhibits
strong type definitions....I was largely poo pood...if you say
"externalise state" people start hopping up and down....as breaking
encapsulation...yes I am choosing to expose more than I have to in
order to strengthen my type definitions).

so if we change the language to do it as it would be in mathematics i.e.

interface IEllipse
{
IEllipse SetFocusA(x);
IEllipse SetFocusB(x);
}

(I don't know how to write the contract but effectively an ellipse is
immutable...if you SetFocusA/B you get a new IEllipse

interface ICircle : IEllipse
{
ICircle SetFocusAAndB(x);
}

now circles "are" ellipses...and are true subtypes.

And all I had to do is :

type Ellipse
{
focusA(f) ;
// post: focusA() = f
}

type Circle
{
invariant : focusA() = focusB()

focusA(f) ;
}

No substitutability conflict.


OK......because you''ve kept mutability, your abstraction of ellipse is
incredibly weak...much weaker than mine.

I cannot actually set a given ellipse to given dimensions.....


SetToUnitCircle(Ellipse e)
{
e.focusA(1) ;
e.focusB(1) ;

// is e a unit circle?.....I have no guarentee.
}

In my world it is guarenteed (given the post conditions).

(thus my point about mutability having a large cost in terms of type
strength).


But we work in the real world. And more often than not, the conflict
reveals itself in all its gory glory at the exact time that it causes the
most grief.

The grief is the closure of state obeying the type definition....the
real world (for the usual circle/ellipse example) is not a model of our
abstractions....the abstraction is mathematically incorrect.....all we
need to do is make the abstraction actually describe the mathematics
and it all just works.

And how do you make the abstraction correct ??
By understanding what it is that causes the software realisation to become
*incorrect* .

I don't understand this phrase "software realisation"....

I define an abstraction which either models the world or doesn't....I
then implement it correctly or incorrectly.....my beef is that
mutability renders the 1st part of this exercise (in this example) to
be very very weak, in order to guarentee all implementations are
'correct'.

Liskov/Wing. Wegner and Zdonik. And so on.


They simply give you a 'true'/'false' criteria given a (very
constrained type of) type.

Useful yes.....but it is mutability that renders the types to be very
weak.

Given mutability you cannot define a type so that I can 'set' an
ellipse to be a unit circle, without breaking substitability....in fact
in general the only 'subtypes' (in set terms) are those subsets closed
under all state changes.....for the classic circle ellipse setup that
is the whole of the set....in your example no....but your type is weak.

That seems to me to be potentially tying one hand behind your back
before you've even got to writing the code.


But an Emu clearly is a bird. Just one that cannot fly.
Specifically Emu instances can be used in all contexts that a Bird
instance
can, except that one.

OK fair enough...I know what your saying....it is a weaker substitution
relation....but for some contexts substitutability holds.

Weaker than the Liskov/Wing subtype.

Yes.....and Liskov/Wing types aren't as strong as they could be.



Should a type system reject the substitution for all those other contexts
because of this one exception ... ??

hmmmmm

ideally no.

":" to me indicates "forall" contexts.....

I think I'd rather juggle the type hierachy...effectively those
contexts that aren't interested in flying, but are interested in
feathers are coupled to the property of flying where they shouldn't
be......unnecessary couping = bad...and in this case fatal....I'd
rather go....

[ example snipped ]

I can't pass an emu into this method.

All that work just to avoid the one exceptional context.
And when you have birds that can fly but can't swim ??
Can't fly but can swim ?? Can't do either ??

Theoretically they implement the abstractions that the actually
implement in the real world.

We as humans are lazy....when we say something is a 'bird' it's because
we are too lazy to say...feathered+fly+beak+......but the cost of thay
lazyness is inconsistency....i.e. logical inconsistency....i.e.
incorrectness.....thats fine for the pub.....but more difficult for
legal documents.....and even more difficult for
software.....mathematics avoid it by demanding absolute
consistency....for OO theory I like it to be absolutely consistent.


How much work are you going to be doing on your example to
accommodate the above ... ?? :-)

In theory I would model the real world...I would create abstractions
that describe the real world....and then I can invoke model theory and
absolutely claim my software to absolutely be correct.......in
reality....it depends how important the exception is....there is loads
of coupling in my code and your code becuase of multiple methods
sharing the same interface.....lifes to short to shatter them
all...yes.



If you want to define IFeatheredAndFlying to be synonymous with "bird"
then an emu is not a "bird"...trying to have both is
understandable....but flawed.

It reminds me of the saying "the exception that proves the
rule"....which I never really understood....the exception always
disproves the rule to me.

I think the rationale is that something holds for so long and then every
once in a while something appears that breaks the rule. But it is so far
and in-between that the rule is perceived to universally hold.


Which maybe is your point...and Emu is a bird....all birds
fly.......person to person...yes.

Unnecessary coupling is bad....coupling methods to unnecessary
'properties' is sometimes good.....person to person...yes.

look I agree.....I am picking brains not really disagreeing...

my observation is;

mutability costs either to the strength of your subtype relationship or
to your type definition....I think in general it costs too much.

the theory needs to be mathematically consistent and watertight...no
exceptions.

in the real world software takes long enough without being absolutely
correct - yes...

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.

.

Relevant Pages