Re: no names allowed, we serve types only

On 23 feb, 18:08, David BL <davi..._at_iinet.net.au> wrote:
> On Feb 23, 5:28 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
>
>
>
>
>
> > 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.
>
> I agree with all that, and add that it is noteworthy that the
> ambiguity problem disappears with named attributes.
>
> Anyway, I don't believe our analysis is complete, because our
> definitions don't specify what happens exactly with Keith's "copy"
> types (which must be used where there is a subtype relationship
> between two of the attributes in a header).

If he allows copies of copies or subtypes of copies he will run into the same type of problems. If he doesn't, then he apparently distinguishes copies (which cannot have copies and subtypes) and normal types (which can). But that would be IMHO somewhat ad-hoc and a sign that these copies are not really types at all.

> > > > 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.
>
> That view of subtyping concerns a possible interpretation of
> substitutability (of values), but I believe it is better to adhere to
> the subtype = subset principle for data types.  It cannot be said that
> tuples of the form <a:t1, b:t2, c:t3> represent a subset of tuples of
> the form <a:t1, b:t2>.

Depends on what you mean by "of the form". In type theory for programming languages and databases, if they consider subtyping, the usual definition of a tuple being of the type <a:t1, b:t2> is that it is a tuple that *at least* contains the fields a and b with values of the required types. Under that definition the subtype = subset principle is adhered to.

In case you are interested:

L Cardelli (1984), 'A semantics of multiple inheritance', in: Semantics of Data
Types, LNCS 173, eds. Kahn, MacQueen and Plotkin, Springer Verlag, 51-68.

L Cardelli and P Wegner (1985), 'On understanding types, data abstraction and
polymorphism', ACM Computing Surveys, 17(4), 471-521.

> C.Date presents this argument very well in section 20.9 of an
> Introduction to Database Systems where he claims that a coloured
> circle is not a subtype of circle (or vice versa).

The tuple that represents the circle is not the same thing as the circle itself. I find Date's argument rather unconvincing, to put it very mildly. He is by no means an authority in this area, and those that are mostly disagree with this position.

> I suggest implicit conversions must only be an artefact of the type
> system (i.e. implicit conversions cannot actually change a value by
> adding or removing information), and in fact no concept of implicit
> conversions is required in a typeless formalism.

I would even add to that "or in a typed formalism". If in the semantics you need implicit conversion you probably need to rethink the semantics of your types.

• Jan Hidders