在Idris中实现Eratosthenes筛分

eratosthenesSieve : Int -> List Int
eratosthenesSieve n = let
  isPrime : Vect (n+1) Bool
  isPrime = True :: True :: replicate n False

  sieve : Int -> Vect (n+1) Bool -> Vect (n+1) Bool
  sieve p isPrime = if p * p > n
    then isPrime
    else if isPrime ! p
      then sieve (p + 1) (updateMultiples p isPrime)
      else sieve (p + 1) isPrime

  updateMultiples : Int -> Vect (n+1) Bool -> Vect (n+1) Bool
  updateMultiples p isPrime = let
    multiples = [p * i | i <- [2..n `div` p]]
    in updateList multiples isPrime

  updateList : List Int -> Vect (n+1) Bool -> Vect (n+1) Bool
  updateList [] isPrime = isPrime
  updateList (x :: xs) isPrime = updateList xs (update x False isPrime)

  primes : List Int
  primes = [i | (i, True) <- zip [2..n] (sieve 2 isPrime)]
in primes