Take the 2-minute tour ×
Code Review Stack Exchange is a question and answer site for peer programmer code reviews. It's 100% free, no registration required.
-- 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 consiceness 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` dependeing 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 quirck*)
-- *the little quirck:
-- 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 quirck 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 fucntions 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
-- convinient 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 writting (\n=> ...)

-- distance from Zero as a positive `Z`. contrast with `match` arguments that recieves 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
-- effectivly 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`

-- addition 
-- very simple and expressive interpretaion 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 quirck, 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 = "-"
share|improve this question
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.