Recursion in Idris

Our example demonstrates recursive functions in Idris. Here’s a classic example of factorial calculation using recursion.

module Main

import System.IO

-- This `fact` function calls itself until it reaches the
-- base case of `fact 0`.
fact : Int -> Int
fact n = 
    if n == 0 
        then 1
        else n * fact (n - 1)

main : IO ()
main = do
    putStrLn $ show $ fact 7

    -- Idris doesn't have closures in the same way as some other languages,
    -- but we can define local functions that capture variables from their
    -- surrounding scope. Here's a fibonacci function defined locally:
    let fib : Int -> Int
        fib n = 
            if n < 2 
                then n
                else fib (n - 1) + fib (n - 2)
    
    putStrLn $ show $ fib 7

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:

$ idris recursion.idr -o recursion
$ ./recursion
5040
13

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.