TypeNats, ViewPatterns and arithmoi in Haskell

Question

I am trying to understand typenats and KnownNat etc. Copying code I have come up with:

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

But I don't really understand how the code works. For example - the ViewPattern extracts the gSize as a Proxy, can I do this in code without the Viewpattern? I tried pattern matching on someNatVal() but I couldn't get it to work.

I can see that toMod() can get the group size from the Proxy gSize, but how does the cyclicGroup, cg, know?

Answer 1

The following should work fine to avoid the view pattern:

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

You probably tried something like the following, which fails:

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

Here, someNatVal pn produces an existential of type SomeNat defined something like:

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

In Haskell, you generally use existentials by case-matching on them:

case someNatVal pn of SomeNat gSize -> ...

This has the effect of turning them back into normal, non-existential values, but only within the scope of the right-hand side of the case statement. So, within the "..." part, you can treat gSize :: Proxy m as a typical proxy for a type-level natural, and you can take advantage of its KnownNat m dictionary to get its run-time value (which you don't use directly, but toMod needs it, for example). You can also leverage the type-checker to match m across different types, so that cyclicGroup, isPrimitiveRoot, and discreteLogarithm all end up using the same modulus m, because that's the only way they'll type check (specifically, see the type signature of discreteLogarithm which will tie the moduli of all of its arguments together).

However, you have to finish up with the type m within the "..." part. It and its KnownNat n dictionary don't exist outside the right-hand side of the case. That's why the version that includes the entire rest of the function within the case branch works, but a version that let-binds SomeNat gSize and then tries to operate on its type fails. The view pattern works, not because it does anything magical, but because the entire function body is considered to be within the implied case-match.