# Integer implementation in Idris

This is a try at implementing integers in Idris. Any advice or comments are most welcome.

-- tries to implement integers using fold and a generalized notion of 'reduction' instead of
-- utilizing recursion explicitly in all operations./
-- maximum (reasonable) code reuse, information hiding and conciseness is emphasized through
-- generalized mechanisms, particularly hiding the internal representation and avoiding excessive
-- pattern matchings.
-- integers are interpreted as distances from 0 on the negative or positive sides of the
-- axis. 'reducing' (fold and loop) tries to (recursively) reach Zero which means
-- either suc or pred depending on the sign (bck).
module Z

-- an integer has a sign (P or N) and a distance from 0 (the Nat part with a little quirk*)
-- *the little quirk:
-- if P n == +n and N n == -n then both P O (+0) and N O (-0) would represent 0 which is terrible
-- since this should be taken care of throughout the module so I got smart, heeded the elders
-- advice and decided to interpret n to mean n+1 in P n and N n. this way P 0 means +1 and N 2 means -3.
-- so far only Cast Z Int instance, pred and suc had to pay. other parts of the module are
-- totally agnostic to this quirk which probably means it is the right approach.
data Z = P Nat | N Nat | Zero
data Sign = pos | neg | zro

-- picks an operation and performs it on n according to its sign and distance from 0
-- this is a powerful abstraction since many functions could be defined over it
total match : (n : Z) -> (zero : a) -> (positive : Nat->a) -> (negative : Nat->a) -> a
match Zero zero _ _ = zero
match (P n) _ positive _ = positive n
match (N n) _ _ negative = negative n

-- same as match but works on Nats
-- pay attention that input (n) comes last here
-- because nmatch is used in situations that is more
-- convenient with this arrangement
total nmatch : (zero : a) -> (nonzero : Nat->a) -> (n:Nat) -> a
nmatch zero _ O = zero
nmatch  _ nonzero (S k) = nonzero k

-- move left
total pred : Z -> Z
pred n = match n (N O) (nmatch Zero P) (N . S)

-- move right
total suc : Z -> Z
suc n = match n (P O) (P . S) (nmatch Zero N)

-- converts a constant of type a to a function that accepts a b and returns an a
-- useful in places that expect a function but a simple value would suffice.
-- parameters a and b make this mechanism very flexible.
instance Cast a (b->a) where
cast c = (\x=>c)

-- sign of an integer
total sgn : Z -> Sign
sgn n = match n zro (cast pos) (cast neg) -- employs the above Cast to prevent writing (\n=> ...)

-- distance from Zero as a positive Z. contrast with match arguments that receives the same thing as a Nat
total abs : Z -> Z
abs n = match n Zero P P

-- negation
total ngt : Z -> Z
ngt n = match n Zero N P

-- transforms n depending on its sign
-- basically match but passes the whole n instead of it's distance, effectively
-- removing duplication in such functions as fwd and bck
total caseOnSgn : (n:Z) -> (zero:a) -> (positive : Z->a) -> (negative : Z->a) -> a
caseOnSgn n zero positive negative = match n zero (positive . P) (negative . N)

-- move one number away from Zero
total fwd : Z -> Z
fwd n = caseOnSgn n Zero suc pred

-- move one number towards Zero
-- since Zero is the base case for almost all functions operating on integers, this
-- effectively defines the reducing mechanism for the whole Z as demonstrated in fold
total bck : Z -> Z
bck n = caseOnSgn n Zero pred suc

-- folding from Zero towards n
-- uses bck instead of explicit pattern matching on n thus eliminating
-- duplication , resulting in a more point-free style implementation
%assert_total
total fold : (i : Z) -> (f: Z->Z->Z) -> (n:Z) -> Z
fold i _ Zero = i
fold i f n = let acc = fold i f (bck n) in f acc n -- acc introduced for clarity

-- like fold but ignores the index
-- useful in situations where the intermediate indices are irrelevant (add)
loop : (i:Z) -> (f:Z->Z) -> (n:Z) -> Z
loop i f n = fold i (\acc,index=>f acc) n -- just discards the index

-- very simple and expressive interpretation of addition
-- m+n means :
-- moving n units to the right from m if n is positive
-- moving n units to the left from m if n is negative
-- or just m if n is Zero
add : Z -> Z -> Z
add n m = caseOnSgn m n (loop n suc) (loop n pred) -- suc : move to the right, pred : move to the left

-- subtraction
-- n-m = n + (-m)
sub : Z -> Z -> Z
sub n m = add n (ngt m)

instance Cast Z Int where
cast Zero = 0
cast (P k) = cast {to=Int} (S k) -- (S k) => the little quirk, see definition of Z
cast (N k) = -1 * cast {to=Int} (S k)

instance Show Z where
show n = show \$ cast {to=Int} n

instance Show Sign where
show zro = "0"
show pos = "+"
show neg = "-"