Types as axioms

Takeaway:

In Haskell when we want to represent an even list what comes to mind is activating some sort of language extension to add some constraints.

This perspective is restrictive.

Where we want to restrict our original definition of a List somehow:

-- We want to constraint this
data List a = Nil | Cons a (List a)

However, another perspective we can adopt is constructive.

We first look at the definition of a list on two ways:

  1. The axiom

    The empty list is a list

  2. The inference rule

    If you have a list, and you add an element to the beginning, the result is also a list

Such an approach is constructive, we think of the axioms and inference rules to construct the datatype.

We can have the following axioms for an even list:

  1. The axiom

    The even list is a list

  2. The inference rule

    If you have a list, and you add two element to the beginning, the result is also an even list

Hence we will define our list as such:

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

References: Alexis King - Types as Axioms