Type Algebra and You, Part 1: Basics

Counting and arithmetic on finite types.

When learning a new programming language, its type system can be a point of contention. Dynamic systems are fairly common in scripting languages like Python and JavaScript, which makes them great for beginners. However, it appears to be a general principle that imposing type-strictness (staticness, strength, …) will generally allow errors to be caught before someone discovers them. To the computer, types are illusory, but they are not to the human.

Beyond their use in programming languages, mathematicians also work with types in a purely abstract way (putting aside the fact that “type” is already an abstract concept). Types bear some resemblance to sets, yet in other ways resemble numbers and can be manipulated via algebra. In the following couple of posts, I would like to investigate these resemblances.

This post will primarily focus on making the numerical resemblance clear, since it is more fundamental and everyone tends to agree on how to define arithmetic. Since it can be difficult to appreciate relatively simple expressions without retreating back to a programming language, I will use Haskell to demonstrate some interesting consequences of this higher-kinded world.

Starting from Square Zero

If we can treat types as numbers, then we best start with 0. We interpret this as the number of possible values which populate the type. There are exactly zero possible values of type 0, i.e., there is no way to construct a value with this type.

In Haskell, this type is referred to as Void. Here is a paraphrased definition from (an earlier version of) Data.Void:

newtype Void = V Void

In other words, V, the only constructor of Void, requires already having a Void. This requires infinite regress, so it is logically impossible.

Wait a minute, “only constructor”?

Notice that Void’s constructor, V, has type Void -> Void. This type, unlike Void, is definitely populated. It resembles the empty function from set theory, of which there is only one for the empty set. This means that by constructing an empty type, we’ve also constructed a singleton.

Haskell already has a type with only one possible value: ()¹, with its only value written identically. Can we prove that this is somehow the “same” type as Void -> Void? Of course! Remember, Haskell is a functional language. Therefore, we should focus on writing functions between the two types.

-- Haskell actually complains that you're trying to pattern-match
--   based on the constructor if you specify `V` on the LHS.
toUnit :: (Void -> Void) -> ()
toUnit _ = ()

fromUnit :: () -> (Void -> Void)
fromUnit () = V

The “to” and “from” in the names suggests that if we do one followed by the other, we should end up where we started. Or, in the language of functions, the composition of the functions is the identity.

fromUnit . toUnit == (id :: (Void -> Void) -> (Void -> Void))
toUnit . fromUnit == (id :: () -> ())

In other words, we can reversibly map values from one type to the other (and vice versa). If such functions (also known as bijections) exist, then the types are isomorphic.

Poly-iso-morphisms

We can assemble pairs of functions resembling this structure into a typeclass in Haskell:

class Isomorphism a b where
  -- Isomorphisms must define these two polymorphic functions
  toA :: (b -> a)
  toB :: (a -> b)

  -- And these functions, which *could* be derived automatically
  --   from the prior two, if the compiler didn't complain about ambiguity
  identityA :: (a -> a)
  -- aIdentity = toA . toB
  identityB :: (b -> b)
  -- bIdentity = toB . toA

Specifically, the isomorphism between Void -> Void and () looks like:

instance Isomorphism (Void -> Void) () where
  toA = fromUnit
  toB = toUnit

  identityA = fromUnit . toUnit
  identityB = toUnit . fromUnit

In future examples, I’ll use this typeclass to demonstrate isomorphisms between types.

Hyperoperative (Multi)functors

Another way to go from 0 to 1 is to just add one, an operation also called the successor function.

Kinds live one step up from types, and we can conjecture the kind a successor “function” on types would have.

-- The successor function constructs an integer from an integer
succ :: Int -> Int
-- So we need to be able to construct a "bigger" type from a type
Succ :: * -> *

“Function” is the wrong word for this, since it is evocative of a mapping between values, rather than a mapping between types. The word with the closest meaning is functor, which Haskell already uses to refer to types with a manipulable “inside” that can be mapped over. Fortunately, the kind of Succ matches what Haskell expects Functors to look like².

The functor in Haskell which most closely resembles the successor function is Maybe.

data Maybe a = Nothing | Just a
type One = Maybe Void

\begin{matrix} \scriptsize \text{A Maybe $X$ is either} & \scriptsize \text{Nothing} & \scriptsize \text{or} & \scriptsize \text{a value of $X$} \\ S(X) := & 1 & + & X \\ \scriptsize \text{The 1-valued type is} & \scriptsize \text{Nothing} & \scriptsize \text{or} & \scriptsize \text{logically impossible} \\ \bold{1} =& 1 & + & 0 \end{matrix}

Since Void is has zero possible values, we should expect Maybe Void to have exactly one possible value. Constructing a Just Void would require that we already had a Void value, which is impossible. Therefore, Nothing is the only possible value of Maybe Void.

toUnitM :: Maybe Void -> ()
toUnitM Nothing = ()

fromUnitM :: () -> Maybe Void
fromUnitM () = Nothing

instance Isomorphism (Maybe Void) () where
  toA = fromUnitM
  toB = toUnitM

  identityA = fromUnitM . toUnitM
  identityB = toUnitM . fromUnitM

Sums and Products

If there’s a functor which resembles the successor, then are there ones which also resemble addition and multiplication? Not exactly. Functors are strictly a single-argument kind, and luckily the successor is a unary function. Addition and multiplication are binary, so they require a slightly more complicated kind:

(+)      :: Int -> Int -> Int   -- we can add two things together
Plus a b :: * -> * -> *         -- so we want to be able to add two types together

(*)      :: Int -> Int -> Int   -- likewise, we can multiply two things
Mult a b :: * -> * -> *         -- and we want to be able to multiply two types

These kinds match what Haskell expects Bifunctors to look like. Types get complicated when more than one parameter is involved, so GHC cannot derive Bifunctor. Alternatively, we can just consider bifunctors as they appear here: a functor with an arity of 2.

Putting aside semantics, Haskell indeed has two types resembling type addition and type multiplication. Respectively, they are Either and (,) (i.e., a 2-tuple):

data Either a b = Left a | Right b
data (,) a b = (,) a b

\begin{matrix} \scriptsize \text{Either $X$ or $Y$ is} & \scriptsize \text{a value of $X$} & \scriptsize \text{or} & \scriptsize \text{a value of $Y$} \\ E(X,Y) := & X & + & Y \\ \scriptsize \text{A tuple of $X$ and $Y$ is} & \scriptsize \text{a value of $X$} & \scriptsize \text{and} & \scriptsize \text{a value of $Y$} \\ P(X,Y) := & X & \times & Y \end{matrix}

Product types are common (consider any struct or tuple in a more common language, but sum types are less so. unions in C get close, but they are bound too memory for our purposes. Using addition, we can actually reconstruct the successor from 1:

type MaybeE a = Either () a

toMaybeE :: Maybe a -> MaybeE a
toMaybeE Nothing  = Left ()
toMaybeE (Just x) = Right x

fromMaybeE :: MaybeE a -> Maybe a
fromMaybeE (Left ()) = Nothing
fromMaybeE (Right x) = Just x

instance Isomorphism (Maybe a) (MaybeE a) where
  toA = fromMaybeE
  toB = toMaybeE

  identityA = fromMaybeE . toMaybeE
  identityB = toMaybeE . fromMaybeE

Left () now takes on the role of Nothing, while all the Rights come from the type parameter a.

Rearranging and Rebracketing

Within the world of numbers, addition and multiplication are commutative and associative. Is the same true for types?

Commutativity is obvious, since we can construct functions which switch X and Y around. Haskell already provides these functions, whose definitions I have copied here

-- From https://hackage.haskell.org/package/either-5.0.2/docs/Data-Either-Combinators.html#v:swapEither
swapEither :: Either a b -> Either b a
swapEither (Left x)  = Right x
swapEither (Right x) = Left x

instance Isomorphism (Either x y) (Either y x) where
  toA = swapEither
  toB = swapEither

  identityA = swapEither . swapEither
  identityB = swapEither . swapEither

-- From https://hackage.haskell.org/package/base-4.16.1.0/docs/Data-Tuple.html#v:swap
swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)

