idris - 伊德里斯中的素数

Question

在 idris 0.9.17.1 中，

受https://wiki.haskell.org/Prime_numbers的启发，我编写了以下代码来生成素数

module Main

concat: List a -> Stream a -> Stream a
concat [] ys = ys
concat (x :: xs) ys = x :: (concat xs ys)

generate: (Num a, Ord a) => (start:a) -> (step:a) -> (max:a) -> List a
generate start step max = if (start < max) then start :: generate (start + step) step max else []

mutual
  sieve: Nat -> Stream Int -> Int -> Stream Int
  sieve k (p::ps) x = concat (start) (sieve (k + 1) ps (p * p)) where
    fs: List Int
    fs = take k (tail primes)
    start: List Int
    start = [n | n <- (generate (x + 2) 2 (p * p - 2)), (all (\i => (n `mod` i) /= 0) fs)]

 primes: Stream Int
 primes = 2 :: 3 :: sieve 0 (tail primes) 3


main:IO()
main = do     
  printLn $ take 10 primes

在 REPL 中，如果我写take 10 primes，REPL 正确显示[2, 3, 5, 11, 13, 17, 19, 29, 31, 37] : List Int

但是如果我尝试:exec，什么也不会发生，如果我尝试编译并执行我得到的程序Segmentation fault: 11

有人可以帮我调试这个问题吗？

Answer 1

你的 concat 函数可以懒得解决这个问题。只需将其类型更改为

concat : List a -> Lazy (Stream a) -> Stream a

这会做到的。

注意：要获取所有素数，请将生成函数中的 < 更改为 <=（目前缺少一些，例如 7 和 23）。