Recursion in Idris
Our example demonstrates recursive functions in Idris. Here’s a classic example of factorial calculation using recursion.
In this example, we define a recursive fact
function to calculate factorials. The function calls itself with n - 1
until it reaches the base case of n == 0
.
We then define a local function fib
inside the main
function to calculate Fibonacci numbers. This demonstrates how Idris allows local function definitions that can be recursive.
To run this program, save it in a file with a .idr
extension (e.g., recursion.idr
), then use the Idris compiler to compile and run it:
The output shows the factorial of 7 (5040) and the 7th Fibonacci number (13).
Idris’s strong type system and support for dependent types make it particularly well-suited for writing provably correct recursive functions. While this example doesn’t showcase these advanced features, they’re available when you need them for more complex recursive algorithms.