Created
February 11, 2018 08:54
-
-
Save mizunashi-mana/30bccdd729e1a069580ac17e9d0853f2 to your computer and use it in GitHub Desktop.
IsPrimeを遅延させる
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE PolyKinds #-} | |
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE TypeFamilies #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE ConstraintKinds #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
module Data.DeferIsPrime where | |
import GHC.TypeLits | |
import Data.Type.Equality | |
import Data.Proxy | |
import Unsafe.Coerce | |
import Control.Applicative | |
type family Not (x :: Bool) where | |
Not 'True = 'False | |
Not 'False = 'True | |
type family (x :: Nat) % (y :: Nat) :: Nat where | |
x % y = Mod' x y (y <=? x) | |
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 | |
type IsPrime p = IsPrimeB p ~ 'True | |
type family IsPrimeB (p :: Nat) :: Bool where | |
IsPrimeB 0 = 'False | |
IsPrimeB 1 = 'False | |
IsPrimeB 2 = 'True | |
IsPrimeB p = IsPrimeB' p 3 (p % 2 == 0) (Not (3 ^ 2 <=? p)) | |
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) (p % i == 0) (Not ((i + 2) ^ 2 <=? p)) | |
data SomeIsPrime where | |
SomeIsPrime :: (KnownNat p, IsPrime p) => Proxy p -> SomeIsPrime | |
unsafeMagic :: Proxy p -> IsPrimeB p :~: 'True | |
unsafeMagic _ = unsafeCoerce Refl | |
-- ここに型族のIsPrimeと同じ実装を書く | |
isPrime :: KnownNat n => Proxy n -> Bool | |
isPrime n = case natVal n of | |
0 -> False -- テスト用 | |
1 -> True -- テスト用 | |
_ -> undefined | |
-- | | |
-- >>> import Data.Maybe | |
-- >>> isNothing $ deferIsPrime 0 | |
-- True | |
-- >>> isNothing $ deferIsPrime 1 | |
-- False | |
-- | |
deferIsPrime :: Integer -> Maybe SomeIsPrime | |
deferIsPrime i = do | |
n <- someNatVal i | |
case n of | |
SomeNat p | isPrime p -> case unsafeMagic p of | |
Refl -> pure $ SomeIsPrime p | |
_ -> empty |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment