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