Skip to content

Instantly share code, notes, and snippets.

@twopoint718
Created January 30, 2018 21:05
Show Gist options
  • Save twopoint718/6c474d726a8fad686c53af87be099eb1 to your computer and use it in GitHub Desktop.
Save twopoint718/6c474d726a8fad686c53af87be099eb1 to your computer and use it in GitHub Desktop.
Implementation of Peano integer arithmetic and a few "binary peano" operations
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment