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.bro...@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@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
