NthPrime problem in the Idris2 track

Programming Idris
1

In this problem Nth Prime in Idris on Exercism, the function signature is prime : Nat → Nat. The Nat in Idris2 is basically an inductive type, without compiler optimization, so basic arithmetic for large numbers are basically not usable. I solved the problem after I modify the signature as prime : Integer → Integer.

2

We could increase this exercise’s difficulty on the Idris track, as we have the non-canonical test case

  test "very big prime" (assertEq (prime 65537) 821647)

Today on my laptop (AMD Ryzen 5), I timed the track’s example solutions, running the test runner in docker.

$ time bin/test hello-world
...
real    0m5.087s
...

$ time bin/test nth-prime
...
real    0m5.765s
...

$ time bin/test perfect-numbers
...
real    0m6.262s
...

The nth-prime example solution uses Nat.

The perfect-numbers exercise uses Integer, with the largest test cases involving 33,550,335 33,550,336 33,550,337.

1 Like
3

https://idris2.readthedocs.io/en/stable/reference/builtins.html

Idris2 supports an optimized runtime representation of natural numbers (non-negative integers).

At runtime, Idris2 will automatically represent this the same as the Integer type.

1 Like