[Haskell-cafe] understanding Peano
daniel.is.fischer at web.de
Sat Jul 3 20:23:42 EDT 2010
On Sunday 04 July 2010 01:27:19, Patrick Browne wrote:
> 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?
No, it's all value-level.
Type level would be
data Suc n
The thing is that Suc is a value-constructor, so you can pattern-match on
But you cannot pattern match on function-results, so you can't use suc to
define the other methods of the class.
> module Peano where
> data Nat = Zero | Suc Nat deriving Show
The type Nat has two value-constructors (aka data-constructors),
Zero, which takes no argument, and Suc, which takes an argument of type
> class Peano n where
> suc :: n -> n
> eq :: n -> n -> Bool
> plus :: n -> n -> n
Note that the Peano class should also contain
zero :: n
> instance Peano Nat where
> suc = Suc
The successor function for Nat is the constructor Suc
> eq Zero Zero = True
> eq (Suc m) (Suc n) = eq m n
> eq _ _ = False
The equality-test is defined by pattern-matching.
If both arguments are Zero, they are equal.
If both arguments are constructed with Suc, they are equal if and only if
the arguments of Suc are equal.
Otherwise (one is Zero, the other a Suc something), they are not equal.
> plus m Zero = m
> plus m (Suc n) = Suc (plus m n)
Addition is defined by pattern-matching on the second argument.
If the second argument is Zero, the sum is the first argument.
If the second argument is a successor, the sum is the successor of the sum
of the first argument and the predecessor of the second.
Note that here, we could also write
plus m (Suc n) = suc (plus m n)
and use the class method on the right hand side.
and here we'd have
zero = Zero
> -- 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))
More information about the Haskell-Cafe