Implementing Haskell Integer Arithmetic

For a long time it was believed that natural numbers, like numbers in general, are undetectable concepts, primary; they can be known only by intuition. However, at present all numerical sets have been given a clear definition.

The most convenient way is to determine by Peano. However, it defines countable sets, but does not give a definite constructed set. Another approach is to define a natural number as a special cardinal, namely the power of a finite set. The third is the Church numerals.

I suggest that you consider whether, with all the above definitions, numbers should be considered as predetermined concepts. Let's imagine that suddenly at one moment the whole world will be turned upside down and no single computer will be able to store numerical data. Then the programmers will be very bad. But it is worth remembering all the above and immediately everything will fall into place. We implement the type of a natural and an integer in Haskell, as an example of the definition "from scratch". As a base, take the concept of a list and define nat. the number as its length (assuming the limb of the latter).

data [a] = [] | a:[a] -- , [] : — , [] —
head x:_ = x; tail _:x = x;
data () = () -- ,

A bit of theory:
final list :: = x: (x == []) || (tail x - final)
Equality of lists is determined by []==[] = True; (a:as)==(b:bs) = (a==b) && (as==bs) []==[] = True; (a:as)==(b:bs) = (a==b) && (as==bs) provided that the elements are comparable.
Like the set-theoretic approach, we define the concept of “equalness” of lists, namely:
a ~ b :: = (a == [] && b == []) || (tail a ~ tail b)
This relation is equivalent (symmetric-transitive-reflexive), so you can build an equivalence class for each list. Take the sequence of lists [], [()], [(), ()], [(), (), ()], ..., that is, the set [()] for the base.
Between themselves, they are not equal in length, but for any finite list there is a list from the set [()] of the same length. Therefore, we identify the equivalence class to its representative from [()].
')
type N = [](); -- [()]
data Natural = MkN N; -- ,

We describe several primitive operations for natural numbers:
toList :: Natural -> N; --
toList (MkN x) = x;
incN :: Natural -> Natural; -- ,
incN = MkN.(():).toList;

--
sumN :: Natural -> Natural -> Natural;
sumN (MkN x) = MkN.(++x).toList;

copy :: a->[a]; copy x = x: copy x;
concatAll :: [[a]] -> [a];
concatAll = foldl(++)[];
table :: Natural -> a -> [a]; --
table xy = map (\_->y) $ toList x;

-- a*b a b (),
-- b a ( , )
-- concatAll
multN :: Natural -> Natural -> Natural;
multN xy = MkN $ concatAll $ table x (toList y);
decN :: Natural -> Natural;
decN (MkN(_:xs)) = MkN xs;
decN (MkN []) = error "Cannot decrease 0 staying being Natural";
zeroN :: Natural;
zeroN = MkN [];
oneN :: Natural;
oneN = MkN [()];
equalN :: Natural -> Natural -> Bool;
equalN (MkN a) (MkN b) = a==b;

There are still a few functions left:
subN :: Natural -> Natural -> Natural;
subN xy | y==oneN = decN x -- x-1=decN(x)
| y/=zeroN = decN $ subN x $ decN y -- xy=(x-1)-(y-1)
| True = x; -- x-0=x
divmodN :: Natural -> Natural -> (Natural, Natural);
divmodN (MkN []) _ = error "cannot divide by zero";
divmodN base x | moreThanN base x = (zeroN, x)
| True = let (d,m) = divmodN base (subN x base) in (incN d,m);
moreThanN :: Natural -> Natural -> Bool;
moreThanN (MkN []) _ = False;
moreThanN _ (MkN []) = True;
moreThanN xy = moreThanN (decN x) (decN y);
lengthN :: [a] -> Natural;
lengthN = MkN . map (\_->());

Now we generalize to the concept of an integer:
data Integer = Positive Natural | Negative Natural;
Let us generalize some functions of the natural argument:
absInt :: Integer -> Natural;
absInt (Positive x) = x;
absInt (Negative x) = x;
equalInt :: Integer -> Integer -> Bool;
equalInt (Positive x) (Positive y) = x `equalN` y;
equalInt (Negative x) (Negative y) = x `equalN` y;
equalInt (Negative x) (Positive y) | x==zeroN && y==zeroN = True;
equalInt (Positive x) (Negative y) | x==zeroN && y==zeroN = True;
equalInt _ _ = False;
negate :: Integer -> Integer;
negate (Positive x) = (Negative x);
negate (Negative x) = (Positive x);
sumInt :: Integer -> Integer -> Integer;
sumInt (Positive x) (Positive y) = Positive (sumN xy);
sumInt (Positive x) (Negative y) = if x `moreThanN` y then Positive (subN xy) else Negative (subN yx);
sumInt (Negative x) (Positive y) = if y `moreThanN` x then Positive (subN yx) else Negative (subN xy);
sumInt (Negative x) (Negative y) = Negative (sumN xy);

I will not give further in order to save space.

The final touch: conversion to string. The example implements a ternary system (along the length of figures)
figures = ['0', '1', '2'];
naturalseries = zeroInt : map incInt naturalseries;
figuretoInt = compare $ zip figures naturalseries where{compare ((a,b):c) x | a==x = b | True = compare cx;};
inttoFigure = getElement figures where {getElement (h:t) n = if n==zeroInt then h else getElement t $ decInt n;};
base :: Integer;
base = lengthInt figures;
showInt :: Integer -> [Char];
showInt x | x<zeroInt = '-' : showInt (negate x)
| x==zeroInt = "0"
| x<base = [inttoFigure x]
| True = let (d,m) = divmodInt base x
in (show d) ++ [inttoFigure m];
readInt :: [Char] -> (Integer, [Char]);
readInt "" = error "No integer to read on input";
readInt str@(f:r)
| f=='-' = let (i,s) = readInt r in (negate i,s)
| f=='+' = readInt r
| True = let (num,rest) = split str in (parse $ map figuretoInt num, rest);
split :: [Char] -> ([Char],[Char]);
split "" = ("","");
split (x:y) | x~->figures = let (a,b)=split y in (x:a,b)
| True = ("", x:y);
parse :: [Integer] -> Integer;
parse = foldl (\g h->sumInt h $ multInt base g) zeroInt;

We used the function of belonging the element to the list (~->) :: (Eq a) => a -> [a] -> Bool;
a ~-> [] = False;
a ~-> (b:c) = (a==b) || (a ~-> c); (~->) :: (Eq a) => a -> [a] -> Bool;
a ~-> [] = False;
a ~-> (b:c) = (a==b) || (a ~-> c);

All peace saved!

PS nothing serious. I just wanted to show that those types that are basic almost everywhere, and in many languages ​​do not allow redefinition, can be quietly defined as though from scratch.
PPS, however, I used Bool, so it is always possible to say that this type is an analogue of a bit, then somehow group together 8, 16, 32, 64 elements, which will give analogs of the types Byte, Word, ...