[Haskell-cafe] understanding Peano

[Daniel Fischer]

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