[Haskell-cafe] Peano axioms

[pat browne]

Hi,
Below are two attempts to define Peano arithmetic in Haskell.
The first attempt, Peano1, consists of just a signature in the class
with the axioms in the instance. In the second attempt, Peano2, I am
trying to move the axioms into the class. The reason is, I want to put
as much specification as possible into the class. Then I would like to
include properties in the class such as commutativity something like:
infixl 5 `com`
com :: Int -> Int -> Int
x `com` y  = (x + y)
commutative com a b = (a `com` b) == (b `com` a)

I seem to be able to include just one default equation the Peano2 attempt.
Any ideas?
I have looked at
http://www.haskell.org/haskellwiki/Peano_numbers

Regards,
Pat

-- Attempt 1
-- In this attempt the axioms are in the instance and things seem OK
module Peano1 where
infixl 6 `eq`
infixl 5 `plus`

class Peano1 n where
 suc :: n -> n
 eq :: n -> n -> Bool
 plus :: n -> n -> n

data Nat = One | Suc Nat deriving Show


instance  Peano1 Nat where
 suc = Suc
 One `eq` One = True
 (Suc m) `eq` (Suc n) =  m `eq` n
 _`eq`_  = False
 m `plus` One = Suc m
 m `plus` (Suc n) = Suc (m `plus` n)
-- Evaluation *Peano1> Suc(One) `plus` ( Suc (One))





-- Attempt 2
-- In this attempt the axioms are in the class and things are not OK.
module Peano2 where
infixl 6 `eq`
infixl 5 `plus`

class Peano2 n where
  one :: n
  eq :: n -> n -> Bool
  plus :: n -> n -> n
  suc :: n -> n
  suc a = a `plus` one

{-
 I cannot add the remaining default axioms
  one `eq` one = True
  (suc m) `eq` (suc n) =  m `eq` n
  (suc a) `eq` (suc b) =  a `eq` b
  _`eq`_  = False
-}