<p>There's a question that's been bothering me.</p>
<p>I even implemented it backwards when I implemented the type system for my language.</p>
<p><strong>Why do intersection types have more fields and union types have fewer fields?</strong></p>
<p>In set theory,</p>
<pre><code>{a, b} &amp; {b, c} =&gt; {b}
{a, b} | {b, c} =&gt; {a, b, c}
</code></pre>
<p>Whereas in type theory,</p>
<pre><code>type P = {a: int, b: int}
type Q = {b: int, c: int}

P &amp; Q = {a: int, b: int, c: int}
P | Q = {b: int}
</code></pre>
<p>In set theory, <code>A</code> is a subset of <code>B</code> if all the elements in <code>A</code> are in <code>B</code>.</p>
<p>In type theory, <code>B</code> is a subtype of <code>A</code> if all the fields in <code>A</code> are in <code>B</code>.</p>
<hr />
<p>I know types can't be seen as sets, but I still can't understand why it's all the other way around.</p>
<p>Can anybody give a consistent explanation to answer my doubts, thanks!</p>

<types><type-theory>
Why intersection types have more fields and union types have fewer fields?
CC BY-SA 4.0
2023-06-19T16:20:49.180Z
I have a tingly feeling this is better for CS.SE
Seggan
CC BY-SA 4.0
2023-06-19T18:28:39.717Z
This is answered (in the context of Typescript) on Stack Overflow here: https://stackoverflow.com/q/38855908/12299000
kaya3
CC BY-SA 4.0
2023-06-19T18:43:54.257Z
I've created [a post on meta](https://languagedesign.meta.stackexchange.com/q/368/89) to discuss whether questions purely about type theory should be on-topic here.
kaya3
CC BY-SA 4.0
2023-06-21T08:17:52.130Z
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?
Bruce Adams
CC BY-SA 4.0
2023-06-21T09:54:13.420Z
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.
Michael Homer
<p>There is an extremely short way to answer your question.
In the question, you said the following:</p>
<blockquote>
<p>In set theory,</p>
<pre><code>{a, b} &amp; {b, c} =&gt; {b}
{a, b} | {b, c} =&gt; {a, b, c}
</code></pre>
<p>Whereas in type theory,</p>
<pre><code>type P = {a: int, b: int}
type Q = {b: int, c: int}
P &amp; Q = {a: int, b: int, c: int}
P | Q = {b: int}
</code></pre>
</blockquote>
<p>Note that in <code>{a, b}</code>, <code>a</code> and <code>b</code> are <em>elements</em> of the set, meaning that <code>a ∈ {a, b}</code> <em>and</em> <code>b ∈ {a, b}</code>. However, in <code>{a: int, b: int}</code>, <code>a</code> and <code>b</code> are fields, which does <em>not</em> mean that <code>a : int ∈ {a: int, b: int}</code>! The meaning of <code>a : int</code> here is that if <code>x ∈ {a: int, b: int}</code>, then <code>x.a : int</code>.</p>
<p>So it's reasonable that the arrows are backwards.</p>

CC BY-SA 4.0
2023-06-24T00:41:18.973Z
2023-06-24T00:41:18.973Z
ice1000
<p>Here is my understanding from the perspective of category theory.</p>
<p>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.</p>
<p>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.</p>
<p>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.</p>
<p>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 <em><strong>contravariant</strong></em>, because subtypes actually have more fields than supertypes. It maps products to coproducts and coproducts to products. This is where it becomes counterintuitive.</p>

