Re: no names allowed, we serve types only

On Feb 24, 5:22 pm, Jan Hidders <hidd..._at_gmail.com> wrote:
> On 23 feb, 18:08, David BL <davi..._at_iinet.net.au> wrote:

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

I wonder whether a subtype of a copy is a subtype of the original.

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

Consider a formalism where

1. a tuple-type T(A) is parameterised by a finite set A of (attribute name, attribute type) pairs where the names are distinct; and
2. a tuple-value is an element of [[T(A)]] (using your notation) if it equals a set of (name,value) pairs representing the graph of a function from the attribute names of A to values of the respective attribute types.

If the subtype = subset principle is adhered to, then the question of whether T(A1) <= T(A2) is uniquely determined.

T(A1) <= T(A2) if and only if

   exists bijection f : A1 --> A2
    such that f(N1,D1) = (N2,D2) implies       N1=N2 and D1 <= D2.

I have doubts whether it is possible under ZFC (which disallows universal sets such as a set of all sets) to formalise a tuple in such a way that subtypes occur in the manner you suggest.

If a type <a:t1, b:t2> represents all tuples that at least contains the fields a and b with values of the required types, then this involves a universal and won't represent a set under ZFC.

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

Agreed, but I think the same (informal) reasoning applies to tuples.

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

I was thinking for example that implicit conversion is involved here:

    Ellipse e;
    e = Circle(1, Point(0,0)); // assignment

Implicit conversion doesn't mean a value is being converted. Instead it relates to the implicit upcast on the static type of the right hand side expression. Here, implicit conversion is a concept used in static type analysis. Received on Thu Feb 25 2010 - 02:39:10 CET