How do you formalize a number tower in functional languages?

Question

Everyone knows an elegant way to express natural numbers in functionally dependent languages:

data Nat = Zero | Succ Nat 

The integer, fraction, real, complex and quaternion are also very important for practical programming. They could be implemented as:

 data Integer = Integer (sign : Bool) (modulus : Nat) data Fraction = Fraction (dividend : Nat) (divisor : Nat) data Real = Real (exponent : Integer) (fraction : Nat) data Complex = Complex Real Real data Quaternion = Quaternion Real Real Real Real 

But not one of them really reflects the actual structure / nature of their types as significant as the Nuts does. An integer is not isomorphic to real integers, for example (since Zero occurs twice). Realities need more than a million cells to store (3.141592), but not even 100 to store (4096), which looks unbalanced. The Complex is just a Reals tuple that does not really reflect what the Complex is. Interestingly, what is a natural, elegant way to express a number tower in functional programming languages?

Answer 1

I understand that this is an old question, and my answer is in Scala, not in Haskell / Idris, but it would be interesting to see how they do it in Spire . The approach is to first create a hierarchy of algebraic structures (i.e. Semigroup / Group / Ring / Field / etc.), And then create an instance of the numeric types on top of them by adding various algorithms from the numeric methods. I’m sure that there you can find useful ideas.