# Peano numbers

### From HaskellWiki

(→Peano number values: update link to code.haskell.org) |
(→Peano number types: no wiki page for fundep. Replace it by Functional_dependencies) |
||

Line 29: | Line 29: | ||

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. | 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 [[ | + | Arithmetic can be done using [[Functional_dependencies]]: |

<haskell> | <haskell> |

## Latest revision as of 20:23, 9 January 2018

**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 since unary representation is inefficient, they are more often used to do type arithmetic due to their simplicity.

## Contents |

## [edit] 1 Overview

### [edit] 1.1 Peano number values

data Peano = Zero | Succ Peano

Here's a simple addition function:

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

See an example implementation.

### [edit] 1.2 Peano number types

data Zero data Succ a

Arithmetic can be done using Functional_dependencies:

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.

## [edit] 2 Applications

### [edit] 2.1 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

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 appropriategenericLength xs == (genericLength ys :: Peano)

traverses only as many list nodes as are in the shorter list.

### [edit] 2.2 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.

## [edit] 3 See also

See example implementations: