Re: no names allowed, we serve types only

On 22 feb, 15:39, Jan Hidders <hidd..._at_gmail.com> wrote:
> 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]]
>
> 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. ;-)

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.

• Jan Hidders