Create a :%: modular newtype

[echatav]

newtype (:%:) (int :: Type) (modulus :: Natural) = UnsafeMod int

This is the Mod type from #177 proof-of-concept

Motivation is to model things as what they are. For instance, in elliptic curve crypto, point coordinates are fixed width integer types in their (big-endian?) bit-representation. But the arithmetic functions that operate on them depend on a prime modulus which is smaller than their width. With (:%:) and the largeword library that can be represented directly.

[TurtlePU]

Can we have modulus :: int instead to have a more general implementation (a factorization by an ideal with a single generator)?

[echatav]

Sure, even more generally it's possible to make modulus be polykinded, as it is a phantom parameter.

newtype (:%:) (int :: Type) (modulus :: kind) = UnsafeMod int

[echatav]

But there's a couple reasons we want modulus :: Natural for the case of modular arithmetic, including prime fields. The first is just mathematical that an integer modulus is invariant under sign change,

forall x y n : Integer.
x = y mod n <=> x = y mod (-n)

The second is just pragmatic, Haskell's Integer type doesn't promote to an Integer kind, with any useful operations. Natural on the other hand is self-promoted and has type-level literals as well as operations that let us implement primality checks and take logs, etc. We can implement our own Z kind; I even recently made one here. But it's really unnecessary for just modular arithmetic I think.

[TurtlePU]

We can link int and kind with Demote in the link you provided, actually!

[echatav]

You can link int and kind with Demote kind ~ int, presuming you want to define an instance SingKind kind. However, for many kinds you won't be able to construct a type of that kind, at least not in an obvious way. For instance, you can't construct type Six :: Word8; type Six = 6 because type level numeric literals only work for Natural (and synonyms). Also, consider that Natural can always be linked to any (semi-)integral int using fromIntegral or its ilk after demoting.

It makes sense to make the modulus polykinded because we can interpret a quotient type in different ways for different modulus kinds, even with non-integral numerator types like perhaps polynomials. But focusing on the use case of modular arithmetic, I think that, for example, Word8 :%: 6 contains exactly and only what type-level information is needed (to represent Z/6 in as few bytes as possible). In the use case of elliptic curves a modulus will be a publicly known prime given in published curve standards. These are all currently kinded sensibly as Naturals like so:

type Ed25519_Scalar = 7237005577332262213973186563042994240857116359379907606001950938285454250989

type BN254_Base = 21888242871839275222246405745257275088696311157297823662689037894645226208583

My hope is that this will be conducive for translating between Haskell and Symbolic byte level representations, or abstracting typeclass interfaces they may share. The numerator type for prime field quotient types will be a largeword datatype like Word256 in parallel to a Symbolic datatype like Symbolic context => UInt 256 Auto context.

[TurtlePU]

Consider the following type: Word8 :%: Ed25519_Scalar. How do we prevent anyone from using such datatypes?

[echatav]

I don't think it's important to prevent that 🤷 Just have error function implementations if/when they don't make sense.