Sieve of Eratosthenes

sieve.hs

-- Source: https://wiki.haskell.org/Prime_numbers
--primesTo m = sieve [2..m]
             --where
             --sieve (x:xs) = x : sieve (xs \\ [x,x+x..m])
             --sieve [] = []

type family Sieve (n :: Nat) :: [Nat] where
  Sieve n = Sieve' (Drop N2 (UpToN n))

type family Sieve' (xs :: [Nat]) :: [Nat] where
  Sieve'       '[] = '[]
  Sieve' (x ': xs) = x ': Sieve' (DropEveryN x xs)

type family UpToN (n :: Nat) :: [Nat] where
  UpToN 'Z = '[ 'Z  ]
  UpToN ('S n) = (UpToN n) ++ '[ 'S n ]

type family Drop (n :: Nat) (xs :: [Nat]) :: [Nat] where
  Drop 'Z xs            = xs
  Drop _ '[]            = '[]
  Drop ('S n) (_ ': xs) = Drop n xs

type family DropEveryN (n :: Nat) (xs :: [Nat]) :: [Nat] where
  DropEveryN n xs = DropEveryN' n n xs

type family DropEveryN' (x :: Nat) (n :: Nat) (xs :: [Nat]) :: [Nat] where
  DropEveryN' _ _             '[] = '[]
  DropEveryN' x ('S 'Z) ( _ ': xs) = DropEveryN' x x xs
  DropEveryN' x ('S n) (x' ': xs) = x' ': (DropEveryN' x n xs)

type N0  = 'Z
type N1  = 'S N0
type N2  = 'S N1
type N3  = 'S N2
type N4  = 'S N3
type N5  = 'S N4
type N6  = 'S N5
type N7  = 'S N6
type N8  = 'S N7
type N9  = 'S N8
type N10 = 'S N9

-------------------
-------------------

testDropEveryN :: DropEveryN N2 (UpToN N10) :~: '[ N0, N2, N4, N6, N8, N10 ]
testDropEveryN = Refl

testSieve :: Sieve N10 :~: '[ N2, N3, N5, N7 ]
testSieve = Refl