5.2: Algebraic data types | Categories Bartosz Milewski Youtube notes

Product

Why is it an algebra ?
We have products and sums just like in algebra.
Product is sort of multiplication. It means that we have at least a monoid.
A monoid has an operation (here multiplication) that is associative and has a unit.
But does the product in types behave like multiplication ?

Symetry (this is not needed for a monoid)
The product of numbers is symetric, but this is not true for the product of two types :
If we have types a and b, the pair (a, b) is different from (b,a). However they contain the same information, which means that they are isomorphic ; the isomorphism is called swap.
```
swap :: (a, b) → (b, a)
swap p  = (snd p, fst p)
```
The inverse of swap is swap.
So multiplication is symetric up to isomorphism.
Associativity
Are ((a, b), c) and (a, (b, c)) equivalent ? No.
No but these two types contain the same information, but re-arranged ; they are isomorphic.
```
assoc :: ((a, b), c) = (a, (b, c))
```
This function is an isomorphism, it has an inverse.
Associativity means that we can omit parentheses and simply write (a, b, c).
So we just have tuples ; structs or records with multiple fields are just examples of this.
In classical algebra, this corresponds to (a * b) * c = a * (b * c)
Unit
What would be the type, which paired with any other type would give the same type ? This type should have only one element.
(a, ()) is isomorphic to a.
```
munit(x, ()) = x
munit_inv(x) = (x, ())
```
It's like taking the cartesian product of a line and a point, it gives a line (not exactly the same line).
What we did for right unit can be done for left unit.
In classical algebra, this corresponds to a * 1 = a

So we have a monoid with respect to product.

Sum

Symetry
Either a b ~ Either b a ; isomorphic
Associativity
Similarily it is also associative up to isomorphism.
If we want to associate Eithers we can write data structures like
```
data Triple = Left a | Middle b | Right c
```
Unit
The unit of sum is Void.
Either a Void is isomorphic to a.
In classical algebra, corresponds to a + 0 = a.

Algebra

So we have a second monoid. That's not all, we would like to combine these two monoids into something bigger.

From algebra we have a * 0 = 0
Is it true with types ? Is (a, Void) isomorphic to Void ?
Constructing a pair (a, Void) is impossible because we can't give an element of type Void ; this pair is inhabited, which is the same as Void.

From algebra we also have distributivity : a * (b + c) = a * b + a * c.
This is true, up to an isomorphism : (a, Either b c) ~ Either (a, b) (a, c).

A structure lke this in algebra is called a ring, except that in a true ring, addition and multiplication have an inverse. Here we don't know how to substract something or divide by something.
A structure like that is called a rig or semi-ring.

What is the correspondance of 2 = 1 + 1 ?
1 is the unit type. There are two possible values : left unit or right unit. We can call left unit true, and right unit false. 2 is isomorphic to a boolean.

What is the correspondance of 2 = 1 + a ?
This is Maybe :
data Maybe a = Nothing | Just a.
This has two constructors ; Nothing takes no argument, so it's equivalent to Unit.
So Maybe a is equivalent to Either () a.

Let's see an equation :
l(a) = 1 + a * l(a)
Which can be solved as follows :
l(a) - a * l(a) = 1
l(a) * (1 - a) = 1
l(a) = 1 / (1 - a)

Expressed as type, this gives :
data List a = Nil | Cons a (List a)
A list of a is either empty or it's a Cons of head and tail.
List a is a sum constructor (|)
Nil is a constructor that takes no argument, which corresponds to Unit type.
Cons is a product constructor, it takes two types as arguments.

To solve this equation with types, we cannot do division or substraction.
But l(a) = 1 / (1 - a) happens to be the sum of a geometric sequence : 1 + a + a*a + a*a*a + ...
1 corresponds to empty list ; a is a singleton list ; a*a is a list of 2 elements ; a*a*a is a list of 3 elements...
With this equation we have defined all possible lists.

The equation : l(a) = 1 + a * l(a) can be solved by substitution :
Using classical algebraic notation :
l(a) = 1 + a * (1 + a * l(a)) = 1 + a + a * a * (1 + a * l(a)) ...
This is a way of doing the same thing without doing the power series.