Improve return type of isPrimitiveRoot'

[Bodigrim]

Since PrimitiveRoot a is an abstract data type with a hidden constructor (#130), function isPrimitiveRoot' :: CyclicGroup a -> a -> Bool is pretty much useless: even if it returns True, there are no means to use this boolean as an evidence to construct a PrimitiveRoot value. And the only way to get PrimitiveRoot is using isPrimitiveRoot :: Mod n -> Maybe (PrimitiveRoot n), which runs (possibly expensive) cyclicGroupFromModulo for each candidate.

I do not have any good ideas at the moment, how to fix this.

[b-mehta]

I strongly agree. A large part of this issue is that PrimitiveRoot has an associated modulus on the type level but CyclicGroup does not, so we cannot return a PrimitiveRoot immediately from a CyclicGroup. I suspect an appropriate resolution might need to modify one or both of the types CyclicGroup and PrimitiveRoot.

[Bodigrim]

As a palliative measure we may add a semantic equivalent of fmap isPrimitiveRoot, which constructs a CyclicGroup only once per list of arguments. At least, this will greatly speed up the search of the minimal primitive root.

arePrimitiveRoots :: (Functor f, KnownNat n) => f (Mod n) -> f (Maybe (PrimitiveRoot n))
arePrimitiveRoots = undefined

It seems that a proper solution should include promoting factorisation of modulo to the type level. In this case we can both ensure type safety (that m from Mod m matches modulo of CyclicGroup) and keep factors readily available. This type-foo is technically doable, but kinda involved. I am not sure how practical it is.

[b-mehta]

This sounds like a reasonable temporary fix.

In experimenting for #119 I tried modulo factorisation on the type-level, and it came out fairly unwieldy and impractical: as far as I can tell, we would effectively need a type-level proof of the fundamental theorem.

[Bodigrim]

Sounds like a challenge :)

[b-mehta]

I've sketched a possible new type structure to fix this in #158, but it would be a breaking change if it fully replaces the existing CyclicGroup. Also, the structure I describe is restricted to Natural, but I do not think this is much of a restriction.

[Bodigrim]

I am fine with breaking changes here.

[b-mehta]

In that case, shall I continue with the PR and propagate the change through tests and benchmarks, replacing the existing structures?

[Bodigrim]

Yes, please proceed.

I am not totally convinced in design of CyclicGroup at the moment, but let us see how it unfolds. Restriction to Natural is not very cool (because we rarely have groups larger than 2^64), but should not harm performance since discrete logarithms are tied to Integer anyways. And putting modulo on type level of CyclicGroup makes impossible constructing lists of cyclic groups, but - again - we do not ever construct such lists.

---

Hmm, CyclicGroup m is a singleton type (such that is inhabited by a single value). We might push this approach further, introducing a more general type like

data Foo (m :: Nat) = Foo [(Prime Natural, Word)]

where the term-level list is a factorisation of a type-level integer. It looks like a way to achieve both type safety and avoid repetitive factorisations in M.NT.Moduli.Equations and other places. Instead of

solveQuadratic :: KnownNat m => Mod m -> Mod m -> Mod m -> [Mod m]

which is vastly inefficient in loops like map (solveQuadratic 1 2) [1..1000] :: [[Mod 1234567890]], we will have

solveQuadratic' :: KnownNat m => Foo m -> Mod m -> Mod m -> Mod m -> [Mod m]

[b-mehta]

I'm similarly unsure about the design. Perhaps we could parametrise by the type, for something like CyclicGroup a (n :: Nat), where a will typically be Natural or Word?

And putting modulo on type level of CyclicGroup makes impossible constructing lists of cyclic groups, but - again - we do not ever construct such lists.

My suspicion is that it might possibly be nice to construct such a list eventually, since we can store the structure of multiplicative groups as a product of cyclic groups.

I'll submit a PR for Dirichlet characters soon, where I think similar ideas can be used.

[Bodigrim]

I've been exploring the idea of singletons in 8ecb8e9. They fit nicely for M.NT.Moduli.Equations and M.NT.Moduli.Sqrt.