«K12/K13» PeanoN0.hs «PDF», «POD»

{-# OPTIONS_GHC -fglasgow-exts #-}
module PeanoN0 where

data N0 = Zero | Succ N0 deriving (Eq)

instance Show N0 where
  show n = "N0[" ++ show (toInteger n) ++ "]"

instance Num N0 where
  n + Zero     = n
  n + (Succ m) = Succ $ n + m

  n - Zero            = n
  (Succ n) - (Succ m) = n - m
  n        - m        = error $ show n ++ " - " ++ show m

  n * Zero     = 0
  n * (Succ m) = n + n * m

  abs = id

  signum Zero = Zero
  signum _    = 1

  fromInteger n | n == 0    = Zero
  fromInteger n | n  > 0    = Succ $ fromInteger (n - 1)
  fromInteger n | otherwise = error $ "fromInteger " ++ show n

instance Integral N0 where
  Zero `div` _ = 0
  n    `div` m = 1 + (n - m) `div` m

  toInteger Zero     = 0
  toInteger (Succ n) = 1 + toInteger n

instance Ord N0 where
  n <= m | n == m = True
  n <= m | m == 0 = False
  n <= m | (Succ m') <- m = n <= m'

instance Enum N0 where
  succ = Succ
  pred Zero     = error $ "pred " ++ show Zero
  pred (Succ n) = n

  toEnum   = fromInteger  . fromIntegral
  fromEnum = fromIntegral . toInteger

instance Real N0 where
  toRational = toRational . toInteger