<p>I don't know a name for this, but it is extremely useful (see below). The point is that the tag carries information; the exact amount of information depends on how many tags there can be, as witnessed by the isomorphism you yourself exhibit.</p>
<p>The point is that information meaningful to the programmer, i.e. intensional information, can be encoded in the tags, which makes the resulting code much more meaningful and thus tends to be more maintainable. Code ought to be written as much for future programmers' understanding as for a computers' current consumption.</p>
<p>There this is particularly useful is when A is actually itself used to encode completely different information, so that to &quot;make sense&quot; of A, you need to know the tag. The most obvious is coordinate system (i.e. you can use 2 doubles to encode both cartesian and polar coordinates, but you sure need to know which one you have to interpret it properly!). <code>int</code> is almost worse, in that there's a plethora of (incompatible, incomparable) things that can be coded as an <code>int</code> but it would be non-sensible to do arithmetic on.</p>
<p>I realize that this is an odd answer on the cstheory SE! The 'interesting theoretical content' of the question has already been well answered by Martin Berger (and if you're interested in that part, I've written more than one paper on that theory). But I think the question you were asking seemed to lend itself best to how this can be useful <em>in practice</em>.</p>

CC BY-SA 4.0
2024-10-12T17:10:33.447Z
Indeed, thank you. I appreciate the concrete examples.
A. Bear
CC BY-SA 4.0
2024-10-11T17:16:17.907Z
2024-10-11T17:16:17.907Z
Jacques Carette
<p>A tagged union or disjoint union is a data structure that can contain a value of different types, depending on its tag. What if all the tags correspond to using the same type, say A?</p>
<p>To clarify the question, I'm asking about types such as A + A + A + A where each option has the same type. This could alternatively be represented as something like the type 4×A with members { (0, a₀), (1, a₁), (2, a₂), (3, a₃) }.</p>
<p>Is there in general any point to this? I'm asking because it seems like this would be the categorical dual of an array type (if you were to represent arrays as monotypical products.) Is this meaningful or just a mostly useless mathematical artifact only relevant to specific applications?</p>

CC BY-SA 4.0
2024-10-11T16:28:09.210Z
Not sure I'm answering your question, but your insight can be seen as a case of the question of *type isomorphisms*. Two types are isomorphic when we can convert between them without loosing information. Whether two types are isomorphic or not, depends on the ambient programming language, including the chosen notion of equality, such as β vs η-equality. See e.g. [*Axioms and Decidability for Type Isomorphism in the Presence of Sums*](https://arxiv.org/abs/1401.2567) as a starting point.
Martin Berger
CC BY-SA 4.0
2024-10-11T16:33:15.667Z
Type isomorphisms are useful if you can use a them to code up 'missing' type constructors. For example System F doesn't seem to have algebraic data types, but they can be coded up.
Martin Berger
CC BY-SA 4.0
2024-10-11T16:40:34.567Z
If you think carefully, you realise that under the hood all code gets executed by a conventional processor which has just one data type: a gigantic bitvector, and other data types emerge (in complicated ways) by type isomorphisms. (At least if we squint a bit.)
Martin Berger
CC BY-SA 4.0
2024-10-11T20:11:17.177Z
It can be seen as a special case of a co-power. An $n$-fold power of $A$ is $A^n$. An $n$-fold copower is $n \times A$.
Andrej Bauer
CC BY-SA 4.0
2024-10-12T17:12:18.047Z
Thank you @MartinBerger. I will look at that.
A. Bear
CC BY-SA 4.0
2024-10-12T17:13:20.593Z
@AndrejBauer This is interesting. Could you recommend anything as a basic introduction to co-powers? I'm not familiar. I see there's an nLab article but I haven't checked it yet.
A. Bear
CC BY-SA 4.0
2024-10-12T17:24:30.353Z
The nLab will do, take the category of sets enriched over itself, and interpret $n$ as a set with $n$ elements.
Andrej Bauer
<type-theory><pl.programming-languages><dependent-type><type-systems>
Is there a name for and a use for a tagged union where all the constructors take the exact same type?
A. Bear
# Is there a name for and a use for a tagged union where all the constructors take the exact same type?

(Asked by: username_0 on 2024-10-11)

A tagged union or disjoint union is a data structure that can contain a value of different types, depending on its tag. What if all the tags correspond to using the same type, say A?

To clarify the question, I'm asking about types such as A + A + A + A where each option has the same type. This could alternatively be represented as something like the type 4×A with members { (0, a₀), (1, a₁), (2, a₂), (3, a₃) }.

Is there in general any point to this? I'm asking because it seems like this would be the categorical dual of an array type (if you were to represent arrays as monotypical products.) Is this meaningful or just a mostly useless mathematical artifact only relevant to specific applications?

**Tags:** type-theory, pl.programming-languages, dependent-type, type-systems

> **Comments:**
> **username_1**: Not sure I'm answering your question, but your insight can be seen as a case of the question of *type isomorphisms*. Two types are isomorphic when we can convert between them without loosing information. Whether two types are isomorphic or not, depends on the ambient programming language, including the chosen notion of equality, such as β vs η-equality. See e.g. [*Axioms and Decidability for Type Isomorphism in the Presence of Sums*](https://arxiv.org/abs/1401.2567) as a starting point.  
> **username_1**: Type isomorphisms are useful if you can use a them to code up 'missing' type constructors. For example System F doesn't seem to have algebraic data types, but they can be coded up.  
> **username_1**: If you think carefully, you realise that under the hood all code gets executed by a conventional processor which has just one data type: a gigantic bitvector, and other data types emerge (in complicated ways) by type isomorphisms. (At least if we squint a bit.)  
> **username_2**: It can be seen as a special case of a co-power. An $n$-fold power of $A$ is $A^n$. An $n$-fold copower is $n \times A$.  
> **username_0**: Thank you @MartinBerger. I will look at that.  
> **username_0**: @AndrejBauer This is interesting. Could you recommend anything as a basic introduction to co-powers? I'm not familiar. I see there's an nLab article but I haven't checked it yet.  
> **username_2**: The nLab will do, take the category of sets enriched over itself, and interpret $n$ as a set with $n$ elements.  

---

## 1 answers

### Answer by username_3 on 2024-10-11. Score: 1 | Accepted answer

I don't know a name for this, but it is extremely useful (see below). The point is that the tag carries information; the exact amount of information depends on how many tags there can be, as witnessed by the isomorphism you yourself exhibit.

The point is that information meaningful to the programmer, i.e. intensional information, can be encoded in the tags, which makes the resulting code much more meaningful and thus tends to be more maintainable. Code ought to be written as much for future programmers' understanding as for a computers' current consumption.

There this is particularly useful is when A is actually itself used to encode completely different information, so that to "make sense" of A, you need to know the tag. The most obvious is coordinate system (i.e. you can use 2 doubles to encode both cartesian and polar coordinates, but you sure need to know which one you have to interpret it properly!). `int` is almost worse, in that there's a plethora of (incompatible, incomparable) things that can be coded as an `int` but it would be non-sensible to do arithmetic on.

I realize that this is an odd answer on the cstheory SE! The 'interesting theoretical content' of the question has already been well answered by username_1 (and if you're interested in that part, I've written more than one paper on that theory). But I think the question you were asking seemed to lend itself best to how this can be useful *in practice*.

> **Comments:**
> **username_0**: Indeed, thank you. I appreciate the concrete examples.  

---

