エラトステネス篩をIdrisで実装する

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にならないようにコンパイラに指示するのは難しいです。この関数の2番目の引数は、各再帰呼び出しで構造的に小さくなっています。誰かに提案がある場合は、コメントや別の回答として追加してください！