使用 Haskell 类型族或 GADT 的模块化算术？

Posted 2023-02-18

【中文标题】使用 Haskell 类型族或 GADT 的模块化算术？

【英文标题】：Modular Arithmetic using Haskell Type-Families or GADTs?

【发布时间】：2015-12-25 20:28:45

【问题描述】：

我经常有机会在 Haskell 中执行模运算，其中模通常很大并且通常是素数（例如 2000000011）。目前，我只使用（modAdd mab）、（modMul mab）、（modDiv mab）等函数。但这很不方便，需要始终指定和携带一个附加参数，并在常规积分中创建我的各种函数形式和单独的形式。

因此，创建一个类似这样的新类可能是个好主意：

class Integral a => Mod a

m = 2000000011

instance Integral a => Num (Mod a) where
   ... defining (+), etc. as modulo m

然后人们可以只执行常规算术，使用常规函数，并定义有用的结构，如

factorials :: [Mod Int]
factorials = 1:zipWith (*) factorials [1..]

但这有一个问题：Mod Int 类型的所有值都必须具有相同的模数。但是，我经常需要在一个程序中处理多个模数（当然总是只组合相同模数的值）。

我认为，但不能很好地确定，这可以通过以下方式克服：

class Integral a => Mod Nat a

其中 Nat 是一种以 Peano 方式对模数进行编码的类型。这将是有利的：我可以有不同模数的值，并且类型检查器可以避免我意外地组合这个值。

