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 错误。有人能帮我调试这个问题吗？

- Molochdaa

---

你应该在 GitHub 上提交一个错误报告。很明显是编译器出了问题。 - dfeuer

完成：https://github.com/idris-lang/Idris-dev/issues/2290 - Molochdaa

Answer 1

您的 concat 函数可以改为懒执行以解决此问题。只需将其类型更改为

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

这样就可以了。

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

- Falko