Re: no names allowed, we serve types only

On 23 feb, 01:33, David BL <davi..._at_iinet.net.au> wrote:
> On Feb 23, 12:49 am, Jan Hidders <hidd..._at_gmail.com> wrote:
>
> > On 22 feb, 15:39, Jan Hidders <hidd..._at_gmail.com> wrote:
> > > There is indeed a problem with the subtype = subset principle, or at
> > > least the one that I had in mind:
>
> > > - if t1 <= t2 then [[t1]] is a subset of [[t2]]
>
> > > where [[t]] denotes the set of all values that are of type t. Sorry
> > > for being unclear about that.
>
> > > The restriction that f in the definition should be uniquely defined is
> > > implied by this principle, which IMNSHO makes it not ad-hoc or
> > > gratuitous but rather well-founded. The proof is left to the reader as
> > > an exercise. ;-)
>
> My problem is that there may be existing types t1,t2,t3,t4 and an
> existing declared relation-type with H2 = {t3,t4}.  Someone wants to
> create a new relation-type with H1 = {t1,t2} that subtypes H2, perhaps
> where it is required that t1,t3 represent one role and t2,t4 represent
> another.  However it happens that both t1 and t2 subtype both t3 and
> t4 so therefore it cannot be done because of ambiguity.  That seems
> unreasonable.

Mathematics can sometimes be very unreasonable. :-) But I think this makes sense. If you give me a tuple (row/record) of H2 and would ask for the t1-value in that tuple, then this is ambiguous, since both the t3 and t4 value are also t1 values. It seems reasonable to assume that for tuples of type H1 we require that they contain a single value of type t1 and a single value of type t2. But the tuple of type H2 would actually in some sense contain two values of type t1 (and two values of type t2). So semantically speaking it is indeed not really a subtype.

You could try to fix this by taking another semantics of the types, but I don't see a reasonable alternative at the moment. In fact, my current intuition is that this is a symptom of the fact that we are trying to shoehorn the atrribute-type relationship into the subtype relationship, where it doesn't really fit comfortably.

> > PS. Note that the corrected definition can be compactly formulated:
>
> > Definition:  H1 <= H2 if
> >    for each type t2 in H2
> >    there is exactly one type t1 in H1
> >    such that t1 <= t2.
>
> That doesn't seem right to me - by that definition H1 might have more
> attributes than H2 and yet be considered a subtype.

Of course. For the usual record types it holds that <a:t1, b:t2> is a supertype of <a:t1, b:t2, c:t3>. You can use values of the latter where values of the first are expected, not the other way around.

• Jan HIdders