# 5.2: Algebraic data types

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