Math.FiniteField.TypeLevel

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).

Singleton types

data SNat (n :: Nat)

Nat-singletons

Instances

Show (SNat n)

Defined in Math.FiniteField.TypeLevel.Singleton

Methods

showsPrec :: Int -> SNat n -> ShowS

show :: SNat n -> String

showList :: [SNat n] -> ShowS

fromSNat :: SNat n -> Integer

proxyOfSNat :: SNat n -> Proxy n

proxyToSNat :: KnownNat n => Proxy n -> SNat n

unsafeSNat :: Integer -> SNat n

You are responsible here!

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

data SNat64 (n :: Nat)

Word-sized nat-singletons

Instances

Show (SNat64 n)

Defined in Math.FiniteField.TypeLevel.Singleton

Methods

showsPrec :: Int -> SNat64 n -> ShowS

show :: SNat64 n -> String

showList :: [SNat64 n] -> ShowS

fromSNat64 :: SNat64 n -> Word64

proxyOfSNat64 :: SNat64 n -> Proxy n

proxyToSNat64 :: KnownNat n => Proxy n -> SNat64 n

unsafeSNat64 :: Word64 -> SNat64 n

You are responsible here!

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

Creating singleton types

data SomeSNat

Constructors

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

Instances

Show SomeSNat

Defined in Math.FiniteField.TypeLevel.Singleton

Methods

showsPrec :: Int -> SomeSNat -> ShowS

show :: SomeSNat -> String

showList :: [SomeSNat] -> ShowS

someSNat :: Integer -> SomeSNat

data SomeSNat64

Constructors

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

Instances

Show SomeSNat64

Defined in Math.FiniteField.TypeLevel.Singleton

Methods

showsPrec :: Int -> SomeSNat64 -> ShowS

show :: SomeSNat64 -> String

showList :: [SomeSNat64] -> ShowS

someSNat64 :: Int64 -> SomeSNat64

someSNat64_ :: Word64 -> SomeSNat64

Small numbers

data Fits31Bits (n :: Nat)

Instances

Show (Fits31Bits n)

Defined in Math.FiniteField.TypeLevel

Methods

showsPrec :: Int -> Fits31Bits n -> ShowS

show :: Fits31Bits n -> String

showList :: [Fits31Bits n] -> ShowS

from31Bit :: Fits31Bits n -> Word64

from31BitSigned :: Fits31Bits n -> Int64

from31Bit' :: Fits31Bits n -> SNat64 n

fits31Bits :: SNat64 n -> Maybe (Fits31Bits n)

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

Primes

data IsPrime (n :: Nat)

Prime witness

Instances

Show (IsPrime n)

Defined in Math.FiniteField.TypeLevel

Methods

showsPrec :: Int -> IsPrime n -> ShowS

show :: IsPrime n -> String

showList :: [IsPrime n] -> ShowS

fromPrime :: IsPrime n -> Integer

fromPrime' :: IsPrime n -> SNat n

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

Prime testing.

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

believeMeItsPrime :: SNat n -> IsPrime n

Escape hatch

Small primes

data IsSmallPrime (n :: Nat)

Instances

Show (IsSmallPrime n)

Defined in Math.FiniteField.TypeLevel

Methods

showsPrec :: Int -> IsSmallPrime n -> ShowS

show :: IsSmallPrime n -> String

showList :: [IsSmallPrime n] -> ShowS

fromSmallPrime :: IsSmallPrime n -> Word64

fromSmallPrimeSigned :: IsSmallPrime n -> Int64

fromSmallPrimeInteger :: IsSmallPrime n -> Integer

fromSmallPrime' :: IsSmallPrime n -> SNat64 n

isSmallPrime :: SNat64 n -> Maybe (IsSmallPrime n)

Prime testing.

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

believeMeItsASmallPrime :: SNat64 n -> IsSmallPrime n

Escape hatch

smallPrimeIsPrime :: IsSmallPrime n -> IsPrime n

smallPrimeIsSmall :: IsSmallPrime n -> Fits31Bits n

mkSmallPrime :: IsPrime p -> Fits31Bits p -> IsSmallPrime p

Creating small primes

Divisors

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

A proof that k|n

Instances

Show (Divides k n)

Defined in Math.FiniteField.TypeLevel

Methods

showsPrec :: Int -> Divides k n -> ShowS

show :: Divides k n -> String

showList :: [Divides k n] -> ShowS

_dividend :: Divides k n -> Word64

n

_divisor :: Divides k n -> Word64

k

_quotient :: Divides k n -> Word64

q=n/k

dividendSNat :: Divides k n -> SNat64 n

divisorSNat :: Divides k n -> SNat64 k

divides :: SNat64 k -> SNat64 n -> Maybe (Divides k n)

data Divisor (n :: Nat)

Constructors

forall k. Divisor (Divides k n)

Instances

Show (Divisor n)

Defined in Math.FiniteField.TypeLevel

Methods

showsPrec :: Int -> Divisor n -> ShowS

show :: Divisor n -> String

showList :: [Divisor n] -> ShowS

constructDivisor :: SNat64 n -> SNat64 k -> Maybe (Divisor n)

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

Proxy

proxyOf :: a -> Proxy a

proxyOf1 :: f a -> Proxy a

Sanity checking

checkSomeSNat :: SomeSNat -> String

checkSomeSNat64 :: SomeSNat64 -> String