Haskell 中的 TypeNats、ViewPatterns 和 arithmoi

Question

我正在尝试理解 typenats 和 KnownNat 等。复制我想出的代码：

toMod :: KnownNat m => proxy m -> Integer -> Mod m
toMod _ = fromInteger


-- Does the conversions to call discreteLogarithm
-- Solves b^x == a mod g for x 
hack :: Integer -> Natural -> Integer -> Maybe Integer
hack b pn@(someNatVal -> SomeNat gSize) a =
  do 
  let amod = toMod gSize a

  cg <- cyclicGroup
  primitiveRootb <- isPrimitiveRoot cg (fromInteger b)
  multmoda <- isMultElement amod
  pure $ naturalToInteger $ discreteLogarithm cg primitiveRootb multmoda

但我不太明白代码是如何工作的。例如 - ViewPattern 将 gSize 提取为代理，我可以在没有 Viewpattern 的代码中执行此操作吗？我在 someNatVal() 上尝试了模式匹配，但我无法让它工作。

我看到toMod()可以从Proxy gSize中得到group size，但是cyclicGroup，cg是怎么知道的呢？

Answer 1

诀窍在于 cyclicGroup、isPrimitiveRoot 和 isMultElement 的结果都有一个 m :: Nat 类型参数。这由类型检查器统一，因此您最终将 m 作为隐式参数传递给所有这些函数。

Answer 2

以下应该可以很好地避免视图模式：

hack :: Integer -> Natural -> Integer -> Maybe Integer
hack b pn a =
  case someNatVal pn of
    SomeNat gSize -> do
      let amod = toMod gSize a
      cg <- cyclicGroup
      primitiveRootb <- isPrimitiveRoot cg (fromInteger b)
      multmoda <- isMultElement amod
      pure $ naturalToInteger $ discreteLogarithm cg primitiveRootb multmoda

您可能尝试了类似以下的方法，但失败了：

hack :: Integer -> Natural -> Integer -> Maybe Integer
hack b pn a = do
  let SomeNat gSize = someNatVal pn
      amod = toMod gSize a
  cg <- cyclicGroup
  primitiveRootb <- isPrimitiveRoot cg (fromInteger b)
  multmoda <- isMultElement amod
  pure $ naturalToInteger $ discreteLogarithm cg primitiveRootb multmoda

在这里，someNatVal pn 产生一个 SomeNat 类型的存在定义如下：

data SomeNat = forall m. KnownNat m => SomeNat (Proxy m)

在 Haskell 中，您通常通过对它们进行大小写匹配来使用存在性：

case someNatVal pn of SomeNat gSize -> ...

这具有将它们变回正常的、不存在的值的效果，但是仅在 case 语句右侧的范围内.因此，在“...”部分，您可以将 gSize :: Proxy m 视为类型级自然数的典型代理，并且您可以利用其 KnownNat m 字典来获取其运行-时间值（你不直接使用它，但是 toMod 需要它，例如）。您还可以利用类型检查器来匹配不同类型的 m，这样 cyclicGroup、isPrimitiveRoot 和 discreteLogarithm 最终都使用相同的模数 m，因为这是他们进行类型检查的唯一方式（具体来说，请参阅 discreteLogarithm 的类型签名，它将所有参数的模数联系在一起）。

但是，您必须在“...”部分中完成类型 m。它和它的 KnownNat n 字典不存在于案例的右侧之外。这就是为什么在 case 分支中包含整个函数其余部分的版本可以工作，但是 let-绑定 SomeNat gSize 然后尝试对其类型进行操作的版本失败的原因。视图模式有效，不是因为它做了什么神奇的事情，而是因为整个函数体被认为在隐含的大小写匹配中。

Haskell 中的 TypeNats、ViewPatterns 和 arithmoi

TypeNats, ViewPatterns and arithmoi in Haskell

proxy

haskell

discrete-mathematics

typeliteral