你如何在函数式语言中形式化数字塔？

每个人都知道在依赖类型的函数语言中表达自然数的优雅方式:

data Nat = Zero | Succ Nat

整数,分数,实数,复数和四元数对于实际编程应用也非常重要.可以将它们实现为:

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

但是这些都没有真正像Nats那样有意义地反映其类型的实际结构/性质.例如,整数与实际整数不同构(因为零出现两次).Reals需要超过一百万个细胞存储(3.141592),但是甚至不需要100个存储(4096),这看起来是不平衡的.复杂只是Reals的一个元组,它并不真正反映复杂的东西.我想知道在函数式编程语言中表达数字塔的自然,优雅方式是什么？