CC BY-SA 4.0
2023-06-20T01:46:48.160Z
2023-06-20T01:46:48.160Z
alephalpha
<p>Fields on a structural type are not analogous to elements of a set.</p>
<p><code>type P = {a: int, b: int}</code> doesn't mean that a value of type <code>P</code> is either <code>a</code> or <code>b</code>, it means it has to have fields <code>a</code> <em>and</em> <code>b</code>. You can see a field in this way as a constraint on a type. If you want to see <code>P</code> as a set, you can describe it like this pseudo-code: <code>type P = {t forall t if t.a: int &amp; t.b: int}</code></p>
<p>In this notation: <code>P &amp; Q == {t forall t if (t.a: int &amp; t.b: int) &amp; (t.b: int &amp; t.c: int)} == {t forall t if t.a: int &amp; t.b: int &amp; t.c: int}</code>.</p>
<p>There are more constraints on values of type <code>P &amp; Q</code> than there are on values of type <code>P</code>, and thus more fields, but less values, in the sense that the set of values which have type <code>P &amp; Q</code> is a subset of the set of values which have type <code>P</code>.</p>
<p>On the other hand: <code>P | Q == {t forall t if (t.a: int &amp; t.b: int) | (t.b: int &amp; t.c: int)} == {t forall t if (t.a: int | t.c: int) &amp; (t.b: int | t.b: int)} == {t forall t if (t.a: int | t.c: int) &amp; t.b: int}</code>. Since a structural type system may not be able to express types like &quot;either has a field <code>a: int</code> or a field <code>c: int</code>&quot; and having those types tends not to be very useful anyway, it may just drop that constraint and make <code>P | Q == {t forall t if t.b: int}</code></p>
<p>There are less constraints on values of type <code>P | Q</code> than there are on values of type <code>P</code>, and thus less fields, but more values, in the sense that the set of values which have type <code>P | Q</code> is a superset of the set of values which have type <code>P</code>.</p>
<p>So while subtypes are not exactly equivalent to subsets, they are analogous and definitely not &quot;the other way around&quot;.</p>
<p>Finally, when comparing <code>{a, b}</code> and <code>{a: int, b: int}</code>, don't be mislead by the visual similarities. The matching tokens <code>{</code>, <code>a</code>, <code>,</code>, <code>b</code> and <code>}</code> mean different things in both notations, like the way a <code>*</code> means very different things when used in <code>int*</code> versus <code>2 * 3</code> versus <code>.*</code>.</p>

CC BY-SA 4.0
2023-06-19T22:38:39.420Z
2023-06-20T00:06:57.643Z
2023-06-20T00:06:57.643Z
Jasmijn
<p>Intersection is a verb (well technically the nominalization of a verb), so its meaning depends on what object it is being applied to.</p>
<p>In structurally typed languages, the object that the verb is being applied to, is the set of all values/objects that satisfies the type. Note that the size of the set of objects satisfying the type, gets smaller as more members increase.</p>
<p>More constraints == a restriction, as you should expect from an intersection.</p>

CC BY-SA 4.0
2024-06-24T02:34:02.297Z
2024-06-24T21:38:08.217Z
2024-06-24T21:38:08.217Z
Tom Huntington
CC BY-SA 4.0
2024-06-24T02:39:53.977Z
In a nominally typed language, should different names be chosen??? I need to think about this...
Tom Huntington
CC BY-SA 4.0
2024-06-24T13:19:40.727Z
"the object that the verb is being applied to the set of all values/objects that satisfies the type" I feel there's a word missing here. Perhaps "... being applied to **is** the set ..."?
MisterMiyagi
CC BY-SA 4.0
2024-06-24T18:01:37.127Z
"Intersection" is a noun; "intersect" is a verb.
kaya3
<blockquote>
<p>Why do intersection types have more fields and union types have fewer fields?</p>
</blockquote>
<p>Simply because it directly corresponds to set-theoretic unions and intersections. :)</p>
<p>If we interpret types as sets (not always possible or correct), then types specify sets of <em>values</em> (of this type) and we should compare the resulting sets of values.</p>
<p>As another answer already pointed out, intersection <em>narrows</em> the sets while union <em>widens</em> 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.</p>
<p>Now, what happens with <em>sets of values</em> when we intersect and union types? In which set there are more values, in one with more fields or in one with fewer fields?</p>
<p>To make this comparison we need to note two facts. First, quite naturally, ∀ A, B: (A &amp; B) ⊆ (A | B). Second, we understand a type like <code>{ foo: int }</code> as all the values that has <em>at least</em> a field <code>foo</code> with the type <code>int</code>, they can have more fields with any types. That's how an intersection type <code>{a: int, b: string} &amp; {b: string, c: double} ≡ {a: int, b: string, c: double}</code> is a <em>subset</em> of a union type <code>{a: int, b: string} | {b: string, c: double} ≡ {b: string}</code> — the more the fields the fewer the values.</p>
<p>So in the end it indeed works exactly as in set theory, you just need to look at <em>sets</em> — sets of values. And keep in mind <em>structural subtyping</em> — types specify which fields objects must have <em>at least</em>, not the exhaustive list of fields.</p>

