Home > Archive > Functional > May 2005 > Re: Explicit versus implicit subtyping mechanisms
You are viewing an archived Text-only version of the thread.
To view this thread in it's original format and/or if you want to reply to
this thread please [click here]
| Author |
Re: Explicit versus implicit subtyping mechanisms
|
|
| Dmitry A. Kazakov 2005-05-11, 4:00 pm |
| On Wed, 11 May 2005 11:47:34 +0200, Andreas Rossberg wrote:
> Dmitry A. Kazakov wrote:
>
> How does that relate to anything?
Wasn't that in the paper you referred to?
>
> I believe that mathematicians will strongly disagree with you. ;-)
Ah, but mathematicians will also strongly object against the thesis that an
integer *is a* rational. There is an injection from integers to rationals,
no more than that. Mathematically there is no immanent relation between
both. The common structure of interest ring, group, whatsoever depends on
the "application". Quite similar to this, the subtyping relation between
both types has to reflect our need in generic programming. That programming
may need a division, but don't require f(x)/f(y) = f(x/y).
>
> Indeed. So? Who is interested in types with no operations?
Exactly. Where is my division? (:-))
Everything depends on the behavior said Barbara, but the behavior isn't a
property of the types involved. So integer might be a subtype of rational
or not, depending on the context. I do not need such definition of
subtyping.
>
> Not exactly. Just was using your wording.
But LSP-subtyping is about types and so sets. Subtyping is not subsetting.
To preserve the behavior propositions on the elements are too weak.
>
> Mh, you might have misunderstood me. What I meant was that you cannot
> state properties like "there exists an X in C for which the two axes
> have different length". That would be true for the class C of ellipses
> only. But types (usually) cannot encode such properties.
Why? Any covariant out-parameter exposes exactly this. If you want to have
covariant out-parameters + specialization, you are in trouble. (BTW,
in-parameter ain't better. They break under generalization.)
> Can you give an example of a property that is true for any ellipsis, but
> not for a circle? Those are the ones in question.
You want to kill covariance, do you? (:-)) But without it there is no
subtyping. A contravariant ellipse isn't circle.
>
> You describe coercive subtyping. That is only one form of subtyping, and
> certainly not applicable to everything.
I don't see why it couldn't be applicable.
> It also is not the predominant
> model of subtyping on objects, as far as I can tell.
Yes, there is no language I know which consistently applies it. Though this
model explains other type models very well.
>
> Frankly, I have no idea what your rules for creating subtypes are then.
> They do not seem to be based on any semantic property, rather on
> convenience.
Right.
> It is a mystery to me then why - at the same time - you
> oppose structural typing in the name of semantics. I am really 
> about your point of view.
Mmm, there is no obvious relation to me. Either a convenience of the
programmer or program semantics is there any difference? OK, I hope that
programmers do not sabotage. (:-)) Anyway, both lie outside the language.
So you cannot communicate them using the language. Not so the subtypes, I
want them be in. Nominal subtypes are clearly in. Inferred subtypes is a
border case. They are in for the compiler, but for the reader it is not
obvious. I am not entirely against them, I am cautious. Consider a minor
erroneous change which makes A from a subtype of B, an unrelated type. This
could have a catastrophic impact on the whole program. Now, you, a poor
programmer are in the position to figure out why! Sounds familiar? Right
that's C++ templates! Is there anything more dreadful than fighting error
messages in templates? Much worse is when C becomes B while it should be D,
which causes some fine effects when the system load reaches 60% each
afternoon in July 12-20, except w ends...
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
| |
| Mark Nicholls 2005-05-13, 4:08 pm |
| > >It is relevant....because while computer scientists get all hot
under
of[color=darkred]
rationals,[color=darkred]
make[color=darkred]
was......[color=darkred]
>
> All our science is based in such maths,
that was the problem....if science is based on maths, and
mathematicians are not sure whether maths 'works'.....then we're in the
do do.
so they spent lots of time constructing maths from the ground up,
reconstructing Z, Q, R from the axioms of set theory, and had lots of
arguments very much like this, and they were resolved.
I think computer science needs to do the same.
The irony is that the mapping/domain approach seems to fit more
naturally into how we feel type theory should work....another approach
using formal concept analysis is also (to me) more formal and more
natural.
> but computing science is in a
> very primitive stage among other things because it is not able to
> model elementary maths.
well then I think it's ****ed then.
>
of[color=darkred]
>
> Integers are rationals by definition,
OK maybe 'rational', if 'rational' means that it's in the image from
Z-->Q of <x,1>----><x>.
But it is not a member of the rationals Q.....because if it is, then
the rationals cease to have any known sound definition, and potentially
we basing our assertions on fallacy.
Z is a subset of Q
Q is the quotient field of Z
?
oh dear.
> and it is in virtually every
> math textbook that talks about numbers. It is a foolish act to state
> the contrary.
many text books tell us,
F=MA
is it true?
no.
if you want to model the universe you go to einstein and not newton.
If you want to model maths, you go to Godel/Cantor, not a high school
maths book.
>
any[color=darkred]
>
> Because "properties of Z and Q are different" does not mean: the
> properties of any element of Z are different to the properties of
> every element of Q.
>
> That's very basic logic.
is it?...it doesn't work for me. if I say '2', is there a 'number' that
multiplied by it = '1'?
if it's '2' member Q then yes.
if it's '2' member Z then no.
the logic above that is very basic....if you wish to define Z in this
manner, you cannot be sure of anything you say about Z or Q.....it also
leads you into fallacious arguments about the cardinality of numbers.
is Z subset Q.....are there more numbers in the set Z than in Q? that
one probably kept Cantor up all night....and decided that Z is not a
subset of Q.
>
> For instance: the properties of a golf club are different to the
> properties of a tennis club, but it does not mean that you can not be
> a member of a golf club and a tennis club at the same time.
this is the problem with the set membership route.
what happens when I ask you for your membership card?
am I talking to you as a member of the tennis club or the golf
club......
It seems sensible to me to say
I am a member of the domain people.
There exists a mapping from people to the domain of golf memberships.
There exists a mapping from people to the domain of tennis memberships.
now if I ask the question of a member of the domain of golf membership,
I get a golf one, if I ask the question of the domain of tennis
membership, I get a tennis one.
no ambiguity....no double membership, and as formal as the construction
of Q.......so whats the problem?
>
does[color=darkred]
>
> But they are the same thing anyway.
>
> Show me a property of <1> that is not in <1,1>
I cannot go <1>/<n>
>
see....[color=darkred]
>
> How is division broken?
>
> I heard that thing several times but I am still waiting for any
> argument.
technically it is not defined.
if you define it in the natural way......you get Q! (to isomorphism)
thus Z does not exist as a seperate construction.....which is
unfortunate, because Q is defined in terms of Z......pooooofffff....it
all slips through your fingers.....I'm my own grandad.
>
>
> Axioms:
>
> A rational number is a number that can be expressed as a fraction p/q
> where p and q are integers and q<>0.
what is a 'number'?
>
> 1 is an integer
>
> Proof:
>
> 1/1 is a rational (because 1 is integer and 1<>0)
>
> 1/1 = 1 => 1 is a rational Q.E.D.
>
>
> It was not very hard :)
>
but it is unfinished.
please define 'number'.
or are the 'numbers' the rationals....and then it's all lost.
or are the 'numbers' the reals.....its all lost because they are
constructed from the rationals...
http://mathworld.wolfram.com/DedekindCut.html
| |
| Mark Nicholls 2005-05-13, 4:08 pm |
| >
> What is 'what'? What is 'is'?
>
Actually, genuinely this may be the root cause of the problem
'is' to me, at worst means 'isomorphic'.
The problem with claiming that Z 'is' a subset of Q implies to me that
Z is isomorphic to a subset of Q.
At best this is troublesome, becuase what sort of morphism are you
claiming from the subset to Z?
If we assume that it is a field morphism, because Q is a field, then it
does not work.
I actually do not know how to construct the isomorphic map, somehow you
have to remove the axiom of fields from the members of Q in order for
it to work.
If we claim there is a homomorphism into Q, then I'm happy, if you
claim that you can embed Z in Q, I'll wince, but keep quiet, if you
claim that Q is an 'extension' of Z, I'll probably complain a
little.....
| |
| Mark Nicholls 2005-05-13, 4:08 pm |
|
Ketil Malde wrote:
> "Mark Nicholls" <Nicholls.Mark@mtvne.com> writes:
>
>
> By construction - we define Q as Z and some other elements. How
could
> it *not* be a subset?
>
but you told me
"Define the obvious equivalence classes for rationals"......
so which is your definition?
| |
| Mark Nicholls 2005-05-13, 4:08 pm |
| Ketil Malde wrote:
> "Mark Nicholls" <Nicholls.Mark@mtvne.com> writes:
>
that[color=darkred]
>
> Yes, it's the rational number one half.
but if I was talking about '2' member of Z....then there isn't.
so it seems quite important to state with '2' I am talking about.
>
>
> Nonsense. Two is two, regardless of which sets it constitutes a
member
> of. How else could you pay a rational price if you only have integer
> money?
?
I cannot construct 234456/343465645 pence....money to me are
integers....and this example is a demonstration of the danger, if I
modelled money as a rational, I would be in the ****.
>
> Division is perfectly well defined on integers as well, it just
> happens to be a partial function if you don't allow for rationals.
In
> fact, it is a partial function on rationals as well if you allow
zero.
partial funtion?
I suspect this construction is isomorphic to the rationals.....well
done, you have constructed the rationals, on which, yes, division is
well defined.
>
that[color=darkred]
a[color=darkred]
>
> Reference please? Where does Cantor say this? And perhaps you
should
> read about diagonalization, which I think is due to, yes, Cantor.
he did not say it......he proved that this sort of Z subset Q =>
order(Z) < order(Q) was nonsense.
>
>
> Jerzy's recollection of Cicero spring's to mind.
?
>
>
>
> Sure you can. It's -- borrowing your syntax -- <1,n>. A rational
> number. The same as you get by dividing <1,1>/<n>.
again you have just constructed the rationals.
yet if you define that Z is a subset, how can you construct them.
>
>
>
>
> Well, neither is it defined for all rational numbers (see above).
It is not defined on **any** member of Z.
It is defined for all members of Q apart from 0.
that is how division is broken.
>
>
> What is 'what'? What is 'is'?
I'll take them as axioms.
now,
what is a 'number'?
>
>
> Come on, he's only used integers, which can be defined as nested
sets,
> or Peano numbers or whatever.
is it defined as nested sets? peano postulates? or as a subset of Q?
I no longer know what you definition is.
>
>
> Could you explain the relevance, please?
>
maybe we can define the rationals as a subset of the reals and see how
far we get........
maybe we can construct derivatives of functions defined in terms of Z?
maybe the set of Q is bigger than Z?
| |
| Mark Nicholls 2005-05-13, 4:08 pm |
|
Ketil Malde wrote:
> "Mark Nicholls" <Nicholls.Mark@mtvne.com> writes:
>
>
> ..you would be talking nonsense.
so you are claiming that I cannot talk about '2' being a member of
Z?!?!?!?
am I talking about the '2' that is both a member of Z and Q, or the one
in Q or the one just in Z......that's nonsense.
>
that[color=darkred]
a[color=darkred]
>
Cantor.[color=darkred]
>
>
> So what, exactly, was the point?
>
> Look, I strongly suspect that you have no clue about Cantor.
a reasonable assertion.
I do know my maths foundations though.....or at least did.
> I'll
> happily review my position when you come up with a quote where he
> states that Z is not a subset of Q.
the onus is on you not me....
you need to demonstrate it is.
Currently the status quo states that the integers are defined as the
quotient field of the integers.
you have sketched a proof that Q can be constucted from the union of Z
and the bits left over.
You also need to demonstrate how you can then 'add' orthogonal axioms
to one domain while preserving isomorphism, to a previously isomorphic
one.
I, quite reasonably, am claiming that it is not the normal construction
of Q, and as such is dubious until proved.
I do not understand why you don't follow the conventional construction
as the basis for your model?
|
|
|
|
|