Created
January 30, 2018 21:05
-
-
Save twopoint718/6c474d726a8fad686c53af87be099eb1 to your computer and use it in GitHub Desktop.
Implementation of Peano integer arithmetic and a few "binary peano" operations
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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