Difference between revisions of "Peano numbers"
MichalPalka (talk  contribs) (Rephrase why peano numbers are used mainly in type arithmethic.) 
(→Peano number types: no wiki page for fundep. Replace it by Functional_dependencies) 

(10 intermediate revisions by 4 users not shown)  
Line 14:  Line 14:  
<haskell> 
<haskell> 

−  +  add Zero b = b 

−  +  add (Succ a) b = Succ (add a b) 

</haskell> 
</haskell> 

−  See an [http:// 
+  See an [http://code.haskell.org/~thielema/htam/src/Number/PeanoNumber.hs example implementation]. 
=== Peano number types === 
=== Peano number types === 

<haskell> 
<haskell> 

−  +  data Zero 

−  +  data Succ a 

−  data Succ a 

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

−  +  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> 
</haskell> 

Line 40:  Line 40:  
<haskell> 
<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> 
</haskell> 

Line 57:  Line 57:  
length xs == 0 
length xs == 0 

</haskell> 
</haskell> 

−  because <hask>length</hask> constructs all list nodes, 

⚫  
⚫  
⚫  
⚫  
−  but with Peano numbers you achieve the same 

<haskell> 
<haskell> 

genericLength xs == Zero 
genericLength xs == Zero 

Line 76:  Line 74:  
genericLength xs == (genericLength ys :: Peano) 
genericLength xs == (genericLength ys :: Peano) 

</haskell> 
</haskell> 

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

−  
=== Equation solving === 
=== Equation solving === 

Line 89:  Line 87:  
See example implementations: 
See example implementations: 

* [http://darcs.haskell.org/htam/src/Number/PeanoNumber.hs using standard Prelude] 
* [http://darcs.haskell.org/htam/src/Number/PeanoNumber.hs using standard Prelude] 

−  * [http://darcs.haskell.org/numericprelude/src/Number/Peano.hs 
+  * using [[Numeric Prelude]] [http://darcs.haskell.org/numericprelude/src/Number/Peano.hs type classes] 
[[Category:Mathematics]] 
[[Category:Mathematics]] 
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
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 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.
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
traverses the whole list and may take a long time doing so, 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)
traverses only as many list nodes as are in the shorter list.
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: