<p><strong><a href="https://en.wikipedia.org/wiki/Set_(abstract_data_type)" rel="nofollow noreferrer">Set theorhetical structures and operations</a> are quite fundamental and typically are either part of a languages standard library or built into it.
Given that types are fundamental to programming why do we not see abstract data types for type theorhetical structures and operations as <em>basic</em> (not necessarily first class) data types more commonly?</strong></p>
<p>Programs in typed languages are written in terms of types but this is not what I mean.
I mean manipulating data structures representing those types the way we might manipulate data structures representing sets.
In languages supporting higher kinded types this is like meta-programming but what about in languages that don't directly support higher kinded types?</p>
<p>We use types to operate on primitive types and values but types themselves are often baked into the language and entirely separate.
For example:</p>
<ul>
<li>We may have a <code>set</code> container with operations like <code>union</code>, <code>intersection</code> and <code>difference</code> (e.g. std::set in C++).</li>
</ul>
<p>For dealing with types we might have:</p>
<ul>
<li>values</li>
<li>types</li>
<li>basic operations on types</li>
<li>maybe terms, kinds and judgements as well</li>
</ul>
<p>The point is types here need not be types of the language implementing these data structures (though that might be convenient).</p>
<p>In fact libraries* for type theory seem rare in mainstream languages (I may be wrong). And yet you would think they were useful for implementing type systems for compilers and interpreters which is a very common use case.
If they are (or can be) foundational to maths and logic you would expect other use cases too.</p>
<p>Maybe support for types like this implies higher-kinded types? or homoiconicity?
So in fact this is more common in languages that support those.
Why are types less useful/common at the 'foundational level'?</p>
<p>Another reason might be because there isn't a necessarily a single definition of a type system. Do we want Hindler-Milner say or something than can handle dependent types? But to me that is a reason to have it as a separate set of data structures and functions independent of those in the base language.</p>
<p>If I am more specific and search for Hindley Milner type library there are a few hits like <a href="https://github.com/tomprimozic/type-systems/" rel="nofollow noreferrer">https://github.com/tomprimozic/type-systems/</a></p>
<p>Sets or types can be used as the foundation of maths. Given that types are the foundation of programming why aren't these kinds of library more common?</p>
<p>What are the trade offs?</p>
<hr />
<p>*I am not even sure what you would call such a library or interlinked set of data structures. &quot;type system library&quot; is not good search term perhaps there is something better. &quot;type checker&quot; is too use case specific and as a search term leads you to information about the type checkers for specific languages not libraries used to implement them.</p>
<hr />
<p>Put another way why do many programmers tend to think in terms of sets rather than types (or categories)?
Especially given the interrelatedness of types, sets and categories as put <a href="https://math.stackexchange.com/a/3802966/554439">here</a>:</p>
<blockquote>
<p>the different viewpoints are :</p>
<ul>
<li><p>Logic -&gt; Proof theory. There is an emphasis in manipulating proof as mathematical objects in your deductive system.</p>
</li>
<li><p>Type theory -&gt; algorithms. There is an emphasis in manipulating algorithms which are just a collection of instructions.</p>
</li>
<li><p>Category Theory -&gt; algebra. Here the emphasis is on manipulating algebraic objects using algebraic rules.</p>
</li>
</ul>
</blockquote>
<hr />
<p>For context this quesiton was inspired by thinking about this question <a href="https://languagedesign.stackexchange.com/questions/1566/why-intersection-types-have-more-fields-and-union-types-have-fewer-fields">Why intersection types have more fields and union types have fewer fields?</a>.</p>
<hr />
<p>I'm having a hard time expressing this effectively. My <a href="https://languagedesign.meta.stackexchange.com/questions/396/any-advice-on-how-to-fix-my-yo-yo-question?noredirect=1#comment807_396">related question on meta</a> tries to give an explanation of what this question is about and how it could be answered.
<a href="https://languagedesign.meta.stackexchange.com/questions/396/any-advice-on-how-to-fix-my-yo-yo-question?noredirect=1#comment807_396">Any advice on how to fix my yo-yo question?</a></p>

