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

The axiom

The empty list is a list

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:

The axiom

The even list is a list

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