CC BY-SA 4.0
2023-06-20T08:27:37.760Z
2023-06-20T08:27:37.760Z
Alex Chichigin
<p><strong>Think about it like this:</strong></p>
<p>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.</p>
<p>This is pretty intuitive, so let's move on to type theory.</p>
<p>Let's use your example:</p>


<pre class="lang-java prettyprint-override"><code>type P = {a: int, b: int}
type Q = {b: int, c: int}
</code></pre>
<p>In type theory, when you take the union of types <code>P</code> and <code>Q</code>, the only thing you <em>know</em> for sure is that you will have the <code>b</code> field. You can't be sure if you have the <code>a</code> field or the <code>c</code> field. This means that:</p>
<pre class="lang-java prettyprint-override"><code>P | Q = {b: int}
</code></pre>
<p>Also, when you take the intersection, the new type has all the fields because  it is necessary that it can be converted to both <code>P</code> and <code>Q</code>. If it only had the <code>b</code> field, you couldn't convert it to either <code>P</code> or <code>Q</code>. This means that:</p>
<pre class="lang-java prettyprint-override"><code>P &amp; Q = {a: int, b: int, c: int}
</code></pre>
<p><strong>In conclusion</strong>, 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 <code>P | Q</code> could be from either <code>P</code> or <code>Q</code>, so we can't assume anything about the uncommon fields. An object of type <code>P &amp; Q</code> will have all of the fields of <code>P</code> and all of the fields of <code>Q</code> because it can be converted to either <code>P</code> or <code>Q</code>.</p>
<p>Also, about the subtypes/supertypes thing, think of it as &quot;<code>B</code> is a subtype of <code>A</code> if you can convert an object of type <code>B</code> to type <code>A</code>&quot;. This means that all the fields in <code>A</code> are also in <code>B</code>.</p>

CC BY-SA 4.0
2023-06-19T16:05:11.677Z
2023-06-19T16:05:11.677Z
The Thonnu
# Why intersection types have more fields and union types have fewer fields?
Posted by: username_0 on 2023-06-19
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!
**Tags:** types type-theory
> **Comments:**
> **username_1**: I have a tingly feeling this is better for CS.SE  
> **username_2**: This is answered (in the context of Typescript) on Stack Overflow here: https://stackoverflow.com/q/38855908/12299000  
> **username_2**: I've created [a post on meta](https://languagedesign.meta.stackexchange.com/q/368/89) to discuss whether questions purely about type theory should be on-topic here.  
> **username_3**: 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?  
> **username_4**: 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.  
---
## 6 answers
### Answer by username_11 on 2023-06-19. Score: 6 | Accepted answer
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.
---
### Answer by username_5 on 2023-06-24. Score: 6
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.
---
### Answer by username_6 on 2023-06-20. Score: 3
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.
---
### Answer by username_7 on 2023-06-19. Score: 3
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 `.*`.
---
### Answer by username_10 on 2023-06-20. Score: 3
> 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.
---
### Answer by username_8 on 2024-06-24. Score: 0
Intersection is a verb (well technically the nominalization of a verb), so its meaning depends on what object it is being applied to.

In structurally typed languages, the object that the verb is being applied to, is the set of all values/objects that satisfies the type. Note that the size of the set of objects satisfying the type, gets smaller as more members increase.

More constraints == a restriction, as you should expect from an intersection.
> **Comments:**
> **username_8** (2024-06-24): In a nominally typed language, should different names be chosen??? I need to think about this...  
> **username_9** (2024-06-24): "the object that the verb is being applied to the set of all values/objects that satisfies the type" I feel there's a word missing here. Perhaps "... being applied to **is** the set ..."?  
> **username_2** (2024-06-24): "Intersection" is a noun; "intersect" is a verb.  
---