<types><data-structures>
Why are type theorhetic data structures rarer (than sets) if they are fundamental?
CC BY-SA 4.0
2023-06-21T10:01:36.447Z
This seems to be a question about prevalence of first-class (structural?) types for most of its running, but then at the end it's "put another way" as something about how programmers think, so I'm not sure what kind of answer it's getting at.
Michael Homer
CC BY-SA 4.0
2023-06-21T12:42:44.640Z
Its sort of a type theory quesiton. If programming languages are really about types how come as a group we prefer sets to types. Its a bit amorphous because I don't have a solid background in type theory and I'm not clear that my assertions are true a wider range of languages - particularly functional ones.
Bruce Adams
CC BY-SA 4.0
2023-06-21T12:49:46.290Z
Any suggestions on how to make myself clearer here before the close boot gets me?
Bruce Adams
CC BY-SA 4.0
2023-06-21T14:00:44.697Z
In fact I am dismayed to find that in my modest collection of books on compilers, computer science and related math few even have an entry for "type theory" in the index though some do mention lambda calculus.
Bruce Adams
CC BY-SA 4.0
2023-06-22T01:57:11.543Z
I'm curious what it would mean to declare a struct or union type at runtime in C, or what a `std::type` container in C++ would represent. If you mean to ask what are the pros and cons of [reflection](https://en.wikipedia.org/wiki/Reflective_programming), then the question could be a lot shorter. By the way, the other linked question has been reopened, after a discussion on meta.
kaya3
CC BY-SA 4.0
2023-06-22T02:23:23.277Z
"This is a product type in type theory. Typically a discriminated union or variant type in PL." -- Isn't a discriminated union a _sum type_? Product types are like structs and tuples.
Bbrk24
CC BY-SA 4.0
2023-06-22T02:57:09.277Z
@kaya3-supportthestrike I mean if we had a container like class that represented a "type" in the mathematical i.e. type theory - sense not the language sense. So its not reflection. A language or library might represent types as a data structure. The use cases would be more like writing a theorem prover or a type checker.
Bruce Adams
CC BY-SA 4.0
2023-06-22T03:00:32.927Z
@Bbrk24 correct I got my wires crossed.
Bruce Adams
CC BY-SA 4.0
2023-06-22T03:06:25.280Z
OK. Well, there is no "universal" type system that should be privileged by being represented in a language's standard library, unless it's that language's own type system (in which case, just have reflection). Even the idea that `{a: number} & {b: string}` is equal to `{a: number, b: string}` is a consequence of multiple choices that Typescript made in its own type system, and other type systems could make different choices. E.g. this intersection would be `never` if `{a: number, b: string}` weren't a subtype of `{a: number}`, and `{a: number}` wouldn't exist anyway in a nominal type system.
kaya3
CC BY-SA 4.0
2023-06-22T09:29:47.600Z
That is generally true of type systems in programming languages but you can still have structures to represent and implement some general aspects of type theory.
Bruce Adams
CC BY-SA 4.0
2023-06-22T15:40:12.150Z
Stop reopening with changing anything or changing something unrealted
Starship
CC BY-SA 4.0
2023-06-22T16:52:59.770Z
I too am surprised to see three reopen votes following someone adding some bullet points on my behalf. Perhaps they are actually responding to changes I made before the final close vote arrived? I would welcome edit suggestion that made this question better.
Bruce Adams
CC BY-SA 4.0
2023-06-22T16:56:51.680Z
The (hidden) timeline  feature supports by hypthesis https://languagedesign.stackexchange.com/posts/1601/timeline
Bruce Adams
CC BY-SA 4.0
2023-06-24T00:48:31.287Z
I encourage the OP to learn dependent type theories ;p
ice1000
CC BY-SA 4.0
2023-06-24T00:54:21.583Z
I expect my current side project to involve implementing both dependent and refinement types so that is quite likely.
Bruce Adams
CC BY-SA 4.0
2023-06-25T17:43:29.920Z
I got an upvote and a close vote in the same breath.
Bruce Adams
<p>I think you're confused a lot about the meaning of the word &quot;Set&quot;. In CS, Sets are special Lists with extra properties, as you pointed out. That's simply it. This is close to how they're defined in math, but not all!</p>
<ol>
<li>The usual constructions on Set are very difficult to deal with, compared to the usual constructions on types.</li>
</ol>
<p>For instance, the set of functions <code>Int → Int</code>, is defined to be the subset of the Cartesian product <code>R ∈ Int × Int</code>, where for every <code>a ∈ Int</code>, the set <code>{ (a, b) ∈ R | b ∈ Int }</code> is a singleton. This is called a functional relation. However, when we talk about types, the type of functions <code>Int → Int</code> is really the same as &quot;formulas that uses a variable <code>x : Int</code>, and the formula itself has type <code>Int</code>. This is more like a &quot;procedure&quot;, instead of a &quot;functional relation&quot;. In CS, computation is very important, and the type-theoretic function suits our needs better.</p>
<ol start="2">
<li>Set theory tends to encode everything with sets (for instance, natural numbers may accidentally have the same encoding as some functions).</li>
</ol>
<p>While in type theory, &quot;encoding&quot; a type with another type is just one way to do things -- it's more likely that we invent a new type and its instances are distinguished.</p>
<p>Back to the question. Why are type-theoretic structures rarer? I think it's quite the opposite! Type-theoretic structures are essential in PLs. Many constructions in set theory has their version in type theory, such as disjointed unions, Cartesian products, initial algebras of polynomial functors, etc.</p>
<p>Also, I'd like to correct one more sentence:</p>
<blockquote>
<p>there isn't a necessarily a single definition of a type system</p>
</blockquote>
<ol>
<li>There isn't a standard set theory either. ZFC/ZF is very popular, but there are much more than that!</li>
<li>A multi-modal type theory can potentially be a unifying type theory that can extend to tons of interesting type theories. See <a href="https://hott.github.io/HoTT-2023/slides/shulman.pdf" rel="nofollow noreferrer">slides</a>.</li>
</ol>

CC BY-SA 4.0
2023-06-23T23:56:46.117Z
2023-06-23T23:56:46.117Z
ice1000
CC BY-SA 4.0
2023-06-25T08:04:34.023Z
Do you know of a type checker that implements multi-mode type theory?
Bruce Adams
CC BY-SA 4.0
2023-06-25T08:34:57.600Z
@BruceAdams Not that I'm aware of, but Agda has a flat modality for you to add axioms on it.
ice1000
# Why are type theorhetic data structures rarer (than sets) if they are fundamental?
Posted by: username_0 on 2023-06-21
**[Set theorhetical structures and operations](https://en.wikipedia.org/wiki/Set_(abstract_data_type)) are quite fundamental and typically are either part of a languages standard library or built into it.
Given that types are fundamental to programming why do we not see abstract data types for type theorhetical structures and operations as *basic* (not necessarily first class) data types more commonly?**

Programs in typed languages are written in terms of types but this is not what I mean.
I mean manipulating data structures representing those types the way we might manipulate data structures representing sets.
In languages supporting higher kinded types this is like meta-programming but what about in languages that don't directly support higher kinded types?

We use types to operate on primitive types and values but types themselves are often baked into the language and entirely separate.
For example:

* We may have a `set` container with operations like `union`, `intersection` and `difference` (e.g. std::set in C++).

For dealing with types we might have:

* values
* types
* basic operations on types
* maybe terms, kinds and judgements as well

The point is types here need not be types of the language implementing these data structures (though that might be convenient).

In fact libraries\* for type theory seem rare in mainstream languages (I may be wrong). And yet you would think they were useful for implementing type systems for compilers and interpreters which is a very common use case.
If they are (or can be) foundational to maths and logic you would expect other use cases too.

Maybe support for types like this implies higher-kinded types? or homoiconicity?
So in fact this is more common in languages that support those.
Why are types less useful/common at the 'foundational level'?

Another reason might be because there isn't a necessarily a single definition of a type system. Do we want Hindler-Milner say or something than can handle dependent types? But to me that is a reason to have it as a separate set of data structures and functions independent of those in the base language.

If I am more specific and search for Hindley Milner type library there are a few hits like <https://github.com/tomprimozic/type-systems/>

Sets or types can be used as the foundation of maths. Given that types are the foundation of programming why aren't these kinds of library more common?

What are the trade offs?

---

\*I am not even sure what you would call such a library or interlinked set of data structures. "type system library" is not good search term perhaps there is something better. "type checker" is too use case specific and as a search term leads you to information about the type checkers for specific languages not libraries used to implement them.

---

Put another way why do many programmers tend to think in terms of sets rather than types (or categories)?
Especially given the interrelatedness of types, sets and categories as put [here](https://math.stackexchange.com/a/3802966/554439):

> the different viewpoints are :
>
> * Logic -> Proof theory. There is an emphasis in manipulating proof as mathematical objects in your deductive system.
> * Type theory -> algorithms. There is an emphasis in manipulating algorithms which are just a collection of instructions.
> * Category Theory -> algebra. Here the emphasis is on manipulating algebraic objects using algebraic rules.

---

For context this quesiton was inspired by thinking about this question [Why intersection types have more fields and union types have fewer fields?](https://languagedesign.stackexchange.com/questions/1566/why-intersection-types-have-more-fields-and-union-types-have-fewer-fields).

---

I'm having a hard time expressing this effectively. My [related question on meta](https://languagedesign.meta.stackexchange.com/questions/396/any-advice-on-how-to-fix-my-yo-yo-question?noredirect=1#comment807_396) tries to give an explanation of what this question is about and how it could be answered.
[Any advice on how to fix my yo-yo question?](https://languagedesign.meta.stackexchange.com/questions/396/any-advice-on-how-to-fix-my-yo-yo-question?noredirect=1#comment807_396)
**Tags:** types data-structures
> **Comments:**
> **username_1**: This seems to be a question about prevalence of first-class (structural?) types for most of its running, but then at the end it's "put another way" as something about how programmers think, so I'm not sure what kind of answer it's getting at.  
> **username_0**: Its sort of a type theory quesiton. If programming languages are really about types how come as a group we prefer sets to types. Its a bit amorphous because I don't have a solid background in type theory and I'm not clear that my assertions are true a wider range of languages - particularly functional ones.  
> **username_0**: Any suggestions on how to make myself clearer here before the close boot gets me?  
> **username_0**: In fact I am dismayed to find that in my modest collection of books on compilers, computer science and related math few even have an entry for "type theory" in the index though some do mention lambda calculus.  
> **username_2**: I'm curious what it would mean to declare a struct or union type at runtime in C, or what a `std::type` container in C++ would represent. If you mean to ask what are the pros and cons of [reflection](https://en.wikipedia.org/wiki/Reflective_programming), then the question could be a lot shorter. By the way, the other linked question has been reopened, after a discussion on meta.  
> **username_3**: "This is a product type in type theory. Typically a discriminated union or variant type in PL." -- Isn't a discriminated union a _sum type_? Product types are like structs and tuples.  
> **username_0**: @kaya3-supportthestrike I mean if we had a container like class that represented a "type" in the mathematical i.e. type theory - sense not the language sense. So its not reflection. A language or library might represent types as a data structure. The use cases would be more like writing a theorem prover or a type checker.  
> **username_0**: @Bbrk24 correct I got my wires crossed.  
> **username_2**: OK. Well, there is no "universal" type system that should be privileged by being represented in a language's standard library, unless it's that language's own type system (in which case, just have reflection). Even the idea that `{a: number} & {b: string}` is equal to `{a: number, b: string}` is a consequence of multiple choices that Typescript made in its own type system, and other type systems could make different choices. E.g. this intersection would be `never` if `{a: number, b: string}` weren't a subtype of `{a: number}`, and `{a: number}` wouldn't exist anyway in a nominal type system.  
> **username_0**: That is generally true of type systems in programming languages but you can still have structures to represent and implement some general aspects of type theory.  
> **username_4**: Stop reopening with changing anything or changing something unrealted  
> **username_0**: I too am surprised to see three reopen votes following someone adding some bullet points on my behalf. Perhaps they are actually responding to changes I made before the final close vote arrived? I would welcome edit suggestion that made this question better.  
> **username_0**: The (hidden) timeline  feature supports by hypthesis https://languagedesign.stackexchange.com/posts/1601/timeline  
> **username_5**: I encourage the OP to learn dependent type theories ;p  
> **username_0**: I expect my current side project to involve implementing both dependent and refinement types so that is quite likely.  
> **username_0**: I got an upvote and a close vote in the same breath.  
---
## 1 answers
### Answer by username_5 on 2023-06-23. Score: 3
I think you're confused a lot about the meaning of the word "Set". In CS, Sets are special Lists with extra properties, as you pointed out. That's simply it. This is close to how they're defined in math, but not all!

1. The usual constructions on Set are very difficult to deal with, compared to the usual constructions on types.

For instance, the set of functions `Int → Int`, is defined to be the subset of the Cartesian product `R ∈ Int × Int`, where for every `a ∈ Int`, the set `{ (a, b) ∈ R | b ∈ Int }` is a singleton. This is called a functional relation. However, when we talk about types, the type of functions `Int → Int` is really the same as "formulas that uses a variable `x : Int`, and the formula itself has type `Int`. This is more like a "procedure", instead of a "functional relation". In CS, computation is very important, and the type-theoretic function suits our needs better.

2. Set theory tends to encode everything with sets (for instance, natural numbers may accidentally have the same encoding as some functions).

While in type theory, "encoding" a type with another type is just one way to do things -- it's more likely that we invent a new type and its instances are distinguished.

Back to the question. Why are type-theoretic structures rarer? I think it's quite the opposite! Type-theoretic structures are essential in PLs. Many constructions in set theory has their version in type theory, such as disjointed unions, Cartesian products, initial algebras of polynomial functors, etc.

Also, I'd like to correct one more sentence:

> there isn't a necessarily a single definition of a type system

1. There isn't a standard set theory either. ZFC/ZF is very popular, but there are much more than that!
2. A multi-modal type theory can potentially be a unifying type theory that can extend to tons of interesting type theories. See [slides](https://hott.github.io/HoTT-2023/slides/shulman.pdf).
> **Comments:**
> **username_0** (2023-06-25): Do you know of a type checker that implements multi-mode type theory?  
> **username_5** (2023-06-25): @BruceAdams Not that I'm aware of, but Agda has a flat modality for you to add axioms on it.  
---
