Strange results from modulo - Idris

What happens

Modulo check is outputting strange results on Idris

What do you understand or find about that problem

I’m trying to find the index of the first non-zero member of the Fibonacci sequence which is evenly divisible by a number M. I coded something that works for small M numbers and the Codeabbey example input just fine, however when trying to test the large M numbers given by DATA.lst/CA the program outputs larger indexes that do not correspond to the answer.

You make any workaround? What did you do?

If I use the Int data type, the program will run almost instantly but the result will be wrong for large M numbers, if I try using the Nat data type, the program will compile, will work for small M numbers but otherwise it won’t stop running for a long time

Evidences

The code:


Lines 13 and 14 compute the Fibonacci index (calculated as a counter initialized at 2) of the first Fib number C that satisfies C%M == 0. This function is mapped over the array to compute the result.

The code will work for small M numbers
image
image

But it gets way off base with large numbers
image

I need help with

Understanding why does this code work for small numbers but not for large numbers and why does changing the data type has a huge effect on run times. Maybe the implementation details for large Integers on Idris has something to do with this, but I’m not knowledgeable enough on the inner workings of the language to assert this.

as you realized the problem is the data type you are using, the Int data type does not support big integers and at some point your ind variable gets a big integer, so this number is interpreted as a different number that generates a bad solution.

On the other hand, Nat data type works with this big integers but the mod function is quite slow for some reason, if you wait long enough maybe you could get a correct solution, however there’s another data type that allow solving the problem in seconds, check docs for idris2 and change the data type of your solution.

You were right, using the Integer data type instead of Int fixed the issue, thanks.