Re: Types and "join compatibility"

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

Alternatively, if we add two ints, we could come up with an equivalent expression that involves complex numbers. So the type of integer addition is complex!

Again, I don't think this is a very good way to do things.

Marshall Received on Wed Aug 03 2005 - 17:18:24 CEST