Re: Proposal: 6NF

vc wrote:
> Jan Hidders wrote:
> > vc wrote:
> [...]
> > > A, B and C are real;
> > > D, E are integer;
> > >
> > > C = A / B -- is OK
> > > C = D / E -- the LSP requires that should be OK too but it is not
> > > because D / E is undefined.
> >
> > No, it is defined. D and E are in the domain of integers, and therefore
> > also in the domain of reals, so the result is the real D/E with / the
> > operator (in both expressions) as defined by the reals.
>
> The result cannot be "defined by reals" because you do not have any
> elements in your integer domain to define such result. There is no
> number 0.66666666... (2/3) in it, it's gone when you subsetted your
> integers.

The result is defined and exists, that is all that is required. You can repeat as often as you like that it is not an integer, but that is completely irrelevant.

> If you jump into the real domain each time the operation cannot be
> defined in integers, what's the point of even talking about the
> integeres?

It allows a tighter and more refined typing regime that warns you when you use a real where an integer is required. This, after all, was one of the points of having a typed language.

> What's the point of such talk ? Needless to
> say that such viewpoint does not make any sense in math.

It gives us a simple, elegant, intuitive and consistent way of dealing with the semantics of subtyping which has clear practical purposes. By most reasonable definitions of "making sense" I would say that it does. In fact, most mathematicians that I've talked to in my career on this issue don't agree with you, and those are not only the mathematicians that happen to work in my own department.

> The LSP holds because your subtype is ephemeral -- each time the LSP is
> violated you replace the subtype with its 'parent type'.

We don't have to replace anything, since the integers were defined here such that they are a subset of the reals.

• Jan Hidders