Copyright | (c) 2019 Andrew Lelechenko |
---|---|
License | MIT |
Maintainer | Andrew Lelechenko <andrew.lelechenko@gmail.com> |
Safe Haskell | None |
Language | Haskell2010 |
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 13
SFactors {sfactorsFactors = [(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 {sfactorsFactors = [(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 :: CyclicGroup Integer 169
CGOddPrimePower' (Prime 13) 2
>>>
sfactorsToCyclicGroup (fromModulo 4)
Just CG4'>>>
sfactorsToCyclicGroup (fromModulo (2 * 13 ^ 3))
Just (CGDoubleOddPrimePower' (Prime 13) 3)>>>
sfactorsToCyclicGroup (fromModulo (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 (fromModulo 4)))
SFactors {sfactorsModulo = 4, sfactorsFactors = [(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.
>>>
sfactorsToCyclicGroup (fromModulo 4)
Just CG4'>>>
sfactorsToCyclicGroup (fromModulo (2 * 13 ^ 3))
Just (CGDoubleOddPrimePower' (Prime 13) 3)>>>
sfactorsToCyclicGroup (fromModulo (4 * 13))
Nothing
Some wrapper
data Some (a :: Nat -> Type) where Source #
Wrapper to hide an unknown type-level natural.