Implementation of Peano integer arithmetic and a few "binary peano" operations

Nats.hs

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Nats where

import Prelude hiding (even, odd)
import GHC.Real (Ratio(..))
import Test.SmallCheck
import Test.SmallCheck.Series

data Nat = ZN | S Nat
    deriving (Eq, Show)

-- Binary representation:
-- ZB = Zero (binary), T = Twice, TO = Twice plus One
data Bin = ZB | T Bin | TO Bin
    deriving (Eq, Show)

even :: Nat -> Bool
even ZN = True
even (S ZN) = False
even (S (S n)) = even n

odd :: Nat -> Bool
odd n = not (even n)

plusNat :: Nat -> Nat -> Nat
plusNat ZN k = k
plusNat (S n) k = plusNat n (S k)

multNat :: Nat -> Nat -> Nat
multNat ZN _ = ZN
multNat (S n) k = plusNat k (multNat n k)

quotRemNat :: Nat -> Nat -> (Nat, Nat)
quotRemNat _ ZN = error "divide by zero"
quotRemNat n k = go n 0
  where
    go acc count
        | acc < k = (count, acc)
        | acc >= k = go (acc - k) (count + 1)

divNat :: Nat -> Nat -> Nat
divNat n k = fst (quotRemNat n k)

minusNat :: Nat -> Nat -> Nat
minusNat ZN _ = ZN
minusNat n ZN = n
minusNat (S n) (S k) = minusNat n k

intToNat :: Integer -> Nat
intToNat 0 = ZN
intToNat n = S (intToNat (n-1))

natToInt :: Nat -> Integer
natToInt ZN = 0
natToInt (S n) = 1 + natToInt n

binToNat :: Bin -> Nat
binToNat ZB = ZN
binToNat (T b) = 2 * (binToNat b)
binToNat (TO b) = 1 + 2 * (binToNat b)

natToBin :: Nat -> Bin
natToBin ZN = ZB
natToBin (S ZN) = TO ZB
natToBin n =
    if even n
    then T (natToBin (n `divNat` 2))
    else TO (natToBin ((n-1) `divNat` 2))

-- INSTANCES
    
instance Num Nat where
    fromInteger n = intToNat n
    (+) a b = plusNat a b
    (*) a b = multNat a b
    (-) a b = minusNat a b
    abs n = n
    signum n = error "not implemented"

instance Enum Nat where
    toEnum n = intToNat (fromIntegral n)
    fromEnum n = fromIntegral (natToInt n)
    
instance Ord Nat where
    compare ZN ZN = EQ
    compare ZN _  = LT
    compare _ ZN  = GT
    compare (S n) (S k) = compare n k
    
instance Real Nat where
    toRational n = (natToInt n) :% 1

instance Integral Nat where
    toInteger = natToInt
    quotRem = quotRemNat
    
instance Monad m => Serial m Nat where
    series = cons0 ZN \/ cons1 S

-- TESTS

tests = do
    smallCheck 100 roundTripProp
    smallCheck 100 zeroProp
    smallCheck 100 globalMinimumProp

roundTripProp :: Nat -> Bool
roundTripProp n = binToNat (natToBin n) == n

zeroProp :: Nat -> Bool
zeroProp n = 0 - n == 0

-- "zero is as small as anything you can come up with"
globalMinimumProp :: Monad m => Property m
globalMinimumProp =
    forAll $ \(n :: Nat) -> exists $ \(m :: Nat) ->
        (m <= n) == True