[Haskell-cafe] understanding Peano
wolfon at gmail.com
Sat Jul 3 20:06:14 EDT 2010
> 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))
> 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
More information about the Haskell-Cafe