# Difference between revisions of "Peano numbers"

(applications) |
(code markup) |
||

Line 5: | Line 5: | ||

=== Peano number values === |
=== Peano number values === |
||

+ | <haskell> |
||

data Peano = Zero | Succ Peano |
data Peano = Zero | Succ Peano |
||

+ | </haskell> |
||

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

Here's a simple addition function: |
Here's a simple addition function: |
||

+ | <haskell> |
||

add Zero b = b |
add Zero b = b |
||

add (Succ a) b = Succ (add a b) |
add (Succ a) b = Succ (add a b) |
||

+ | </haskell> |
||

See an [http://darcs.haskell.org/htam/src/Number/PeanoNumber.hs example implementation]. |
See an [http://darcs.haskell.org/htam/src/Number/PeanoNumber.hs example implementation]. |
||

Line 18: | Line 22: | ||

=== Peano number types === |
=== Peano number types === |
||

+ | <haskell> |
||

data Zero |
data Zero |
||

data Succ a |
data Succ a |
||

+ | </haskell> |
||

− | Here < |
+ | Here <hask>Zero</hask> and <hask>Succ</hask> are types. <hask>Zero</hask> has kind <hask>*</hask>, and <hask>Succ</hask> has kind <hask>* -> *</hask>. The natural numbers are represented by types (of kind <hask>*</hask>) <hask>Zero</hask>, <hask>Succ Zero</hask>, <hask>Succ (Succ Zero)</hask> etc. |

Arithmetic can be done using fundeps: |
Arithmetic can be done using fundeps: |
||

+ | <haskell> |
||

class Add a b ab | a b -> ab |
class Add a b ab | a b -> ab |
||

instance Add Zero b b |
instance Add Zero b b |
||

instance (Add a b ab) => Add (Succ a) b (Succ ab) |
instance (Add a b ab) => Add (Succ a) b (Succ ab) |
||

+ | </haskell> |
||

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

+ | <haskell> |
||

class Add a b ab | a b -> ab, a ab -> b |
class Add a b ab | a b -> ab, a ab -> b |
||

instance Add Zero b b |
instance Add Zero b b |
||

instance (Add a b ab) => Add (Succ a) b (Succ ab) |
instance (Add a b ab) => Add (Succ a) b (Succ ab) |
||

+ | </haskell> |
||

See [[type arithmetic]] for other functions and encodings. |
See [[type arithmetic]] for other functions and encodings. |

## Revision as of 12:18, 3 July 2007

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

## Contents

## Overview

### 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)
```

See an example implementation.

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

## Applications

### Lazy counting

The lazy nature of Peano numbers rehabilitates the use of list functions which count list elements. As described in Things to avoid one should not write

```
length xs == 0
```

because `length`

constructs all list nodes,
although after you have seen only one, it is obvious that the list is not empty.
The above expression can be simply replaced by `null`

,
but with Peano numbers you achieve the same

```
genericLength xs == Zero
-- or
genericLength xs == (0::Peano)
```

The expression

```
length xs == length ys
```

is harder to make lazy without Peano numbers.
With them (and an appropriate `Num`

instance) this becomes rather simple, because

```
genericLength xs == (genericLength ys :: Peano)
```

constructs only as much list nodes, as the shorter list has.

### Equation solving

Lazy Peano numbers can also be used within "Tying the Knot" techniques. There is a package for determining the right order for solving equations, where an equation is only solved if only one of its variables is still indeterminate.

## See also

See example implementations: