Difference between revisions of "Peano numbers"
Jump to navigation
Jump to search
m (+cat) |
m |
||
| Line 5: | Line 5: | ||
data Peano = Zero | Succ Peano |
data Peano = Zero | Succ Peano |
||
| − | Here <tt>Zero</tt> and <tt>Succ</tt> are values (constructors). <tt>Zero</tt> has type <tt>Peano</tt>, and <tt>Succ</tt> has type <tt>Peano -> Peano</tt>. The natural number zero is represented by <tt>Zero</tt>, one by <tt>Succ Zero</tt>, two by <tt>Succ Succ Zero</tt> and so forth. |
+ | Here <tt>Zero</tt> and <tt>Succ</tt> are values (constructors). <tt>Zero</tt> has type <tt>Peano</tt>, and <tt>Succ</tt> has type <tt>Peano -> Peano</tt>. The natural number zero is represented by <tt>Zero</tt>, one by <tt>Succ Zero</tt>, two by <tt>Succ (Succ Zero)</tt> and so forth. |
== Peano number types == |
== Peano number types == |
||
| Line 13: | Line 13: | ||
data Succ a |
data Succ a |
||
| − | 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]] |
[[Category:Idioms]] |
||
Revision as of 02:03, 25 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.