Franklin's Notes


Casting in categories

Note: this note is all about stuff that I've made up myself for purposes of exploration, not read from any authoritative source. Proceed with skepticism.

Given an inclusion subcategory $\mathsf{C}'$ of a category $\mathsf{C}$, let us say that a morphism $\mathfrak{c}:X\to Y$ of $\mathsf{C}$ is a cast with respect to $\mathsf{C}'$ if and only if $X,Y\in\mathsf{C}'$ and the following diagram commutes for all objects $I\in\mathsf{C}'$ and morphisms $\iota_X,\iota_Y\in\mathsf{C}'$ with $\iota_X:I\to X$ and $\iota_Y:I\to Y$:

This is my attempt at categorically characterizing what type casting in programming languages like C attempts to accomplish: sending elements of one type (i.e. object) to elements of another type (object) with the goal of sending each element of one type to its "best fit" in the other type. With this is mind, if some elements of the two types are identified are being "the same" or "representing the same quantity" - such as 14.0 as a float and 14 as an int - then any type cast between the two types should send these values to each other.

Because it's a matter of choice which elements are to be identified with each other between types, casts are relative to a particular inclusion subcategory , which can be thought of as specifying which types are subtypes of others. As per the definition, any cast between types with a common subtype should preserve the inclusion maps of that subtype. For instance, we would like any type cast between 32-bit unsigned ints and 32-bit signed ints to preserve 16-bit unsigned ints.

Here are some elementary properties of casts, some of which follow from the properties of inclusion subcategories :

The category $\mathsf{C}$ determines what sort of structure we would like our type casts to preserve. For instance, we can use this setup to show that there is no nice way of casting 16-bit integers to 8-bit integers in wuch a way that preserves their structure as an additive group.

Remark 1. In the category $\mathsf{Group}$ with an inclusion subcategory containing $\mathbb Z_{2^8}$ and $\mathbb Z_{2^{16}}$, there is no cast $\mathfrak{c}:\mathbb Z_{2^{16}}\to \mathbb Z_{2^8}$.

Proof. Let $\iota$ be a monomorphism in an inclusion subcategory of $\mathsf{Group}$. Suppose that $\mathfrak{c}:\mathbb Z_{2^{16}}\to \mathbb Z_{2^8}$ is a cast, so that the following diagram commutes:

We have that $\iota(0)=0$ immediately. Furthermore, since $2^8 x = 0$ for all $x\in\mathbb Z_{2^8}$, it follows that for all $x\in\mathbb Z_{2^8}$, meaning that all elements of $\mathbb Z_{2^{16}}$ in the image of $\iota$ are in the subgroup $2^{8}\mathbb Z_{2^{16}}$. Let $x$ be a nonzero element of the image of $\iota$, so that $2^8 y=x$ for some $y\in \mathbb Z_{2^{16}}$. Then we have that but all elements of $\mathbb Z_{2^8}$ have order dividing $2^8$, so it is not possible for $\mathfrak{c}(y)\in \mathbb Z_{2^8}$ to satisfy the above inequality! $\blacksquare$

However, if we consider bitwise addition (via XOR) rather than integer addition modulo large powers of $2$, type casting becomes not only possible, but very flexible:

Remark 2. In the category $\mathsf{Group}$ with an inclusion subcategory containing $\mathbb Z_{2}^8$ and $\mathbb Z_{2}^{16}$, there are many possible casts $\mathfrak{c}:\mathbb Z_{2}^{16}\to \mathbb Z_{2}^8$.

Examples.
1. Let $\iota:\mathbb Z_{2}^8\rightarrowtail\mathbb Z_{2}^{16}$ map each 8-tuple to a 16-tuple by appending $8$ zeroes to the end, and let $\mathfrak{c}:\mathbb Z_{2}^{16}\to \mathbb Z_{2}^8$ map each 16-tuple to an 8-tuple by chopping off the last $8$ bits.
2. Modify the previous example by having $\iota$ append zeroes to the beginning and having $\mathfrak{c}$ chop them off from the beginning.
3. Let $\iota:\mathbb Z_{2}^8\rightarrowtail\mathbb Z_{2}^{16}$ map each 8-tuple to a 16-tuple by appending it to a copy of itself. There are several different casts $\mathfrak{c}:\mathbb Z_{2}^{16}\to \mathbb Z_{2}^8$, such as the one that chops off the last $8$ bits, the one that chops off the first $8$ bits, and the one that chops off the first $4$ and last $4$ bits.
4. Let $\iota:\mathbb Z_{2}^8\rightarrowtail\mathbb Z_{2}^{16}$ map each 8-tuple to a 16-tuple by appending to that 8-tuple $7$ zeroes and an additional bit equal to the XOR of the $8$ bits from the original tuple. What are the possible casts for this inclusion subcategory?
$\blacksquare$

We could also consider 8-bit and 16-bit unsigned ints as elements of $\mathsf{Poset}$ rather than $\mathsf{Group}$. But I'll leave that for another day...

category-theory

computer-science

back to home page