Editing Peano numbers (section)

== Overview ==

=== Peano number values ===

<haskell>
 data Peano = Zero | Succ Peano
</haskell>

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:

<haskell>
add Zero b = b
add (Succ a) b = Succ (add a b)
</haskell>

See an [http://code.haskell.org/~thielema/htam/src/Number/PeanoNumber.hs example implementation].

=== Peano number types ===

<haskell>
data Zero
data Succ a
</haskell>

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 [[Functional_dependencies]]:

<haskell>
class Add a b ab | a b -> ab
instance Add Zero b b
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:

<haskell>
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)
</haskell>

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