7
$\begingroup$

There's a question that's been bothering me.

I even implemented it backwards when I implemented the type system for my language.

Why do intersection types have more fields and union types have fewer fields?

In set theory,

{a, b} & {b, c} => {b}
{a, b} | {b, c} => {a, b, c}

Whereas in type theory,

type P = {a: int, b: int}
type Q = {b: int, c: int}

P & Q = {a: int, b: int, c: int}
P | Q = {b: int}

In set theory, A is a subset of B if all the elements in A are in B.

In type theory, B is a subtype of A if all the fields in A are in B.


I know types can't be seen as sets, but I still can't understand why it's all the other way around.

Can anybody give a consistent explanation to answer my doubts, thanks!

$\endgroup$
5
  • 4
    $\begingroup$ I have a tingly feeling this is better for CS.SE $\endgroup$
    – Seggan
    Jun 19, 2023 at 16:20
  • $\begingroup$ This is answered (in the context of Typescript) on Stack Overflow here: stackoverflow.com/q/38855908/12299000 $\endgroup$
    – kaya3
    Jun 19, 2023 at 18:28
  • 1
    $\begingroup$ I've created a post on meta to discuss whether questions purely about type theory should be on-topic here. $\endgroup$
    – kaya3
    Jun 19, 2023 at 18:43
  • 1
    $\begingroup$ This question and answer may be similar to stackoverflow.com/q/38855908/12299000 but they come at it from a different angle. I feel this question and its answers add value. Could it be migrated? $\endgroup$ Jun 21, 2023 at 8:17
  • 2
    $\begingroup$ The meta post pretty explicitly sets out that this post is on-topic — concretely, this exact post — so it should at least be open pending any further developments on that front. $\endgroup$
    – Michael Homer
    Jun 21, 2023 at 9:54

5 Answers 5

5
$\begingroup$

Think about it like this:

In set theory, the intersection of two sets consists of the elements that are common to both sets. The more sets you intersect, the fewer elements you are left with because you are narrowing down the common elements. On the other hand, the union of sets combines all the elements from the participating sets without duplication. Therefore, the more sets you union, the more elements you accumulate.

This is pretty intuitive, so let's move on to type theory.

Let's use your example:

type P = {a: int, b: int}
type Q = {b: int, c: int}

In type theory, when you take the union of types P and Q, the only thing you know for sure is that you will have the b field. You can't be sure if you have the a field or the c field. This means that:

P | Q = {b: int}

Also, when you take the intersection, the new type has all the fields because it is necessary that it can be converted to both P and Q. If it only had the b field, you couldn't convert it to either P or Q. This means that:

P & Q = {a: int, b: int, c: int}

In conclusion, when you're thinking about unions and intersections in type theory, don't think about the fields. Think about the objects of the types. An object of type P | Q could be from either P or Q, so we can't assume anything about the uncommon fields. An object of type P & Q will have all of the fields of P and all of the fields of Q because it can be converted to either P or Q.

Also, about the subtypes/supertypes thing, think of it as "B is a subtype of A if you can convert an object of type B to type A". This means that all the fields in A are also in B.

$\endgroup$
4
$\begingroup$

There is an extremely short way to answer your question. In the question, you said the following:

In set theory,

{a, b} & {b, c} => {b}
{a, b} | {b, c} => {a, b, c}

Whereas in type theory,

type P = {a: int, b: int}
type Q = {b: int, c: int}
P & Q = {a: int, b: int, c: int}
P | Q = {b: int}

Note that in {a, b}, a and b are elements of the set, meaning that a ∈ {a, b} and b ∈ {a, b}. However, in {a: int, b: int}, a and b are fields, which does not mean that a : int ∈ {a: int, b: int}! The meaning of a : int here is that if x ∈ {a: int, b: int}, then x.a : int.

So it's reasonable that the arrows are backwards.

$\endgroup$
3
$\begingroup$

Fields on a structural type are not analogous to elements of a set.

type P = {a: int, b: int} doesn't mean that a value of type P is either a or b, it means it has to have fields a and b. You can see a field in this way as a constraint on a type. If you want to see P as a set, you can describe it like this pseudo-code: type P = {t forall t if t.a: int & t.b: int}

In this notation: P & Q == {t forall t if (t.a: int & t.b: int) & (t.b: int & t.c: int)} == {t forall t if t.a: int & t.b: int & t.c: int}.

There are more constraints on values of type P & Q than there are on values of type P, and thus more fields, but less values, in the sense that the set of values which have type P & Q is a subset of the set of values which have type P.

On the other hand: P | Q == {t forall t if (t.a: int & t.b: int) | (t.b: int & t.c: int)} == {t forall t if (t.a: int | t.c: int) & (t.b: int | t.b: int)} == {t forall t if (t.a: int | t.c: int) & t.b: int}. Since a structural type system may not be able to express types like "either has a field a: int or a field c: int" and having those types tends not to be very useful anyway, it may just drop that constraint and make P | Q == {t forall t if t.b: int}

There are less constraints on values of type P | Q than there are on values of type P, and thus less fields, but more values, in the sense that the set of values which have type P | Q is a superset of the set of values which have type P.

So while subtypes are not exactly equivalent to subsets, they are analogous and definitely not "the other way around".

Finally, when comparing {a, b} and {a: int, b: int}, don't be mislead by the visual similarities. The matching tokens {, a, ,, b and } mean different things in both notations, like the way a * means very different things when used in int* versus 2 * 3 versus .*.

$\endgroup$
3
$\begingroup$

Here is my understanding from the perspective of category theory.

Let's consider the category whose objects are sets and whose morphisms are defined by subset relation. Set intersection and union are then the categorical product and coproduct respectively. In other words, A ∩ B is the set that, for any set C, C is a subset of A ∩ B if and only if C is both a subset of A and a subset of B; A ∪ B is the set that, for any set C, A ∪ B is a subset of C if and only if both A and B are subsets of C.

Intersection types and union types can be viewed in the same way. They are the product and coproduct in the category whose objects are types and whose morphisms are defined by subtyping relation.

Now we have two categories, one of sets and one of types. We want to define a functor between them. The most natural way is to map each type to its set of values. This functor is covariant, and preserves products and coproducts.

However, since we are talking about fields, we need to consider the functor that maps each type to its set of fields. You can check that this is indeed a functor. But it is contravariant, because subtypes actually have more fields than supertypes. It maps products to coproducts and coproducts to products. This is where it becomes counterintuitive.

$\endgroup$
3
$\begingroup$

Why do intersection types have more fields and union types have fewer fields?

Simply because it directly corresponds to set-theoretic unions and intersections. :)

If we interpret types as sets (not always possible or correct), then types specify sets of values (of this type) and we should compare the resulting sets of values.

As another answer already pointed out, intersection narrows the sets while union widens the set. Which was already evident from your examples: intersection had only one element — fewer than both original sets — while union had three elements — more than any original one.

Now, what happens with sets of values when we intersect and union types? In which set there are more values, in one with more fields or in one with fewer fields?

To make this comparison we need to note two facts. First, quite naturally, ∀ A, B: (A & B) ⊆ (A | B). Second, we understand a type like { foo: int } as all the values that has at least a field foo with the type int, they can have more fields with any types. That's how an intersection type {a: int, b: string} & {b: string, c: double} ≡ {a: int, b: string, c: double} is a subset of a union type {a: int, b: string} | {b: string, c: double} ≡ {b: string} — the more the fields the fewer the values.

So in the end it indeed works exactly as in set theory, you just need to look at sets — sets of values. And keep in mind structural subtyping — types specify which fields objects must have at least, not the exhaustive list of fields.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .