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 -}