Peano numbers
Jump to navigation
Jump to search
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.