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