在伊德里斯实施埃拉托色尼筛

Question

我正在努力将我对 Eratosthenes 筛的定义翻译成 Idris。这是到目前为止的功能：

%default total

eratos : Nat -> (l : List Nat) -> { auto ok: NonEmpty l } -> List Nat
eratos limit (prime :: rest) =
  if prime * prime > limit -- if we've passed the square root of n
  then prime :: xs         -- then we're done!
  -- otherwise, subtract the multiples of that prime and recurse
  else prime :: (eratos limit (rest \\ [prime^2,prime^2+prime..limit]))

main : IO ()
main = printLn $ eratos [2..100]

不幸的是，我遇到了一个奇怪的编译器错误：

idris --build euler.ipkg
./E003.idr:18:18: error: expected: ")",
    dependent type signature
  else prime :: (eratos n (xs \\ [prime^2,prime^2+prime..n])) 

为什么编译器要寻找类型签名？

Answer 1

我能够实现它如下：

eratos : Nat -> (l : List Nat) -> List Nat
eratos _ [] = []
eratos limit (prime :: rest) =
  if prime * prime > limit -- if we've passed the square root of n
  then prime :: rest       -- then we're done!
  -- otherwise, subtract the multiples of that prime and recurse
  else prime :: eratos limit (rest \\ [(prime*prime),(prime*prime+prime)..limit])

有了这个实现，类型检查器认为这个函数是“覆盖”的。

最理想的情况是，我们不需要第一种情况，并且可以将输入限制为列表长度 >= 1 的情况。但是，很难向编译器显示列表永远不会为 null 或者这函数的第二个参数在每次递归调用时在结构上变得更小。如果有人有建议，请将它们添加为 cmets 或其他答案！