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

Question

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

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 那样真正反射(reflect)其类型的实际结构/性质。例如，整数与实际整数并不同构(因为零出现了两次)。 Reals 需要超过一百万个单元格来存储 (3.141592)，但甚至不需要存储 100 个单元格 (4096)，这看起来不平衡。 Complex 只是 Reals 的元组，它并不能真正反射(reflect) Complex 是什么。我想知道在函数式编程语言中表达数字塔的自然、优雅的方式是什么？

Answer 1

我意识到这是一个老问题，我的答案是用 Scala 而不是 Haskell/Idris，但看看他们如何在 Spire 中做到这一点可能会很有趣。 。方法是建立代数结构的层次结构(即Semigroup/Group/Ring/Field/等)，然后在其之上实例化数值类型，添加数值方法中的各种算法。我相信人们可以在那里找到一些有用的想法。