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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe