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.

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
```

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`

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
```

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
```

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)
```

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
...
```

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.

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 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)
```

This modified text is an extract of the original Stack Overflow Documentation created by following contributors and released under CC BY-SA 3.0

This website is not affiliated with Stack Overflow