Peano numbers

Peano numbers are a simple way of representing the natural numbers using only a zero value and a successor function. In Haskell it is easy to create a type of Peano number values, but they are more often used to create a set of phantom types.

Peano number values

data Peano = Zero | Succ Peano

Here Zero and Succ are values (constructors). Zero has type Peano, and Succ has type Peano -> Peano. The natural number zero is represented by Zero, one by Succ Zero, two by Succ (Succ Zero) and so forth.

Peano number types

data Zero

data Succ a

Here Zero and Succ are types. Zero has kind *, and Succ has kind * -> *. The natural numbers are represented by types (of kind *) Zero, Succ Zero, Succ (Succ Zero) etc.