[Haskell-cafe] understanding Peano

[Andrew Korzhuev]

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)
>    
Look's like author would like to declare an increment function instead 
of suc lately.
> 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)
>    
And plus stands for reqursive unfolding second argument till it becomes 
Zero and then substitute first argument into it.
>
>
> -- 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
>