<p>Is there a known algebraic structure over set of Types (however they are defined) which is equipped with:</p>
<ol>
<li>commutative and associative product operation for building product types from simpler types, and</li>
<li>relation of inheritance, ie. relation which shows that certain product types share factors (are build up from common simpler types).</li>
</ol>
<p>Cartesian product is not practical as the operation (1) because it is not commutative and associative (though results are <a href="https://math.stackexchange.com/questions/1202223/associativity-of-cartesian-product-and-nested-ordered-n-tuples">isomorphic</a>).</p>
<hr />
<p><strong>Detailed explanation</strong></p>
<p>I'm interested in modeling notions of class and structure from computer programming in algebraic manner - meaning to introduce a set of rules which can be used to calculate with classes and structures.</p>
<p>Let's define following structures in <span class="math-container">$C$</span>:</p>
<pre><code>struct PhysicalCharacteristics {
   height: int;
   width: int;
}

struct Human {
   height: int;
   width: int;
   name: string;
   age: double;
}

struct Human2 {
   physique: PhysicalCharacteristics;
   name: string;
   age: double;
}
</code></pre>
<p>I am looking for an algebra which would allow me to express statements like these:
<span class="math-container">\begin{eqnarray}
\text{PhysicalCharacteristics}&amp;=&amp;\text{int}^{\{\text{width}\}} \times \text{int}^{\{\text{height}\}}\\
\text{Human}&amp;=&amp;\text{int}^{\{\text{width}\}} \times \text{int}^{\{\text{height}\}} \times \text{string}^{\{\text{name}\}} \times \text{double}^{\{\text{age}\}}\\
&amp;=&amp;\text{PhysicalCharacteristics} \times \text{string}^{\{\text{name}\}} \times \text{double}^{\{\text{age}\}}\\
\text{Human2}&amp;=&amp; \text{PhysicalCharacteristics}^{\{\text{physique}\}} \times \text{string}^{\{\text{name}\}} \times \text{double}^{\{\text{name}\}}\\
&amp;=&amp;(\text{int}^{\{\text{width}\}} \times \text{int}^{\{\text{height}\}})^{\{\text{physique}\}} \times \text{string}^{\{\text{name}\}} \times \text{double}^{\{\text{name}\}}
\end{eqnarray}</span></p>
<p>and where <span class="math-container">$\times$</span> is commutative and associative and where we can formally establish a notion that type <span class="math-container">$\text{PhysicalCharacteristics}$</span> is a subtype of <span class="math-container">$\text{Human}$</span>.</p>

CC BY-SA 4.0
2023-09-03T11:04:00.190Z
The 'product'  sounds a bit like union in sets or multisets. So the algebraic structure might be some kind of lattice?
Martin Berger
CC BY-SA 4.0
2023-09-03T17:05:19.780Z
I will ask again here: are we allow to "multiply" products that share a label? If so, what is the result?
Andrej Bauer
CC BY-SA 4.0
2023-09-04T10:17:10.733Z
Multiplying products that share labels may be **algebraically** meaningful depending on how the algebra is established. However, as we want the result of the operation to represent valid product type (or even a class or a structure in real-life computer program) we may introduce additional constraints which forbid such operations.

I am wondering if you know any attempt to establish such algebra.
Bogdan Nikolic
<type-theory><algebra>
Product types: algebraic structure for modeling product types with commutative and associative product operation
Bogdan Nikolic
# Product types: algebraic structure for modeling product types with commutative and associative product operation

(Asked by: username_0 on 2023-09-03)

Is there a known algebraic structure over set of Types (however they are defined) which is equipped with:

commutative and associative product operation for building product types from simpler types, and
relation of inheritance, ie. relation which shows that certain product types share factors (are build up from common simpler types).

Cartesian product is not practical as the operation (1) because it is not commutative and associative (though results are isomorphic).

Detailed explanation
I'm interested in modeling notions of class and structure from computer programming in algebraic manner - meaning to introduce a set of rules which can be used to calculate with classes and structures.
Let's define following structures in $C$:
struct PhysicalCharacteristics {
   height: int;
   width: int;
}

struct Human {
   height: int;
   width: int;
   name: string;
   age: double;
}

struct Human2 {
   physique: PhysicalCharacteristics;
   name: string;
   age: double;
}

I am looking for an algebra which would allow me to express statements like these:
\begin{eqnarray}
\text{PhysicalCharacteristics}&=&\text{int}^{\{\text{width}\}} \times \text{int}^{\{\text{height}\}}\\
\text{Human}&=&\text{int}^{\{\text{width}\}} \times \text{int}^{\{\text{height}\}} \times \text{string}^{\{\text{name}\}} \times \text{double}^{\{\text{age}\}}\\
&=&\text{PhysicalCharacteristics} \times \text{string}^{\{\text{name}\}} \times \text{double}^{\{\text{age}\}}\\
\text{Human2}&=& \text{PhysicalCharacteristics}^{\{\text{physique}\}} \times \text{string}^{\{\text{name}\}} \times \text{double}^{\{\text{name}\}}\\
&=&(\text{int}^{\{\text{width}\}} \times \text{int}^{\{\text{height}\}})^{\{\text{physique}\}} \times \text{string}^{\{\text{name}\}} \times \text{double}^{\{\text{name}\}}
\end{eqnarray}
and where $\times$ is commutative and associative and where we can formally establish a notion that type $\text{PhysicalCharacteristics}$ is a subtype of $\text{Human}$.

**Tags:** type-theory, algebra
> **Comments:**
> **username_1**: The 'product'  sounds a bit like union in sets or multisets. So the algebraic structure might be some kind of lattice?  
> **username_2**: I will ask again here: are we allow to "multiply" products that share a label? If so, what is the result?  
> **username_0**: Multiplying products that share labels may be **algebraically** meaningful depending on how the algebra is established. However, as we want the result of the operation to represent valid product type (or even a class or a structure in real-life computer program) we may introduce additional constraints which forbid such operations.  I am wondering if you know any attempt to establish such algebra.  

---

## 0 answers

