Re: Types and "join compatibility"

From: dawn <dawnwolthuis_at_gmail.com>
Date: 4 Aug 2005 18:24:04 -0700
Message-ID: <1123205044.832143.82530_at_g44g2000cwa.googlegroups.com>


Marshall Spight wrote:
> x wrote:
> > "Marshall Spight" <marshall.spight_at_gmail.com> wrote in message
> > news:1122761293.933576.29120_at_o13g2000cwo.googlegroups.com...
> >
> > >As to the rename, yes of course, otherwise it wouldn't be a *natural*
> > >join. In fact, I'm going to rename your whole example for clarity.
> >
> > >(read ":" as "has type"; P for parent, C for child)
> > >Relation PR : (a : P)
> > >Relation CR : (a : C)
> >
> > >What is the type of PR join CR?
> >
> > What kind of type ?
> > The declared type or the most specific type ?
>
> The terminology you're looking for is "static type" and
> "runtime type." TTM makes up a lot of new terms for things
> with perfectly acceptible terms already. I do not know
> whether it is because they are unaware of modern type
> theory or because they just don't consider it of value.
>
> > >Date&Darwen's TTM says it's a relation of type (a : P).
> > >This has never made sense to me; the result can only contain
> > >values that correspond to C, so what's the point of having
> > >it be P?

Agreed. Assuming a natural join is necessarily an equijoin (I think that is the case, but didn't look it up to verify), we know that a could be said to have type C in the result. Making it a P would unnecessarily lose information (e.g. constraints).

> > The declared type is (a:P).
> > The most specific type is (a:C)
> >
> > The declared type is (a:P) because they decided that every two echivalent
> > expressions have the same declared type.
>
> That does not strike me as a very good reason.
>
>
> > Let M:Set(P) and N:Set(C).
> > M intersect N = M minus (M minus N)
> > type(M intersect N) = type (M minus ( M minus N)) =
> > type (M)\/(type(M)\/type(N))=Set(P)\/(Set(P)\/Set(C))=
> > Set(P)\/Set(P)=Set(P)
>
> In the same way:
>
> Let U = the universal set. U:U
> M intersect N = N minus (U minus M)
> type (M intersect N) = type (N minus (U minus M)) =
> type (M) union (type (U) union type M) =
> type (M) union (type U) =
> type (U)
>
> So the *real* answer is that the static type is the universal set.

love it --dawn Received on Fri Aug 05 2005 - 03:24:04 CEST

Original text of this message