[Haskell-cafe] Peano axioms

[Job Vranish]

The problem is that you are using 'suc' as if it is a constructor: ((suc m)
`eq` (suc n) =  m `eq` n)
You'll have to change it to something else, and it will probably require
adding an unpacking function to your class and it will probably be messy.
I'd suggest you make use of the Eq typeclass and defined the Eq instances
separately:

class (Eq n) => Peano2 n where
 one :: n
 plus :: n -> n -> n
 suc :: n -> n
 suc a = a `plus` one

- Job

On Thu, Sep 17, 2009 at 2:36 PM, pat browne <Patrick.Browne at comp.dit.ie>wrote:

> 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
> -}
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090917/1e72ac4a/attachment-0001.html