[Haskell-cafe] understanding Peano

[aditya siram]

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 <patrick.browne at dit.ie> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>