| Copyright | (c) 2019 Andrew Lelechenko |
|---|---|
| License | MIT |
| Maintainer | Andrew Lelechenko <andrew.lelechenko@gmail.com> |
| Safe Haskell | None |
| Language | Haskell2010 |
Math.NumberTheory.Moduli.Singleton
Description
Singleton data types.
Synopsis
- data SFactors a (m :: Nat)
- sfactors :: forall a m. (Ord a, UniqueFactorisation a, KnownNat m) => SFactors a m
- someSFactors :: (Ord a, Num a) => [(Prime a, Word)] -> Some (SFactors a)
- unSFactors :: SFactors a m -> [(Prime a, Word)]
- proofFromSFactors :: Integral a => SFactors a m -> () :- KnownNat m
- data CyclicGroup a (m :: Nat)
- cyclicGroup :: forall a m. (Integral a, UniqueFactorisation a, KnownNat m) => Maybe (CyclicGroup a m)
- cyclicGroupFromFactors :: (Eq a, Num a) => [(Prime a, Word)] -> Maybe (Some (CyclicGroup a))
- cyclicGroupFromModulo :: (Integral a, UniqueFactorisation a) => a -> Maybe (Some (CyclicGroup a))
- proofFromCyclicGroup :: Integral a => CyclicGroup a m -> () :- KnownNat m
- pattern CG2 :: CyclicGroup a m
- pattern CG4 :: CyclicGroup a m
- pattern CGOddPrimePower :: Prime a -> Word -> CyclicGroup a m
- pattern CGDoubleOddPrimePower :: Prime a -> Word -> CyclicGroup a m
- cyclicGroupToSFactors :: Num a => CyclicGroup a m -> SFactors a m
- sfactorsToCyclicGroup :: (Eq a, Num a) => SFactors a m -> Maybe (CyclicGroup a m)
- data Some (a :: Nat -> Type) where
SFactors singleton
data SFactors a (m :: Nat) Source #
This singleton data type establishes a correspondence
between a modulo m on type level
and its factorisation on term level.
Instances
sfactors :: forall a m. (Ord a, UniqueFactorisation a, KnownNat m) => SFactors a m Source #
Create a singleton from a type-level positive modulo m,
passed in a constraint.
>>>:set -XDataKinds>>>sfactors :: SFactors Integer 13SFactors {unSFactors = [(Prime 13,1)]}
someSFactors :: (Ord a, Num a) => [(Prime a, Word)] -> Some (SFactors a) Source #
Create a singleton from factors of m.
Factors must be distinct, as in output of factorise.
>>>import Math.NumberTheory.Primes>>>someSFactors (factorise 98)SFactors {unSFactors = [(Prime 2,1),(Prime 7,2)]}
proofFromSFactors :: Integral a => SFactors a m -> () :- KnownNat m Source #
Convert a singleton to a proof that m is known. Usage example:
toModulo :: SFactors Integer m -> Natural toModulo t = case proofFromSFactors t of Sub Dict -> natVal t
CyclicGroup singleton
data CyclicGroup a (m :: Nat) Source #
This singleton data type establishes a correspondence
between a modulo m on type level
and a cyclic group of the same order on term level.
Instances
cyclicGroup :: forall a m. (Integral a, UniqueFactorisation a, KnownNat m) => Maybe (CyclicGroup a m) Source #
Create a singleton from a type-level positive modulo m,
passed in a constraint.
>>>:set -XDataKinds>>>import Data.Maybe>>>cyclicGroup :: Maybe (CyclicGroup Integer 169)Just (CGOddPrimePower' (Prime 13) 2)
>>>:set -XTypeOperators -XNoStarIsType>>>import GHC.TypeNats>>>sfactorsToCyclicGroup (sfactors :: SFactors Integer 4)Just CG4'>>>sfactorsToCyclicGroup (sfactors :: SFactors Integer (2 * 13 ^ 3))Just (CGDoubleOddPrimePower' (Prime 13) 3)>>>sfactorsToCyclicGroup (sfactors :: SFactors Integer (4 * 13))Nothing
cyclicGroupFromFactors :: (Eq a, Num a) => [(Prime a, Word)] -> Maybe (Some (CyclicGroup a)) Source #
Create a singleton from factors.
Factors must be distinct, as in output of factorise.
cyclicGroupFromModulo :: (Integral a, UniqueFactorisation a) => a -> Maybe (Some (CyclicGroup a)) Source #
Similar to cyclicGroupFromFactors . factorise,
but much faster, because it
but performes only one primality test instead of full
factorisation.
proofFromCyclicGroup :: Integral a => CyclicGroup a m -> () :- KnownNat m Source #
Convert a cyclic group to a proof that m is known. Usage example:
toModulo :: CyclicGroup Integer m -> Natural toModulo t = case proofFromCyclicGroup t of Sub Dict -> natVal t
pattern CG2 :: CyclicGroup a m Source #
Unidirectional pattern for residues modulo 2.
pattern CG4 :: CyclicGroup a m Source #
Unidirectional pattern for residues modulo 4.
pattern CGOddPrimePower :: Prime a -> Word -> CyclicGroup a m Source #
Unidirectional pattern for residues modulo p^k for odd prime p.
pattern CGDoubleOddPrimePower :: Prime a -> Word -> CyclicGroup a m Source #
Unidirectional pattern for residues modulo 2p^k for odd prime p.
SFactors <=> CyclicGroup
cyclicGroupToSFactors :: Num a => CyclicGroup a m -> SFactors a m Source #
Invert sfactorsToCyclicGroup.
>>>import Data.Maybe>>>cyclicGroupToSFactors (fromJust (sfactorsToCyclicGroup (sfactors :: SFactors Integer 4)))SFactors {unSFactors = [(Prime 2,2)]}
sfactorsToCyclicGroup :: (Eq a, Num a) => SFactors a m -> Maybe (CyclicGroup a m) Source #
Check whether a multiplicative group of residues, characterized by its modulo, is cyclic and, if yes, return its form.
>>>:set -XTypeOperators -XNoStarIsType>>>import GHC.TypeNats>>>sfactorsToCyclicGroup (sfactors :: SFactors Integer 4)Just CG4'>>>sfactorsToCyclicGroup (sfactors :: SFactors Integer (2 * 13 ^ 3))Just (CGDoubleOddPrimePower' (Prime 13) 3)>>>sfactorsToCyclicGroup (sfactors :: SFactors Integer (4 * 13))Nothing
Some wrapper
data Some (a :: Nat -> Type) where Source #
Wrapper to hide an unknown type-level natural.