Re: no names allowed, we serve types only

On 22 feb, 03:40, David BL <davi..._at_iinet.net.au> wrote:
> On Feb 21, 7:05 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
>
> > On 20 feb, 03:40, David BL <davi..._at_iinet.net.au> wrote:
>
> > > I agree this provides some motivation, but it doesn't seem sufficient
> > > justification to "conflate" concerns (as Bob says).  The crucial point
> > > is this:  The attribute domains are part of the relation-type, whereas
> > > the attribute names are part of the relation-value.  What happens with
> > > your suggestion?
>
> I got that wrong.  I should have said:
>
> The crucial point is this:  Whereas both the declared attribute names
> and attribute domains are part of the relation-type, only the
> attribute names are part of the relation-value.
>
>
>
>
>
> > > It's very important to keep a clear separation between a value and its
> > > declared type, in order to understand equality.  Your suggestion ends
> > > up conflating relation-type and relation-value.
>
> > > How do you support sub-typing of relation-types according to sub-
> > > typing of the attribute domains, and still allow for addressing the
> > > attributes by type name?
>
> > That's actually no problem at all. The formal definition of a relation
> > type / relation header in Keith's approach would be a set of types
> > (*). For those types you can define a subtyping relation as follows: a
> > relation header H1 is said to be a subtype of H2 if for every type in
> > R2 there is a subtype in R1. It's even possible to have a matching
> > semantics with that that follows the subtype=subset principle. So no
> > notion of coercion is really needed here.
>
> > (*) Note there would / should be an additional requirement that a
> > header can only contain incomparable types, i.e., it cannot contain t1
> > and t2 such that t1 is a proper subtype of t2.
>
> There is a problem.
>
> Let's write t1 <= t2 if t1 is a subtype of t2 (let this include the
> case t1 = t2).
>
> Definition: header H is valid if for all t1,t2 in H,
>
>   t1 <= t2    implies   t1 = t2.
>
> (this is your "additional requirement")
>
> Definition:  H1 <= H2 if
>   exists bijection f from H1 to H2
>     such that for each t in H1, t <= f(t).

That was not my definition. It would be:

 Definition:  H1 <= H2 if
   exists a function f : H2 -> H1
     such that for each t in H2, f(t) <= t.

Note the direction of f. But also this function is not unique, and yes, I do think that this is a problem.

> [...] Ambiguity in the bijection is incompatible with
> the subtype = subset principle.  So multiple inheritance throws a
> spanner in the works.  The only way to salvage the situation is to
> require the bijection be unique (so in the above example it is deemed
> that H1 is not a subtype of H2).  However I find this gratuitous at
> best.

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]]

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. ;-)

• Jan Hidders