For me the easiest way to understand something like this is to follow the transformations of the code. Here's how your examples evaluate:
let t1 = plus (Suc (Zero)) (Suc ( Suc (Zero)))
t1 = plus (Suc (Zero)) (Suc ( Suc (Zero))) = Suc (plus (Suc (Zero)) (Suc (Zero))) = Suc (Suc (plus (Suc (Zero)) Zero)) = Suc (Suc (Suc (Zero)))
let t2 = plus (Suc (Suc(Zero))) ( Suc (Zero))
t2 = plus (Suc (Suc(Zero))) ( Suc (Zero)) = Suc (plus (Suc (Suc(Zero))) Zero) = Suc (Suc ( Suc (Zero)))
eq t1 t2 eq (Suc (Suc (Suc (Zero)))) (Suc (Suc (Suc (Zero)))) = eq (Suc (Suc (Zero))) (Suc (Suc (Zero))) = eq (Suc (Zero)) (Suc (Zero)) = eq Zero Zero = True
-deech
On Sat, Jul 3, 2010 at 7:27 PM, 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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe