I am not quite sure what this ZInt is actually describing.
data Nat = Zero | S Nat
data ZInt = Z Nat Nat deriving Show
addZ :: ZInt -> ZInt -> ZInt
addZ (Z a b) (Z c d) = Z (add a c) (add b d)
with
add :: Nat -> Nat -> Nat
add a Zero = a
add a (S b) = S (add a b)
mult :: Nat -> Nat -> Nat
mult _ Zero = Zero
mult a (S b) = add a (mult a b)
At first glance i thought maybe it's a presentation of complex numbers, adding imaginary and real components (in function addZ) without displaying form of
a+b*i
But what is happening in this functions?
subZ :: ZInt -> ZInt -> ZInt
subZ (Z a b) (Z c d) = Z (add a d) (add b c)
multZ :: ZInt -> ZInt -> ZInt
multZ (Z a b) (Z c d) = Z (add (mult a d) (mult c b)) (add (mult a c) (mult b d))
So I do understand data Nat = Zero | S Nat and also the add and mult functions, but not addZ, subZ and multZ.
First, ZInt is representing each integer as an ordered pair of natural numbers. @freestyle covers how this representation works well; I will just expand on how the arithmetic operators take advantage of this encoding.
addZ, subZ and multZ are simply manipulating the pair of natural numbers that represent each integer.
addZ (Z a b) (Z c d) = Z (add a c) (add b d)
(a - b) + (c - d) == a - b + c - d
== a + c - b - d
== (a + c) - (b + d)
subZ (Z a b) (Z c d) = Z (add a d) (add b c)
(a - b) - (c - d) == a - b - c + d
== a + d - b - c
== (a + d) - (b + c)
multZ (Z a b) (Z c d) = Z (add (mult a d) (mult c b)) (add (mult a c) (mult b d))
(a - b) * (c - d) == ac - ad - bc + bd
== ac + bd - ad - bc
== (ac + bd) - (ad + bc)
Note that the given definition of multZ can get the sign wrong; it should be
multZ (Z a b) (Z c d) = Z (add (mult a c) (mult b d)) (add (mult a d) (mult b c))
(For clarity, it should also use mult b c instead of mult c b, even though multiplication of natural numbers is commutative.)