# Why quotient and subset on datatype ?

Why we need quotients and subsets of datatypes ?

One of the reaons is we could derive operations naturally. A simple example is the unordered pair. Define $R_{uo}$ as $(a, b)~R_{uo}~(b, a)$ for all $a, b \in \mathbf{A}$. Then, $(\mathbf{A} \times \mathbf{A}) / R_{uo}$ is the unordered pair.

Another example is $(\mathbb{N} \times \mathbb{N}) / R_{Z}$ where $(a, b)~R_{Z}~(c, d)$ if $a + d = b + c$. We could define plus, inverse, and products via ${[}(a, b){]} + {[}(c, d){]} = {[}(a + c, b + d){]}$, $-[(a, b)] = [(b, a)]$, and ${[}(a, b){]} * {[}(c, d){]} = {[}(a*c+b*d), (b*c+a*d){]}$ respectively. It could be shown that it’s isomorphic to $(\mathbb{Z}, +, *)$.

One more example is $\mathbf{Queue(A)}$. We could construct a queue by defining a equivalence relation $\mathbf{R}_q$ such that for all $xs_{1}, xs_{2}, ys_{1}, ys_{2} \in \mathbf{List(A)}$, $(xs_{1}, xs_{2})~R_q~(ys_{1}, ys_{2})$ if $xs_{1} + xs_{2}^{r} = ys_{1} + ys_{2}^{r}$ where $xs^{r}$ is ther reverse list of $xs$. Hence, the standard operations on $\mathbf{Queue(A)}$ like pop and push could be defined as ${[}(init(xs_{1}), xs_{2}){]}$ for $a$ is not null list ${[} \epsilon, (init(xs_{2}^{r}))^{r}]$ otherwise, and ${[}(xs_{1}, xs_{2}){]} \mapsto {[}(xs_{1}, (x :: xs_{2}) {]}$ respectively.

Likewise, we could describe many data structure as subsets. For example, the complete binary tree $(x, l, r)$ where $x$ is the root and $l, r$ are binary tree satisfying the complete properties. That is, $size(l) = size(r)$ and $l, r$ are complete. We could define the balenced tree similiarly.

In programming, we want to aviod some unsuitable case of the input like the input is outside of the English letters within ASCII code. We usually just check the input in the function or define a type (class, in OOP) which maps the type to the sub-type. In the later method, we have to define functions in the sub-type whether we have one in the super-type or not (thought, inheritance is a possible solution). In the former method, it looks irrelevant to the behavior(algorithm) of the function itself but we glue them together inside the same place.

Can we devise an algorithmtic method on type $\mathbf{A}$ and we could (almost) directly use it on its quotient and subset via a natural mapping, that is, given $f : A \rightarrow B$ and $g : B \rightarrow A$ , do we have

• $g_q : B \rightarrow (A/\sim)$, and
• $f_s : A' \subset A \rightarrow B$

by

• $\pi : A \rightarrow (A / \sim)$
• $\mathbf{i} : (A') \rightarrow A$

such that $f_q = \pi \circ g$ and $f_q = f \circ \mathbf{i}$ where $\pi$ is surjective and $\mathbf{i}$ is injective ($\mathbf{i}$ is just inclusion).