finite-fields-0.2.0.1: Arithmetic in finite fields
Safe HaskellSafe-Inferred
LanguageHaskell2010

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 details

Defined in Math.FiniteField.TypeLevel.Singleton

Methods

showsPrec :: Int -> SNat n -> ShowS #

show :: SNat n -> String #

showList :: [SNat n] -> ShowS #

unsafeSNat :: Integer -> SNat n Source #

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 details

Defined in Math.FiniteField.TypeLevel.Singleton

Methods

showsPrec :: Int -> SNat64 n -> ShowS #

show :: SNat64 n -> String #

showList :: [SNat64 n] -> ShowS #

unsafeSNat64 :: Word64 -> SNat64 n Source #

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
Show SomeSNat Source # 
Instance details

Defined in Math.FiniteField.TypeLevel.Singleton

data SomeSNat64 Source #

Constructors

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

Instances

Instances details
Show SomeSNat64 Source # 
Instance details

Defined in Math.FiniteField.TypeLevel.Singleton

Small numbers

data Fits31Bits (n :: Nat) Source #

Instances

Instances details
Show (Fits31Bits n) Source # 
Instance details

Defined in Math.FiniteField.TypeLevel

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

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 details

Defined in Math.FiniteField.TypeLevel

Methods

showsPrec :: 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

believeMeItsPrime :: SNat n -> IsPrime n Source #

Escape hatch

Small primes

data IsSmallPrime (n :: Nat) Source #

Instances

Instances details
Show (IsSmallPrime n) Source # 
Instance details

Defined in Math.FiniteField.TypeLevel

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

Prime testing.

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

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

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 details

Defined in Math.FiniteField.TypeLevel

Methods

showsPrec :: 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 details

Defined in Math.FiniteField.TypeLevel

Methods

showsPrec :: 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 #

Sanity checking