instance Isomorphism (x, y) (y, x) where
  toA = swap
  toB = swap

  identityA = swap . swap
  identityB = swap . swap

Associativity is a bit trickier, since it deals with triples rather than pairs.

assocRightSum :: Either a (Either b c) -> Either (Either a b) c
assocRightSum (Left x)          = Left (Left x)
assocRightSum (Right (Left y))  = Left (Right y)
assocRightSum (Right (Right z)) = Right z

assocLeftSum :: Either (Either a b) c -> Either a (Either b c)
assocLeftSum (Left (Left x))  = Left x
assocLeftSum (Left (Right y)) = Right (Left y)
assocLeftSum (Right z)        = Right (Right z)

instance Isomorphism (Either a (Either b c)) (Either (Either a b) c) where
  toA = assocLeftSum
  toB = assocRightSum

  identityA = assocLeftSum . assocRightSum
  identityB = assocRightSum . assocLeftSum

assocRightProd :: (a, (b, c)) -> ((a, b), c)
assocRightProd (x, (y, z)) = ((x, y), z)

assocLeftProd :: ((a, b), c) -> (a, (b, c))
assocLeftProd ((x, y), z) = (x, (y, z))

instance Isomorphism (a, (b, c)) ((a, b), c) where
  toA = assocLeftProd
  toB = assocRightProd

  identityA = assocLeftProd . assocRightProd
  identityB = assocRightProd . assocLeftProd

In fact, since we don’t care about order or grouping, we can forget both entirely and map them instead into 3-tuples and a triple-sum type:

data Either3 a b c = Left3 a | Center3 b | Right3 c
data (,,) a b c = (,,) a b c

toLeftSum :: Either3 a b c -> Either (Either a b) c -- x+y+z = (x+y)+z
toLeftSum (Left3 x)   = Left (Left x)
toLeftSum (Center3 y) = Left (Right y)
toLeftSum (Right3 z)  = Right z

fromLeftSum :: Either (Either a b) c -> Either3 a b c
fromLeftSum (Left (Left x))  = Left3 x
fromLeftSum (Left (Right y)) = Center3 y
fromLeftSum (Right z)        = Right3 z

instance Isomorphism (Either3 a b c) (Either (Either a b) c) where
  toA = fromLeftSum
  toB = toLeftSum

  identityA = fromLeftSum . toLeftSum
  identityB = toLeftSum . fromLeftSum

toLeftProd :: (a,b,c) -> ((a,b),c)
toLeftProd (x,y,z) = ((x,y),z)

fromLeftProd :: ((a,b),c) -> (a,b,c)
fromLeftProd ((x,y),z) = (x,y,z)

instance Isomorphism (a, b, c) ((a,b), c) where
  toA = fromLeftProd
  toB = toLeftProd

  identityA = fromLeftProd . toLeftProd
  identityB = toLeftProd . fromLeftProd

There’s still a bit of work to prove associativity in general from these local rules. But that’s fine, since we’re still primarily concerned with the equivalent functors Either and (,) (which are local anyway).

Other Arithmetic Properties

Naturally, 0 and 1 satisfy their typical properties. There are additional interpretations, however:

Additive identity

0 + X \cong X

Isomorphism (Either Void a) a

Since 0 is unoccupied, its sum with any other type can only ever contain values from that other type (i.e., only Right values).

Multiplicative Identity

1 \cdot X \cong X

Isomorphism ((), a) a

Since 1 has exactly one possible value, its product with any other type is this value and any value from the other type (i.e., tuples of the form ((), x)).

Multiplicative Annihilator

0 \cdot X \cong 0

Isomorphism (Void, a) Void

Since 0 is unoccupied, we cannot construct a type which requires a value from it (i.e., writing a tuple of the form (Void, x) requires having a Void value).

Distributivity

Finally, to hammer home the resemblance to normal arithmetic, we should consider the distribution of multiplication over addition. First, notice that type multiplication does distribute over the successor:

type SuccDist a b = (Maybe a, Maybe b)
data SumProd a b = Nada | LProd a | RProd b | BothProd a b

\begin{matrix} \scriptsize \text{Maybe $X$ and Maybe $Y$} & \scriptsize \text{is equivalent to} \\ (1 + X) \cdot (1 + Y) \cong \\ 1 & \scriptsize \text{Both Nothing} \\ + X \phantom{\cdot Y} & \scriptsize \text{or Just $x$, Nothing} \\ + \phantom{X \cdot} Y & \scriptsize \text{or Nothing, Just $y$} \\ + X \cdot Y & \scriptsize \text{or Just $x$, Just $y$} \end{matrix}

If we forbade the first and last cases (in other words, if we “subtract” them out), then the type would be equivalent to the sum of X and Y.

eitherToSuccDist :: Either a b -> SuccDist a b
eitherToSuccDist (Left x) = (Just x, Nothing)
eitherToSuccDist (Right y) = (Nothing, Just y)

succDistToEither :: SuccDist a b -> Either a b
succDistToEither (Just x, Nothing) = Left x
succDistToEither (Nothing, Just y) = Right y
succDistToEither _                 = undefined -- non-exhaustive!

-- succDistToEither . eitherToSuccDist == (id :: Either a b -> Either a b)
-- eitherToSuccDist . succDistToEither /= id (because of extra values)

toSumProd :: SuccDist a b -> SumProd a b
toSumProd (Nothing, Nothing) = Nada
toSumProd (Just x, Nothing)  = LProd x
toSumProd (Nothing, Just y)  = RProd y
toSumProd (Just x, Just y)   = BothProd x y

toSuccDist :: SumProd a b -> SuccDist a b
toSuccDist Nada           = (Nothing, Nothing)
toSuccDist (LProd x)      = (Just x, Nothing)
toSuccDist (RProd y)      = (Nothing, Just y)
toSuccDist (BothProd x y) = (Just x, Just y)

instance Isomorphism (SuccDist a b) (SumProd a b) where
  toA = toSuccDist
  toB = toSumProd

  identityA = toSuccDist . toSumProd
  identityB = toSumProd . toSuccDist

Fortunately, general distributivity is also relatively simple. We do as grade schoolers do and FOIL out the results.

type PreDist a b c d  = (Either a b, Either c d)
-- first, outer, inner, last
data PostDist a b c d = F a c | O a d | I b c | L b d

\begin{matrix} \scriptsize \text{Either $X$ $Y$ and Either $Z$ $W$} & \scriptsize \text{is equivalent to} \\ (X + Y) \cdot (Z + W) \cong \\ \phantom{+} X \cdot Z & \scriptsize \text{Firsts,} \\ \vphantom{} + X \cdot W & \scriptsize \text{Outers,} \\ \vphantom{} + Y \cdot Z & \scriptsize \text{Inners,} \\ \vphantom{} + Y \cdot W & \scriptsize \text{or Lasts} \end{matrix}

…then construct our bijections:

distribute :: PreDist a b c d -> PostDist a b c d
distribute (Left x, Left z)   = F x z
distribute (Left x, Right w)  = O x w
distribute (Right y, Left z)  = I y z
distribute (Right y, Right w) = L y w

undistribute :: PostDist a b c d -> PreDist a b c d
undistribute (F x z) = (Left x, Left z)
undistribute (O x w) = (Left x, Right w)
undistribute (I y z) = (Right y, Left z)
undistribute (L y w) = (Right y, Right w)

instance Isomorphism (PreDist a b c d) (PostDist a b c d) where
  toA = undistribute
  toB = distribute

  identityA = undistribute . distribute
  identityB = distribute . undistribute

This works primarily because without further information about any of the types a, b, c, d, we can only rearrange values of them.

Bools, Bools, and more Bools

While it’s all well and good that these operations appear to mirror familiar arithmetic, we haven’t counted farther than 0 and 1. Everyone past the age of two recognizes that 2 comes next.

Fortunately, this corresponds to a much better-known type: booleans. Rather than defining them as numbers like in lower-level languages (as a computer would understand), we can construct them directly as abstract values in Haskell

data Bool = True | False

\begin{matrix} \scriptsize \text{A bool is either} & \scriptsize \text{True} & \scriptsize \text{or} & \scriptsize \text{False} \\ \text{Bool} := & 1 & + & 1 &= \bold{2} \end{matrix}

Bools may also be defined using the above functors, either by two successors or by addition:

type BoolSucc = Maybe (Maybe Void) -- succ (succ 0)
type BoolEither = Either () () -- 1 + 1

toBoolSucc :: Bool -> BoolSucc
toBoolSucc False = Nothing
toBoolSucc True  = Just Nothing

fromBoolSucc :: BoolSucc -> Bool
fromBoolSucc Nothing        = False
fromBoolSucc (Just Nothing) = True

instance Isomorphism Bool BoolSucc where
  toA = fromBoolSucc
  toB = toBoolSucc

  identityA = fromBoolSucc . toBoolSucc
  identityB = toBoolSucc . fromBoolSucc

toBoolEither :: Bool -> BoolEither
toBoolEither False = Left ()
toBoolEither True  = Right ()

fromBoolEither :: BoolEither -> Bool
fromBoolEither (Left ())  = False
fromBoolEither (Right ()) = True

instance Isomorphism Bool BoolEither where
  toA = fromBoolEither
  toB = toBoolEither

  identityA = fromBoolEither . toBoolEither
  identityB = toBoolEither . fromBoolEither

Four Great Justice

Rather than progressing to 3, let’s jump to 4. The number 2 has an interesting property: its sum with itself is its product with itself (is its exponent with itself…) is 4. Thus, the following types all encode a four-valued type:

data Four     = Zero | One | Two | Three
type FourSucc = Maybe (Maybe Bool)
type FourSum  = Either Bool Bool
type FourProd = (Bool, Bool)

\begin{align*} 4 &:= 1+1+1+1 \\ & \phantom{:}\cong S(S(2)) \\ & \phantom{:}\cong E(2,2) = 2 + 2 \\ & \phantom{:}\cong P(2,2) = 2 \cdot 2 \\ \end{align*}

Showing isomorphism here can get a bit tricky, but there are natural bijections for FourSum and FourProd obtained by examining the binary expansions of 0, 1, 2, and 3.

toFourSucc :: Four -> FourSucc
toFourSucc Zero  = Nothing
toFourSucc One   = Just Nothing
toFourSucc Two   = Just (Just False)
toFourSucc Three = Just (Just True)

fromFourSucc :: FourSucc -> Four
fromFourSucc Nothing             = Zero
fromFourSucc (Just Nothing)      = One
fromFourSucc (Just (Just False)) = Two
fromFourSucc (Just (Just True))  = Three

instance Isomorphism Four FourSucc where
  toA = fromFourSucc
  toB = toFourSucc

  identityA = fromFourSucc . toFourSucc
  identityB = toFourSucc . fromFourSucc

toFourSum :: Four -> FourSum
toFourSum Zero  = Left False   -- 00
toFourSum One   = Left True    -- 01
toFourSum Two   = Right False  -- 10
toFourSum Three = Right True   -- 11

fromFourSum :: FourSum -> Four
fromFourSum (Left False)  = Zero
fromFourSum (Left True)   = One
fromFourSum (Right False) = Two
fromFourSum (Right True)  = Three

instance Isomorphism Four FourSum where
  toA = fromFourSum
  toB = toFourSum

  identityA = fromFourSum . toFourSum
  identityB = toFourSum . fromFourSum

toFourProd :: Four -> FourProd
toFourProd Zero  = (False, False)  -- 00
toFourProd One   = (False, True)   -- 01
toFourProd Two   = (True, False)   -- 10
toFourProd Three = (True, True)    -- 11

fromFourProd :: FourProd -> Four
fromFourProd (False, False) = Zero
fromFourProd (False, True)  = One
fromFourProd (True, False)  = Two
fromFourProd (True, True)   = Three

instance Isomorphism Four FourProd where
  toA = fromFourProd
  toB = toFourProd

  identityA = fromFourProd . toFourProd
  identityB = toFourProd . fromFourProd

Hiding in the Clouds

Though I mentioned exponentiation earlier, I did not show the equivalent for types. Set theorists sometimes write the set of functions from one set A to another set B as B^A because the number of possible functions comes from the cardinalities of the sets: |B|^{|A|}. We previously examined how the constructor for Void is a singleton, which satisfies the equation 0^0 = 1. At least in the finite world, sets and types are not so different, and indeed, we can write:

type FourFunc = Bool -> Bool

-- There are exactly four functions:
taut x = True   -- tautology
cont x = False  -- contradiction
id'  x = x      -- identity
not'   = not    -- negation

\textcolor{red}{2} \rightarrow \textcolor{blue}{2} = \textcolor{blue}{2}^{\textcolor{red}{2}} \cong \bold 4

If we want to map these functions onto our Four type, we can again examine the binary expansion of the numbers 0-3. This time, the rightmost place value encodes the value of the function on False, and the leftmost value the same on True.

toFourFunc :: Four -> FourFunc
--                       -- f(1) f(0)
toFourFunc Zero  = cont  --   0    0
toFourFunc One   = not'  --   0    1
toFourFunc Two   = id'   --   1    0
toFourFunc Three = taut  --   1    1

fromFourFunc :: FourFunc -> Four
fromFourFunc cont = Zero
fromFourFunc not' = One
fromFourFunc id'  = Two
fromFourFunc taut = Three

instance Isomorphism Four FourFunc where
  toA = fromFourFunc
  toB = toFourFunc

  identityA = fromFourFunc . toFourFunc
  identityB = toFourFunc . fromFourFunc

For larger functions, we can see a more generalizable mapping from looking at a truth table, shown here for AND:

Column Number	Binary	Input (x)	Input (y)	x AND y
0	00	False	False	False
1	01	False	True	False
2	10	True	False	False
3	11	True	True	True

Going up the final column and converting to binary digits, we can read “1000”, which is the binary expansion of 8. The other numbers from 0 to (2^2)^2 - 1 can similarly be associated to boolean functions Bool -> (Bool -> Bool)³.

Closing

If you know your Haskell, especially the difference between data and newtype, then you know about the way I have slightly stretched the truth. It is true that types defined with data implicitly add a possible undefined value which can tell the runtime to error out. Everyone who knows Haskell better than me says not to worry about it in most cases. At worst, using data would make some of the pretty arithmetic above be less pretty.

Other fascinating concepts live in this world, such as the Curry-Howard correspondence. Rather than discussing them, in the next post I would like to press onward with the algebra. I have spent this post laying the groundwork for arithmetic on types, so it will focus more upon recursion and fixed points.

Additional Links

• Algebraic Data Types (Wikipedia)
• Generically Deriving Bifunctor (Blogpost by Csongor Kiss)

Footnotes

1. Pronounced as “unit”

2. In fact, since GHC 6.12.1, the compiler is smart enough to derive definitions in many cases.

3. Note that function arrows are assumed to be right-associative, but this is opposite the typical application order of exponentiation. I’ll dive deeper into why this needs to be the case later.