[Haskell-cafe] understanding Peano

[Patrick Browne]

Hi,
I would like to understand the Peano module below.
I do wish to implement or improve the code.
I am unsure of the semantics of (suc = Suc) and then the subsequent use
of  (Suc n)
Is this an example of type-level programming?


module Peano where
data Nat = Zero | Suc Nat deriving Show

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


instance  Peano Nat where
 suc = Suc
 eq Zero Zero = True
 eq (Suc m) (Suc n) = eq m n
 eq _ _ = False
 plus m Zero = m
 plus m (Suc n) = Suc (plus m n)



-- Some evaluations
let t1 = plus (Suc (Zero)) (Suc ( Suc (Zero)))
let t2 = plus (Suc (Suc(Zero))) ( Suc (Zero))
is 1+2=2+1?
eq t1 t2 -- true
*Peano> :t plus (Suc (Suc(Zero))) ( Suc (Zero))

regards,
Pat

This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie