Implementing Peano Naturals

Computer Science Level 3

One way to explain what natural numbers are is to do define

$0 := \left \{ \right \} \\ 1 := \left \{ \left \{ \right \}\right \} \\ 2 := \left \{ \left \{ \right \}, \left \{ \left \{ \right \} \right \}\right \} \\ \vdots$

I want to implement them using Haskell Lists like this:

peano 0 = []
peano 1 = [[]]
peano 2 = [[], [[]]]
.
.

To do so, I write the following program:

1 2	`peano 0 = [] peano n = map peano [0..n-1]`

What can I do to fix this program?

Inspired by Peano Axioms

Add a type signature The program will work Add appropriate parantheses This program can never be fixed

1 solution

Agnishom Chattopadhyay
Aug 31, 2016

The problem with this function is that there is no way to properly type it. Let me explain what I mean by that with some smaller values.

Suppose the function peano works only upto 1, in which case, it could be defined like this:

1
2
3

peano :: Integer -> [[t]]
peano 0 = []
peano 1 = [[]]

But then again, peano 2 is [[], [[]]] is not really of type [[t]] . It contains elements of type [[t]] . This means, it must be of the type [[[t]]] . In which case, we could define peano this way:

peano :: Integer -> [[[t]]]
peano 0 = []
peano 1 = [[]]
peano 2 = [[], [[]]]

But there is no way can define this to be infinitely nested, which is why we can never specify a function that works for all natural numbers.

Implementing Peano Naturals

1 solution

0 pending reports