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

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

Answer 1

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