5.2: Algebraic data types

Notes from this youtube video


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 ? So we have a monoid with respect to product.



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.