Proving Algebraic Datatypes are “Algebraic”

Several programming languages allow programmers to define (potentially recursive) custom types, by composing together existing ones. For instance, in OCaml, one can define lists as follows:

type 'a list =
| Cons of 'a * 'a list
| Nil

This translates in Haskell as

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

In Rust:

enum List<A> {
  Cons(A, Box< List<a> >),
  Nil,
}

In Coq:

Inductive list a :=
| cons : a -> list a -> list a
| nil

And so forth.Each language will have its own specific constructions, and the type systems of OCaml, Haskell, Rust and Coq —to only cite them— are far from being equivalent. That being said, they often share a common “base formalism,” usually (and sometimes abusively) referred to as algebraic datatypes . This expression is used because under the hood any datatype can be encoded as a composition of types using two operators: sum ( + ) and product ( * ) for types.

• a + b is the disjoint union of types a and b . Any term of a can be injected into a + b , and the same goes for b . Conversely, a term of a + b can be projected into either a or b .
• a * b is the Cartesian product of types a and b . Any term of a * b is made of one term of a and one term of b (remember tuples?).

For an algebraic datatype, one constructor allows for defining “named tuples”, that is ad-hoc product types. Besides, constructors are mutually exclusive: you cannot define the same term using two different constructors. Therefore, a datatype with several constructors is reminescent of a disjoint union. Coming back to the list type, under the syntactic sugar of algebraic datatypes, the list α type is equivalent to unit + α * list α , where unit models the nil case, and α * list α models the cons case.The set of types which can be defined in a language together with + and * form an “algebraic structure” in the mathematical sense, hence the name. It means the definitions of + and * have to satisfy properties such as commutativity or the existence of neutral elements. In this article, we will prove some of them in Coq. More precisely,

• + is commutative, that is $\forall (x, y),\ x + y = y + x$ ∀ ( x , y ) ,   x + x
• + is associative, that is $\forall (x, y, z),\ (x + y) + z = x + (y + z)$ ∀ ( x , y , z ) ,   ( x + y ) + ( y + z )
• + has a neutral element, that is $\exists e_s, \ \forall x,\ x + e_s = x$ ∃ e s ​ ,   ∀ x ,   x + x
• * is commutative, that is $\forall (x, y),\ x * y = y * x$ ∀ ( x , y ) ,   x ∗ x
• * is associative, that is $\forall (x, y, z),\ (x * y) * z = x * (y * z)$ ∀ ( x , y , z ) ,   ( x ∗ y ) ∗ ( y ∗ z )
• * has a neutral element, that is $\exists e_p, \ \forall x,\ x * e_p = x$ ∃ e p ​ ,   ∀ x ,   x ∗ x
• The distributivity of + and * , that is $\forall (x, y, z),\ x * (y + z) = x * y + x * z$ ∀ ( x , y , z ) ,   x ∗ ( y + z ) = z
• * has an absorbing element, that is $\exists e_a, \ \forall x, \ x * e_a = e_a$ ∃ e a ​ ,   ∀ x ,   x ∗ e a ​

For the record, the sum and prod types are defined in Coq as follows:

Inductive sum (A B : Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B

Inductive prod (A B : Type) : Type :=
| pair : A -> B -> prod A B

1. An Equivalence for Type
   1. Introducing type_equiv
   2. type_equiv is an Equivalence
   3. 1. list ’s Canonical Form
      2. nat is a Special-Purpose list
2. prod has an Absorbing Element
3. prod and sum Distributivity
4. Bonus: Algebraic Datatypes and Metaprogramming