# Difference between revisions of "Peano numbers"

DonStewart (talk | contribs) m (category) |
|||

Line 35: | Line 35: | ||

[[Category:Idioms]] |
[[Category:Idioms]] |
||

+ | [[Category:Glossary]] |

## Revision as of 00:11, 9 October 2006

**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 do type arithmetic.

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

Here's a simple addition function:

add Zero b = b add (Succ a) b = Succ (add a b)

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

Arithmetic can be done using fundeps:

class Add a b ab | a b -> ab instance Add Zero b b instance (Add a b ab) => Add (Succ a) b (Succ ab)

Note that classes express relationships between types, rather than functions from type to type. Accordingly, with the instance declarations above one can add another fundep to the class declaration to get subtraction for free:

class Add a b ab | a b -> ab, a ab -> b instance Add Zero b b instance (Add a b ab) => Add (Succ a) b (Succ ab)

See type arithmetic for other functions and encodings.