{-# LANGUAGE NoImplicitPrelude, ExplicitForAll #-}
-- | Defines natural numbers and operations on them.
module Data.Hextra.Nat.Internal where
import qualified Prelude as P
import Extra.Function as Fun
import Extra.Tuple as Tup
import Extra.Integral as Int
data N = Z | S N
-- ^ Inductive natural number type
-- Z is 0, S is the successor function
-- S is equivalent to (+ 1)
(+) :: N -> N -> N
Z + y = y
(S x) + y = S (x + y)
-- ^ Addition of natural numbers
-- Zero is the identity, and therefore, a base case.
-- Otherwise, recursively peels away S layers from argument,
-- applies (+) again, and applies S on the whole.
(*) :: N -> N -> N
Z * _ = Z
(S x) * y = (x * y) + y
-- ^ Multiplication of natural numbers
-- Explanation 1:
-- Zero is an annihilator, and therefore, a base case.
-- Otherwise, recursively peel away S layers from one argument,
-- apply (*) again, and apply (+) with the untouched argument on the whole.
-- annihilator = element which is always returned by the operation (in this case (*))
-- forall x. x \<\> annihilator == annihilator
-- This works because multiplication is iterated addition.
-- Explanation 2:
-- This is an implementation of iterated addition.
-- Whenver one is removed from argument 1, argument 2 is added to the actual value,
-- so argument 2 is added argument 1 times to the actual value,
-- and since the base case for the recursion is always zero, the result is argument 1 times argument 2.
(-) :: N -> N -> N
Z - y = y
x - Z = x
(S x) - (S y) = x - y
-- ^ Difference between two natural numbers
-- This exploits the fact that,
-- if you add something to two numbers, the difference stays the same.
-- Peels away a layer of S on both arguments and then apllies itself again.
min :: N -> N -> N
min Z _ = Z
min _ Z = Z
min (S x) (S y) = S (min x y)
-- ^ Finds the smaller of two natural numbers.
-- Zero is smaller than any other natural number, this is the recursion base case.
-- TODO Rewrite the following explanation
-- When subtracting one, you don't change which number is the smallest,
-- so you just need to add one.
max :: N -> N -> N
max Z y = y
max x Z = x
max (S x) (S y) = S (max x y)
-- ^ Finds the larger of two natural numbers.
-- Any other natural number is larger than zero, this is the recursion base case.
-- TODO Rewrite the following explanation
-- When subtracting one, you don't change which number is the largest,
-- so you just need to add one.
-- subtracting ^= peeling away a layer of S
toInteger :: N -> P.Integer
toInteger Z = 0
toInteger (S n) = 1 P.+ toInteger n
-- ^ Converts natural numbers to integers.
-- Z converts to zero, and S ^= (+1).
fromInteger :: P.Integer -> N
fromInteger n = case P.compare 0 n of
P.GT -> S (fromInteger (n P.+ 1))
P.EQ -> Z
P.LT -> S (fromInteger (n P.- 1))
-- ^ Converts integers to natural numbers.
-- Reduces value towards 0 while applying S.
-- Negative integers don't raise errors, but are treated like their positive counterparts.
quotRem :: N -> N -> (N, N)
quotRem = tBothmap fromInteger .> P.quotRem <. toInteger
-- ^ Division and Modulo of natural numbers
-- This just converts them to integers, divides, and converts back.
-- (\<.) and (.\>) are functions for composing two-argument and one-argument functions (from Extra.Function).
-- TODO Consider writing explicit definition
quot = P.fst .> quotRem
rem = P.snd .> quotRem
-- ^ Division and Modulo of natural numbers, respectively
-- Just extracts the first and second elements of the result of quotRem.
difference :: forall n. P.Integral n => N -> N -> n
difference = (P.-) <. toIntegral
-- ^ Subtraction of two natural numbers. The result is not necessarily a natural number.
-- For example, 7 - 21 = (-14), which isn't a natural number,
-- hence a polymorphic type including an integral constraint.
-- Named numbers (up to 12):
zero = Z
one = S Z
-- ^ One (Zero + 1)
two = S one
three = S two
four = S three
five = S four
six = S five
seven = S six
eight = S seven
nine = S eight
ten = S nine
eleven = S ten
twelve = S eleven
-- Instances of N:
instance P.Num N where
(+) = (+)
(-) = (-)
(*) = (*)
fromInteger = fromInteger
negate = P.id
abs = P.id
signum = P.const one
instance P.Eq N where
Z == Z = P.True
Z == _ = P.False
_ == Z = P.False
(S x) == (S y) = x P.== y
instance P.Ord N where
compare Z Z = P.EQ
compare Z _ = P.LT
compare _ Z = P.GT
compare (S x) (S y) = P.compare x y
instance P.Enum N where
succ = S
pred Z = Z
pred (S x) = x
fromEnum = P.fromInteger P.. toInteger
toEnum = P.fromIntegral
instance P.Real N where
toRational = P.toRational P.. toInteger
instance P.Integral N where
quotRem = quotRem
divMod = quotRem
toInteger = toInteger
instance P.Show N where
showsPrec x = P.showsPrec x P.. toInteger
show = P.show P.. toInteger
showList = P.showList P.. P.map toInteger