Skip to content

Instantly share code, notes, and snippets.

@autotaker autotaker/Prime.hs
Created Mar 18, 2019

Embed
What would you like to do?
Type-level prime number validation
{-# LANGUAGE GADTs, DataKinds, UndecidableInstances, KindSignatures, TypeOperators, TypeFamilies #-}
module Prime where
import Data.Type.Bool
import Data.Type.Equality
import GHC.TypeLits
import Data.Kind
import Data.Proxy
type family IsFactorization (n :: Nat) (l :: [Nat]) :: Bool where
IsFactorization 0 l = False
IsFactorization 1 '[] = True
IsFactorization 1 l = False
IsFactorization n (p ': l) = Mod n p == 0 && IsFactorizationSub n p l (Mod n p)
type family IsFactorizationSub n p l m where
IsFactorizationSub 0 _ _ _ = TypeError (Text "Invalid argument 0")
IsFactorizationSub n p l 0 = IsFactorizationSub (Div n p) p l (Mod (Div n p) p)
IsFactorizationSub n p l _ = IsFactorization n l
type family ModPow (a :: Nat) (d :: Nat) (n :: Nat) :: Nat where
ModPow a 0 n = 1
ModPow a d n = ModPowSub a d n (Mod d 2 == 0)
type family ModPowSub a d n b where
ModPowSub a d n True = Square (ModPow a (Div d 2) n) n
ModPowSub a d n False =
Mod (Square (ModPow a (Div d 2) n) n GHC.TypeLits.* a) n
type family Square a n where
Square 1 n = 1
Square 0 n = 0
Square a n = Mod (a GHC.TypeLits.* a) n
type family IsPrimeCert (n :: Nat) (l :: [Nat]) (a :: Nat) :: Bool
where
IsPrimeCert n l a = ModPow a (n - 1) n == 1 && IsPrimeCertSub n l a
type family IsPrimeCertSub n l a
where
IsPrimeCertSub n '[] a = True
IsPrimeCertSub n (p ':l) a =
Not (ModPow a (Div (n - 1) p) n == 1) && IsPrimeCertSub n l a
type family CheckPrimeCert (n :: Nat) (l :: [Nat]) (a :: Nat) :: Constraint
where
CheckPrimeCert n l a =
(
((IsFactorization (n - 1) l
|| TypeError (ShowType l :<>: Text " is not the prime factors of ":<>: ShowType n))
&&
(IsPrimeCert n l a
|| TypeError (ShowType a :<>: Text " is not a generator of the multiplicative group modulo " :<>: ShowType n))) ~ True)
type family KnownPrimes l :: Constraint where
KnownPrimes '[] = ()
KnownPrimes (p:ps) = (KnownPrime p, KnownPrimes ps)
class KnownPrime n where
primeCert :: PrimeCert n
data PrimeCert (n :: Nat) where
PrimeCert :: CheckPrimeCert n l a => Proxy l -> Proxy a -> PrimeCert n
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.