Re: foreign key constraint versus referential integrity constraint

> More generally, the values in the result of a join are the
> intersection
> of the values in the operands; why wouldn't the result type be the
> intersection type?

That's because we're mixing two different levels of typing. The first, weaker kind only considers set operations and typing in general. In this frame of mind, and as Bob already pointed out, you will have to find the common supertype of string and integer before you even have the comparison operator available. The lowest common supertype in this case is TOP, which as it happens *only* has a single equality comparison operator. The type of the join column is then the supertype where we finally find the means of comparison, i.e. TOP.

But you can also go deeper and consider the semantics of the equality operator. Then you actually know that the result set is always the intersection of the incoming ones, that because of that we can unify the two sides of the resulting comparison to get "the join column" of one homogeneous type, and furthermore that, in the case of types whose least common supertype is TOP, the intersection type will also be uninhabited. What happens is that now we're actually propagating types through different kinds of operators, and the equality comparison operator is just one of them, with its particular properties. A minimum nontrivial counterexample in this vein would probably be a join using a less-than comparison between integers and floats.

> Consider relations A and B each with a single, common attribute.
> Natural join and inner union will behave much like intersection
> and union in this case. If the result type of the join isn't an
> intersection type, then we lose the property:
>
> A = A join (A union B)
>
> because the type of the attribute of the expression is different
> than the type of the attribute of A.

That equality never held for types. Only for the values, or in other words for the values considered as inhabitants of TOP. That's essentially because type logics tend to be intuitionistic, or even modal, not classical.

--
Sampo