| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
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
SomeSNatfrom an integer using the functionsomeSNat - pattern match on it with a
caseexpression. 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
isPrimeandfits31Bits - if you want small primes, create a "small prime witness" using
mkSmallPrime - now you are ready to use the resulting witness (of type
IsPrime norIsSmallPrime 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
- data SNat (n :: Nat)
- fromSNat :: SNat n -> Integer
- proxyOfSNat :: SNat n -> Proxy n
- proxyToSNat :: KnownNat n => Proxy n -> SNat n
- unsafeSNat :: Integer -> SNat n
- data SNat64 (n :: Nat)
- fromSNat64 :: SNat64 n -> Word64
- proxyOfSNat64 :: SNat64 n -> Proxy n
- proxyToSNat64 :: KnownNat n => Proxy n -> SNat64 n
- unsafeSNat64 :: Word64 -> SNat64 n
- data SomeSNat = forall (n :: Nat).KnownNat n => SomeSNat (SNat n)
- someSNat :: Integer -> SomeSNat
- data SomeSNat64 = forall (n :: Nat).KnownNat n => SomeSNat64 (SNat64 n)
- someSNat64 :: Int64 -> SomeSNat64
- someSNat64_ :: Word64 -> SomeSNat64
- data Fits31Bits (n :: Nat)
- from31Bit :: Fits31Bits n -> Word64
- from31BitSigned :: Fits31Bits n -> Int64
- from31Bit' :: Fits31Bits n -> SNat64 n
- fits31Bits :: SNat64 n -> Maybe (Fits31Bits n)
- data IsPrime (n :: Nat)
- fromPrime :: IsPrime n -> Integer
- fromPrime' :: IsPrime n -> SNat n
- isPrime :: SNat n -> Maybe (IsPrime n)
- believeMeItsPrime :: SNat n -> IsPrime n
- data IsSmallPrime (n :: Nat)
- fromSmallPrime :: IsSmallPrime n -> Word64
- fromSmallPrimeSigned :: IsSmallPrime n -> Int64
- fromSmallPrimeInteger :: IsSmallPrime n -> Integer
- fromSmallPrime' :: IsSmallPrime n -> SNat64 n
- isSmallPrime :: SNat64 n -> Maybe (IsSmallPrime n)
- believeMeItsASmallPrime :: SNat64 n -> IsSmallPrime n
- smallPrimeIsPrime :: IsSmallPrime n -> IsPrime n
- smallPrimeIsSmall :: IsSmallPrime n -> Fits31Bits n
- mkSmallPrime :: IsPrime p -> Fits31Bits p -> IsSmallPrime p
- data Divides (k :: Nat) (n :: Nat)
- _dividend :: Divides k n -> Word64
- _divisor :: Divides k n -> Word64
- _quotient :: Divides k n -> Word64
- 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) = forall k. Divisor (Divides k n)
- constructDivisor :: SNat64 n -> SNat64 k -> Maybe (Divisor n)
- divisors :: forall n. SNat64 n -> [Divisor n]
- proxyOf :: a -> Proxy a
- proxyOf1 :: f a -> Proxy a
- checkSomeSNat :: SomeSNat -> String
- checkSomeSNat64 :: SomeSNat64 -> String
Singleton types
Nat-singletons
proxyOfSNat :: SNat n -> Proxy n Source #
unsafeSNat :: Integer -> SNat n Source #
You are responsible here!
(this is exported primarily because the testsuite is much simpler using this...)
fromSNat64 :: SNat64 n -> Word64 Source #
proxyOfSNat64 :: SNat64 n -> Proxy n Source #
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 SomeSNat64 Source #
Constructors
| forall (n :: Nat).KnownNat n => SomeSNat64 (SNat64 n) |
Instances
| Show SomeSNat64 Source # | |
Defined in Math.FiniteField.TypeLevel.Singleton Methods showsPrec :: Int -> SomeSNat64 -> ShowS # show :: SomeSNat64 -> String # showList :: [SomeSNat64] -> ShowS # | |
someSNat64 :: Int64 -> SomeSNat64 Source #
someSNat64_ :: Word64 -> SomeSNat64 Source #
Small numbers
data Fits31Bits (n :: Nat) Source #
Instances
| Show (Fits31Bits n) Source # | |
Defined in Math.FiniteField.TypeLevel Methods showsPrec :: Int -> Fits31Bits n -> ShowS # show :: Fits31Bits n -> String # showList :: [Fits31Bits n] -> ShowS # | |
from31Bit :: Fits31Bits n -> Word64 Source #
from31BitSigned :: Fits31Bits n -> Int64 Source #
from31Bit' :: Fits31Bits n -> SNat64 n Source #
fits31Bits :: SNat64 n -> Maybe (Fits31Bits n) Source #
Creating a witness for a number being small (less than 2^31)
Primes
fromPrime' :: IsPrime n -> SNat n Source #
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
| Show (IsSmallPrime n) Source # | |
Defined in Math.FiniteField.TypeLevel Methods showsPrec :: Int -> IsSmallPrime n -> ShowS # show :: IsSmallPrime n -> String # showList :: [IsSmallPrime n] -> ShowS # | |
fromSmallPrime :: IsSmallPrime n -> Word64 Source #
fromSmallPrimeSigned :: IsSmallPrime n -> Int64 Source #
fromSmallPrimeInteger :: IsSmallPrime n -> Integer Source #
fromSmallPrime' :: IsSmallPrime n -> SNat64 n Source #
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
believeMeItsASmallPrime :: SNat64 n -> IsSmallPrime n Source #
Escape hatch
smallPrimeIsPrime :: IsSmallPrime n -> IsPrime n Source #
smallPrimeIsSmall :: IsSmallPrime n -> Fits31Bits n Source #
mkSmallPrime :: IsPrime p -> Fits31Bits p -> IsSmallPrime p Source #
Creating small primes
Divisors
dividendSNat :: Divides k n -> SNat64 n Source #
divisorSNat :: Divides k n -> SNat64 k Source #
Proxy
Sanity checking
checkSomeSNat :: SomeSNat -> String Source #
checkSomeSNat64 :: SomeSNat64 -> String Source #