Difference between revisions of "Peano numbers"
Jump to navigation
Jump to search
m (+cat) |
|||
Line 14: | Line 14: | ||
Here <tt>Zero</tt> and <tt>Succ</tt> are types. <tt>Zero</tt> has kind <tt>*</tt>, and <tt>Succ</tt> has kind <tt>* -> *</tt>. The natural numbers are represented by types (of kind <tt>*</tt>) <tt>Zero</tt>, <tt>Succ Zero</tt>, <tt>Succ Succ Zero</tt> etc. |
Here <tt>Zero</tt> and <tt>Succ</tt> are types. <tt>Zero</tt> has kind <tt>*</tt>, and <tt>Succ</tt> has kind <tt>* -> *</tt>. The natural numbers are represented by types (of kind <tt>*</tt>) <tt>Zero</tt>, <tt>Succ Zero</tt>, <tt>Succ Succ Zero</tt> etc. |
||
+ | |||
+ | [[Category:Idioms]] |
Revision as of 20:33, 24 January 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 create a set of phantom types.
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.
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.