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 wrote:

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

On Sunday 04 July 2010 01:27:19, Patrick Browne wrote:

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?

No, it's all value-level. Type level would be data Zero data Suc n ... The thing is that Suc is a value-constructor, so you can pattern-match on Suc. But you cannot pattern match on function-results, so you can't use suc to define the other methods of the class.

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

The type Nat has two value-constructors (aka data-constructors), Zero, which takes no argument, and Suc, which takes an argument of type Nat.

class Peano n where suc :: n -> n

successor function

eq :: n -> n -> Bool

equality-test

plus :: n -> n -> n

addition Note that the Peano class should also contain zero :: n

instance Peano Nat where suc = Suc

The successor function for Nat is the constructor Suc

eq Zero Zero = True eq (Suc m) (Suc n) = eq m n eq _ _ = False

The equality-test is defined by pattern-matching. If both arguments are Zero, they are equal. If both arguments are constructed with Suc, they are equal if and only if the arguments of Suc are equal. Otherwise (one is Zero, the other a Suc something), they are not equal.

plus m Zero = m plus m (Suc n) = Suc (plus m n)

Addition is defined by pattern-matching on the second argument. If the second argument is Zero, the sum is the first argument. If the second argument is a successor, the sum is the successor of the sum of the first argument and the predecessor of the second. Note that here, we could also write plus m (Suc n) = suc (plus m n) and use the class method on the right hand side.

and here we'd have zero = Zero

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