Natural numbers in type algebra

We can draw a connection between the Haskell types and the natural numbers. This connection can be made assigning to every type the number of inhabitants it has.

Finite union types

For finite types, it suffices to see that we can assign a natural type to every number, based in the number of constructors. For example:

type Color = Red | Yellow | Green

would be 3. And the Bool type would be 2.

type Bool = True | False

Uniqueness up to isomorphism

We have seen that multiple types would correspond to a single number, but in this case, they would be isomorphic. This is to say that there would be a pair of morphisms f and g, whose composition would be the identity, connecting the two types.

f :: a -> b
g :: b -> a

f . g == id == g . f

In this case, we would say that the types are isomorphic. We will consider two types equal in our algebra as long as they are isomorphic.

For example, two different representations of the number two are trivally isomorphic:

type Bit  = I    | O
type Bool = True | False

bitValue :: Bit -> Bool
bitValue I = True
bitValue O = False

booleanBit :: Bool -> Bit
booleanBit True  = I
booleanBit False = O

Because we can see bitValue . booleanBit == id == booleanBit . bitValue

One and Zero

The representation of the number 1 is obviously a type with only one constructor. In Haskell, this type is canonically the type (), called Unit. Every other type with only one constructor is isomorphic to ().

And our representation of 0 will be a type without constructors. This is the Void type in Haskell, as defined in Data.Void. This would be equivalent to a unhabited type, wihtout data constructors:

data Void

Addition and multiplication

The addition and multiplication have equivalents in this type algebra. They correspond to the tagged unions and product types.

data Sum a b = A a | B b
data Prod a b = Prod a b

We can see how the number of inhabitants of every type corresponds to the operations of the algebra.

Equivalently, we can use Either and (,) as type constructors for the addition and the multiplication. They are isomorphic to our previously defined types:

type Sum' a b = Either a b
type Prod' a b = (a,b)

The expected results of addition and multiplication are followed by the type algebra up to isomorphism. For example, we can see an isomorphism between 1 + 2, 2 + 1 and 3; as 1 + 2 = 3 = 2 + 1.

data Color = Red | Green | Blue

f :: Sum () Bool -> Color
f (Left ())     = Red
f (Right True)  = Green
f (Right False) = Blue

g :: Color -> Sum () Bool
g Red   = Left ()
g Green = Right True
g Blue  = Right False

f' :: Sum Bool () -> Color
f' (Right ())   = Red
f' (Left True)  = Green
f' (Left False) = Blue

g' :: Color -> Sum Bool ()
g' Red   = Right ()
g' Green = Left True
g' Blue  = Left False

Rules of addition and multiplication

The common rules of commutativity, associativity and distributivity are valid because there are trivial isomorphisms between the following types:

-- Commutativity
Sum a b           <=> Sum b a
Prod a b          <=> Prod b a
-- Associativity
Sum (Sum a b) c   <=> Sum a (Sum b c)
Prod (Prod a b) c <=> Prod a (Prod b c)
-- Distributivity
Prod a (Sum b c)  <=> Sum (Prod a b) (Prod a c)

Recursive types

Lists

Lists can be defined as:

data List a = Nil | Cons a (List a) 

If we translate this into our type algebra, we get

List(a) = 1 + a * List(a)

But we can now substitute List(a) again in this expression multiple times, in order to get:

List(a) = 1 + a + a*a + a*a*a + a*a*a*a + …

This makes sense if we see a list as a type that can contain only one value, as in []; or every value of type a, as in [x]; or two values of type a, as in [x,y]; and so on. The theoretical definition of List that we should get from there would be:

-- Not working Haskell code!
data List a = Nil
            | One a
            | Two a a
            | Three a a a 
            ...

Trees

We can do the same thing with binary trees, for example. If we define them as:

data Tree a = Empty | Node a (Tree a) (Tree a)

We get the expression:

Tree(a) = 1 + a * Tree(a) * Tree(a)

And if we make the same substitutions again and again, we would obtain the following sequence:

Tree(a) = 1 + a + 2 (a*a) + 5 (a*a*a) + 14 (a*a*a*a) + …

The coefficients we get here correspond to the Catalan numbers sequence, and the n-th catalan number is precisely the number of possible binary trees with n nodes.

Derivatives

The derivative of a type is the type of its type of one-hole contexts. This is the type that we would get if we make a type variable disappear in every possible point and sum the results.

As an example, we can take the triple type (a,a,a), and derive it, obtaining

data OneHoleContextsOfTriple = (a,a,()) | (a,(),a) | ((),a,a)

This is coherent with our usual definition of derivation, as:

d/da (a*a*a) = 3*a*a

More on this topic can be read on this article.

Functions

Functions can be seen as exponentials in our algebra. As we can see, if we take a type a with n instances and a type b with m instances, the type a -> b will have m to the power of n instances.

As an example, Bool -> Bool is isomorphic to (Bool,Bool), as 2*2 = 2².

iso1 :: (Bool -> Bool) -> (Bool,Bool)
iso1 f = (f True,f False)

iso2 :: (Bool,Bool) -> (Bool -> Bool)
iso2 (x,y) = (\p -> if p then x else y)