算术和幻象类型答案

【问题标题】：Arithmoi and phantom types算术和幻象类型
【发布时间】：2019-03-27 10:23:05
【问题描述】：

我很想了解包 arithmoi (https://hackage.haskell.org/package/arithmoi-0.8.0.0) 中幻象类型的使用。它有助于检查我是否使用了正确的残基类 (Z/nZ)。

有问题的幻象类型是data Mod (n :: Nat) = Mod Natural，据我了解，构造函数没有导出。但是SomeMod的构造函数是导出的，所以我想我必须用它来构造::Mod n变量。而且，可以看文档，但是我不能用。

case modulo n m of
  SomeMod k -> process k -- Here k has type Mod m
  InfMod{}  -> error "impossible"

所以我尝试了：

foo :: KnownNat m => Nat -> Nat -> Mod m
foo n m = case modulo n m of
    (SomeMod k) -> k
    otherwise -> error "some error"

我收到一个关于变量 m 的错误，m1 正在逃逸其范围。我有点疑惑。

【问题讨论】：

您可能还喜欢Statically enforcing that two objects were created from the same (Int) “seed”。在阅读问题（以及我的答案）时，当您看到“种子”时，请考虑“模数”；当你看到Collection时，想Mod；当您看到“合并集合”时，请考虑“加法”或“乘法”或类似的操作，这些操作仅在两个参数的模数相等时才有效。

标签： haskell phantom-types

【解决方案1】：

像 IO 一样，existentials 无法逃脱。一次在存在主义中，总是在存在主义中。不过没关系——如果你愿意承认KnownNat m，你的类型签名声称你愿意这样做，那么你可以直接提升到那个类型。

foo :: KnownNat m => Natural -> Mod m
foo = fromIntegral

【讨论】：

感谢您的回答，但在这种情况下，例如无法选择使用模 2。这是不可能的吗？如果是这样的话，我不明白拥有Mod m等数据类型的目的
@jgrec 如果你在编译时无法知道模数——也就是说，如果你不愿意承认KnownNat m——那么是的，你必须进入存在领域。 “它”是否不可能在很大程度上取决于“它”是什么。对于任何m，您当然不能将SomeMod 解包成Mod m，但这几乎总是不是最终目标；而是作为通过另一种方式实现的更大目标的垫脚石。
我开始有点理解了，但是由于我无法访问Mod (::Nat) 的构造函数，并且由于我无法将SomeMod 转换为Mod，我该如何使用Mod x 进入程序（事先不知道x）？在ghci 我明白了，但不是在程序中。
@jgrec 如果您事先不知道x，则不要使用Mod x。你直接使用SomeMod。再说一遍：你想用它做什么？抽象地回答几乎是不可能的，但如果您谈论您想要执行的操作，我们可以在SomeMods 上讨论是否/如何执行这些操作。
我想计算矩阵 mod x 的行列式，但 x 必须随机选择。但是一旦选择了 x，我就不能用它来创建 mod x 值。由于SomeMod 不是Ord 的实例，线性算术库将无法执行行列式计算。也许我可以为SomeMod 编写自己的Ord 实例？但是那样我就会失去限制相同模式的矩阵的好处。使用SomeMod，我可以添加/mul 值 mod 5 和 mod 3。在某种程度上，我似乎需要依赖类型，但它可能不可行。