haskell - 算术和幻象类型

Question

我很想了解 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 的错误，它正在逃逸其范围。我有点疑惑。

score 4 · Accepted Answer

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

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

1 回答 1