title: How do you formalize the numeric tower on functional languages?
body: <p>Everyone knows the elegant way to express natural numbers on dependently typed functional languages:</p>
  
  <pre><code>data Nat = Zero | Succ Nat
  </code></pre>
  
  <p>Integer, Fraction, Real, Complex and Quaternion are, too, very important for practical programming application. One could implement them as:</p>
  
  <pre><code>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
  </code></pre>
  
  <p>But none of those really reflect the actual structure/nature of their types as meaningfully as Nats do. Integer isn't isomorphic to actual integers, for example (as Zero occurs twice). Reals needs more than a million of cells to store (3.141592), yet not even 100 to store (4096), which looks unbalanced. Complex is just a tuple of Reals, which doesn't really reflect what a Complex is. I wonder <strong>what is the natural, elegant way to express the numeric tower on functional programming languages?</strong></p>