7

I'm trying to write a function 

toPeano :: Int -> Nat
toPeano n =

that turns an Integer into its Peano Number.

I have the data:

data Nat =
   Zero |
   Succ Nat
   deriving Show

For example, 

toPeano 0 = Zero
toPeano 1 = Succ Zero
toPeano 2 = Succ (Succ Zero)

and so on.

I have no idea how to get it to print out the Peano Numbers given an integer. I've never worked with Peano numbers so any help with this would be greatly appreciated!

Thank you!

dgilperez
  • 10,716
  • 8
  • 68
  • 96
Shabu
  • 645
  • 4
  • 11
  • 17

2 Answers2

7

Your question isn't clear, so I'll start from the conversion:

toPeano 0 = Zero
toPeano 1 = Succ Zero
toPeano 2 = Succ (Succ Zero)

This is rather explicit. You can define Peano numbers with a simple recursion and have that work for all naturals:

toPeano 0 = Zero
toPeano x
  | x < 0 = error "Can not convert a negative number to Peano"
  | otherwise = Succ (toPeano (x-1))

The core here is the Succ (toPeano (x-1)) - this just subtracts one from the integer and adds one to the Peano construction.

Now how about the other direction? Well, every time you see "Succ" you can just add one:

fromPeano Zero = 0
fromPeano (Succ x) = 1 + fromPeano x  -- note this is inefficent but right now we don't care

Printing Results

Now the only part of what you said that looked like a question was:

I have no idea how to get it to print out the Peano Numbers given an integer.

This has nothing to do with Peano numbers, but in GHCi you can just run either of these functions:

> fromPeano (toPeano 5)
5

Or you can make a program and use print to print out results:

main = print (toPeano 5829)

and use GHC to compile the program

$ ghc --make myProg.hs
$ ./myProg
Succ (Succ (Succ (...
Thomas M. DuBuisson
  • 64,245
  • 7
  • 109
  • 166
  • is it possible to avoid this `check for < 0` by using some type of `Natural` numbers type? – Kevin Meredith Oct 15 '14 at 19:28
  • Sure, I used GADTs to encode binary in one question ([http://stackoverflow.com/questions/11910143/positive-integer-type/11912348#11912348]) and am sure there are other ways to do this. – Thomas M. DuBuisson Oct 15 '14 at 20:00
1

Would something like this be what you're looking for?

toPeano 0 = Zero
toPeano n = Succ $ toPeano (n-1)
mvarela
  • 209
  • 1
  • 3
  • 8