这样的事情可行且有效吗？如果我尝试使用该模数，是否会导致编译器或 RTS 尝试实际构建巨大的 (Succ (Succ (Succ ... 重复 2000000011 次)，从而使解决方案有效地无用？RTS 会尝试检查每个操作的类型匹配？每个值的 RTS 表示是否会从原本可能只是一个未装箱的 int 中被炸毁？

有没有更好的办法？

结论

感谢cirdec、dfeuer、user5402 和tikhon-jelvis 提供的帮助，我了解到（不出所料）我不是第一个有这个想法的人。特别是，Kiselyov 和 Shan 最近的 paper 提供了一个实现，并且 tikhon-jelvis 已向 Hackage 发布了一个名为（惊喜！）modular-arithmetic 的解决方案，该解决方案使用花哨的 ghc 编译指示提供了更好的语义。

打开问题（对我）

幕后发生了什么？特别是，[Mod Int 2000000011] 的一百万个元素列表是否会携带额外的一百万个 2000000011 副本？或者它是否编译为与单独携带模数参数的一百万个 Int 列表相同的代码？后者会很好。

性能附录

我针对我正在处理的当前问题运行了一些基准测试。第一次运行使用了一个未装箱的 10,000 元素 Int 向量并对其执行了 10,000 次操作：

   4,810,589,520 bytes allocated in the heap
         107,496 bytes copied during GC
       1,197,320 bytes maximum residency (1454 sample(s))
         734,960 bytes maximum slop
              10 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0      6905 colls,     0 par    0.109s   0.101s     0.0000s    0.0006s
  Gen  1      1454 colls,     0 par    0.812s   0.914s     0.0006s    0.0019s

  TASKS: 13 (1 bound, 12 peak workers (12 total), using -N11)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.000s  (  0.001s elapsed)
  MUT     time    2.672s  (  2.597s elapsed)
  GC      time    0.922s  (  1.015s elapsed)
  EXIT    time    0.000s  (  0.001s elapsed)
  Total   time    3.594s  (  3.614s elapsed)

  Alloc rate    1,800,454,557 bytes per MUT second

  Productivity  74.3% of total user, 73.9% of total elapsed

第二次运行时，我对一个未装箱的 10,000 向量（Mod Int 1000000007）执行了相同的操作。这使我的代码更简单一些，但花费了大约 3 倍的时间（同时具有几乎相同的内存配置文件）：

   4,810,911,824 bytes allocated in the heap
         107,128 bytes copied during GC
       1,199,408 bytes maximum residency (1453 sample(s))
         736,928 bytes maximum slop
              10 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0      6906 colls,     0 par    0.094s   0.107s     0.0000s    0.0007s
  Gen  1      1453 colls,     0 par    1.516s   1.750s     0.0012s    0.0035s

  TASKS: 13 (1 bound, 12 peak workers (12 total), using -N11)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.000s  (  0.001s elapsed)
  MUT     time    8.562s  (  8.323s elapsed)
  GC      time    1.609s  (  1.857s elapsed)
  EXIT    time    0.000s  (  0.001s elapsed)
  Total   time   10.172s  ( 10.183s elapsed)

  Alloc rate    561,858,315 bytes per MUT second

  Productivity  84.2% of total user, 84.1% of total elapsed

我想知道为什么会发生这种情况以及是否可以解决。不过，我真的很喜欢模块化算术包，并且会在性能不是绝对关键的地方使用它。

【问题讨论】：

您可能对论文Functional Pearl: Implicit Configuration 和相应的reflection 包感兴趣。

请注意，reflection 中与 Given 相关的所有内容都被认为是不明智的；其余的真的很酷。

现在正在看报纸。很有意思。感谢 Cirdec 和 dfeuer。这可能正是我想要的。我剩下的主要困惑点是，是否有可能构造 Kiselyov/Shan 模数而不会将它们视为废弃参数的函数。

【参考方案1】：

较新版本的 GHC 内置了类型级别的数字，它应该比您使用 Peano 算术自己滚动的数字更有效。您可以通过启用DataKinds 来使用它们。作为奖励，您还将获得一些不错的语法：

factorials :: [Mod Int 20]

这是否有效取决于您如何实现Mod 类型。在最一般的情况下，您可能只想在每次算术运算之后只使用mod。除非您处于保存少量指令很重要的热循环中，否则这应该没问题。 （在热循环中，最好明确说明您何时修改。）

我实际上在 Hackage 上的一个库中实现了这种类型：modular-arithmetic。它有一个测试套件，但没有基准，所以我不能保证绝对性能，但它没有做任何应该很慢的事情，而且对于我的目的来说已经足够快了。 （诚​​然，这涉及到小的模数。）如果您尝试它并遇到性能问题，我很想听听它们，以便我可以尝试修复它们。

【讨论】：

非常好。看起来你已经完全按照我的想法做了。一个问题：为什么要定义一个新的“inv”函数，而不是实例化 Fractional 并使用 recip？这也为您提供了 fromRational 和 /，这两者通常都对模数有意义。

@CarlEdman：啊，公平点。我只是没有想到，但这似乎是有道理的，虽然也许有些行为不直观？ （fromRational 感觉有点奇怪...）你能打开一个GitHub issue 或拉取请求吗？谢谢！

【参考方案2】：

这是一些使用Data.Reflection的工作代码：

-# LANGUAGE Rank2Types #-
-# LANGUAGE FlexibleContexts #-

import Data.Reflection
import Data.Proxy

data M a s = M a -- Note the phantom comes *after* the concrete

-- In `normalize` we're tying the knot to get the phantom types to align
-- note that reflect :: Reifies s a => forall proxy. proxy s -> a

normalize :: (Reifies s a, Integral a) => a -> M a s
normalize a = b where b = M (mod a (reflect b)) 

instance (Reifies s a, Integral a) => Num (M a s) where
  M a + M b = normalize (a + b)
  M a - M b = normalize (a - b)
  M a * M b = normalize (a * b)
  fromInteger n = normalize (fromInteger n)
  abs _     = error "abs not implemented"
  signum _  = error "sgn not implemented"

withModulus :: Integral a => a -> (forall s. Reifies s a => M a s) -> a
withModulus m ma = reify m (runM . asProxyOf ma)
  where asProxyOf :: f s -> Proxy s -> f s
        asProxyOf a _ = a

runM :: M a s -> a
runM (M a) = a

example :: (Reifies s a, Integral a) => M a s
example = normalize 3

example2 :: (Reifies s a, Integral a, Num (M a s)) => M a s
example2 = 3*3 + 5*5

mfactorial :: (Reifies s a, Integral a, Num (M a s)) => Int -> M a s
mfactorial n = product $ map fromIntegral [1..n]

test1 p n = withModulus p $ mfactorial n

madd :: (Reifies s Int, Num (M Int s)) => M Int s -> M Int s -> M Int s
madd a b = a + b

test2 :: Int -> Int -> Int -> Int
test2 p a b = withModulus p $ madd (fromIntegral a) (fromIntegral b)

【讨论】：

为避免混淆，我强烈建议您在使用启用forall 关键字的扩展时使用ScopedTypeVariables。在这里没有区别，但我不喜欢考虑它是打开还是关闭。

事实上，ScopedTypeVariables 在这里非常有用，可以避免打结。只需使用normalize :: forall s a . (Reifies s a, Integral a) => a -> M a s，然后使用normalize a = M (mod a (reflect (Proxy :: Proxy s)))

完全同意，当我第一次得知类型变量是 not 作用域时，我感到非常震惊。 ScopedTypeVariables 确实属于 Haskell'。