[Haskell-cafe] Peano axioms
pat browne
Patrick.Browne at comp.dit.ie
Thu Sep 17 14:36:37 EDT 2009
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
-}
More information about the Haskell-Cafe
mailing list