{-# 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