for #questions haskell-jp.slack.com

Sample.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}

import Data.Typeable
import Data.Type.Equality
import GHC.TypeLits
import Data.Constraint (Dict(..))
import Data.Singletons
import Data.Singletons.Prelude.Bool
import Data.Singletons.Prelude.Eq
import Data.Singletons.Prelude.Ord
import Data.Singletons.Prelude.Num

class FiniteField k where
  hoge :: k -> String

newtype IntResidueClass (n :: Nat) = MkIntResidueClass Integer deriving (Show, Typeable)

instance (IsPrime p) => FiniteField (IntResidueClass p) where
  hoge _ = "hogehoge"

type family Mod' (x :: Nat) (y :: Nat) (xGeqY :: Bool) :: Nat where
  Mod' x y 'True  = Mod' (x :- y) y (y :<= (x :- y))
  Mod' x y 'False = x

sMod' :: Sing x -> Sing y -> Sing xGeqY -> Sing (Mod' x y xGeqY)
sMod' sx _  SFalse = sx
sMod' sx sy STrue  = sMod' (sx %:- sy) sy (sy %:<= (sx %:- sy))

type family Mod (x :: Nat) (y :: Nat) :: Nat where
  Mod x y = Mod' x y (y :<= x)

sMod :: Sing x -> Sing y -> Sing (Mod x y)
sMod sx sy = sMod' sx sy (sy %:<= sx)

type family IsPrimeB' (p :: Nat) (i :: Nat) (hasFactor :: Bool) (searchEnd :: Bool) where
  IsPrimeB' _ _ 'True _ = 'False
  IsPrimeB' _ _ _ 'True = 'True
  IsPrimeB' p i _ _     = IsPrimeB' p (i :+ 2) (Mod p i :== 0) (Not ((i :+ 2) :* (i :+ 2) :<= p))

s0 :: Sing 0
s0 = sing
s1 :: Sing 1
s1 = sing
s2 :: Sing 2
s2 = sing
s3 :: Sing 3
s3 = sing

sIsPrimeB' :: Sing p -> Sing i -> Sing hasFactor -> Sing searchEnd -> Sing (IsPrimeB' p i hasFactor searchEnd)
sIsPrimeB' p i hasFactor searchEnd =
  case hasFactor of
    STrue -> SFalse
    SFalse -> case searchEnd of
      STrue -> STrue
      SFalse -> sIsPrimeB' p (i %:+ s2) (sMod p i %:== s0) (sNot ((i %:+ s2) %:* (i %:+ s2) %:<= p))

type family IsPrimeB (p :: Nat) (is0 :: Bool) (is1 :: Bool) (is2 :: Bool) :: Bool where
  IsPrimeB _ 'True 'False 'False  = 'False
  IsPrimeB _ 'False 'True 'False  = 'False
  IsPrimeB _ 'False 'False 'True  = 'True
  IsPrimeB p 'False 'False 'False = IsPrimeB' p 3 (Mod p 2 :== 0) (Not (3 :* 3 :<= p))

sIsPrimeB :: Sing p -> Sing is0 -> Sing is1 -> Sing is2 -> Sing (IsPrimeB p is0 is1 is2)
sIsPrimeB _ STrue SFalse SFalse  = SFalse
sIsPrimeB _ SFalse STrue SFalse  = SFalse
sIsPrimeB _ SFalse SFalse STrue  = STrue
sIsPrimeB p SFalse SFalse SFalse = sIsPrimeB' p s3 (sMod p s2 %:== s0) (sNot (s3 %:* s3 %:<= p))
sIsPrimeB _ _ _ _ = error "don't reach this case"

type IsPrime p = IsPrimeB p (p :== 0) (p :== 1) (p :== 2) ~ 'True

testIsPrime :: Sing p -> Maybe (Dict (IsPrime p))
testIsPrime p = case testEquality (sIsPrimeB p (p %:== s0) (p %:== s1) (p %:== s2)) STrue of
  Nothing -> Nothing
  Just eq -> gcastWith eq $ Just Dict

mkIntResidueClassFromSing :: Sing p -> Integer -> IntResidueClass p
mkIntResidueClassFromSing _ = MkIntResidueClass

main :: IO ()
main = do
  s <- getLine
  let i = read s :: Integer
  withSomeSing i $ \p ->
    case testIsPrime p of
      Nothing -> error $ shows i " is not prime"
      Just Dict -> do
        let irc = mkIntResidueClassFromSing p 0
        print $ hoge irc