finite-fields-0.2: Arithmetic in finite fields

Math.FiniteField.TypeLevel

Description

Type level naturals, singletons, prime witnesses and stuff.

This would be much simpler in a dependently typed language; alas, we are in Haskell, so for now we have to feel the pain.

How to use this, the over-complicated way:

• create a SomeSNat from an integer using the function someSNat
• pattern match on it with a case expression. Within the matched scope, the type parameter is "instantiated". So all your program will be "inside" this case branch (of course you can call out to functions)
• create witnesses for this being prime and/or being small using the functions isPrime and fits31Bits
• if you want small primes, create a "small prime witness" using mkSmallPrime
• now you are ready to use the resulting witness (of type IsPrime n or IsSmallPrime n) to create finite fields.

Or you can just the functions provided with each field implementation to create the fields directly (in form of existantials, ie. sigma types, so you still have to do the case _ of thing).

Synopsis

Singleton types

data SNat (n :: Nat) Source #

Nat-singletons

Instances

Instances details
 Show (SNat n) Source # Instance detailsDefined in Math.FiniteField.TypeLevel.Singleton MethodsshowsPrec :: Int -> SNat n -> ShowS #show :: SNat n -> String #showList :: [SNat n] -> ShowS #

You are responsible here!

(this is exported primarily because the testsuite is much simpler using this...)

data SNat64 (n :: Nat) Source #

Word-sized nat-singletons

Instances

Instances details
 Show (SNat64 n) Source # Instance detailsDefined in Math.FiniteField.TypeLevel.Singleton MethodsshowsPrec :: Int -> SNat64 n -> ShowS #show :: SNat64 n -> String #showList :: [SNat64 n] -> ShowS #

You are responsible here!

(this is exported primarily because the testsuite is much simpler using this...)

Creating singleton types

data SomeSNat Source #

Constructors

 forall (n :: Nat).KnownNat n => SomeSNat (SNat n)

Instances

Instances details
 Source # Instance detailsDefined in Math.FiniteField.TypeLevel.Singleton MethodsshowList :: [SomeSNat] -> ShowS #

Constructors

 forall (n :: Nat).KnownNat n => SomeSNat64 (SNat64 n)

Instances

Instances details
 Source # Instance detailsDefined in Math.FiniteField.TypeLevel.Singleton MethodsshowList :: [SomeSNat64] -> ShowS #

Small numbers

data Fits31Bits (n :: Nat) Source #

Instances

Instances details
 Source # Instance detailsDefined in Math.FiniteField.TypeLevel MethodsshowsPrec :: Int -> Fits31Bits n -> ShowS #show :: Fits31Bits n -> String #showList :: [Fits31Bits n] -> ShowS #

Creating a witness for a number being small (less than 2^31)

Primes

data IsPrime (n :: Nat) Source #

Prime witness

Instances

Instances details
 Show (IsPrime n) Source # Instance detailsDefined in Math.FiniteField.TypeLevel MethodsshowsPrec :: Int -> IsPrime n -> ShowS #show :: IsPrime n -> String #showList :: [IsPrime n] -> ShowS #

isPrime :: SNat n -> Maybe (IsPrime n) Source #

Prime testing.

Note: this uses trial division at the moment, so it's only good for small numbers for now

Escape hatch

Small primes

data IsSmallPrime (n :: Nat) Source #

Instances

Instances details
 Source # Instance detailsDefined in Math.FiniteField.TypeLevel MethodsshowsPrec :: Int -> IsSmallPrime n -> ShowS #show :: IsSmallPrime n -> String #showList :: [IsSmallPrime n] -> ShowS #

Prime testing.

Note: this uses trial division at the moment, so it's only good for small numbers for now

Escape hatch

Creating small primes

Divisors

data Divides (k :: Nat) (n :: Nat) Source #

A proof that k|n

Instances

Instances details
 Show (Divides k n) Source # Instance detailsDefined in Math.FiniteField.TypeLevel MethodsshowsPrec :: Int -> Divides k n -> ShowS #show :: Divides k n -> String #showList :: [Divides k n] -> ShowS #

data Divisor (n :: Nat) Source #

Constructors

 forall k. Divisor (Divides k n)

Instances

Instances details
 Show (Divisor n) Source # Instance detailsDefined in Math.FiniteField.TypeLevel MethodsshowsPrec :: Int -> Divisor n -> ShowS #show :: Divisor n -> String #showList :: [Divisor n] -> ShowS #

divisors :: forall n. SNat64 n -> [Divisor n] Source #

Proxy

proxyOf :: a -> Proxy a Source #

proxyOf1 :: f a -> Proxy a Source #