Closures in Idris

Idris supports anonymous functions, which can form closures. Anonymous functions are useful when you want to define a function inline without having to name it.

import Data.IORef

intSeq : IO (IO Int)
intSeq = do
    i <- newIORef 0
    pure $ do
        modifyIORef i (+1)
        readIORef i

main : IO ()
main = do
    -- We call intSeq, assigning the result (an IO action) to nextInt.
    -- This action captures its own i value, which will be updated
    -- each time we call nextInt.
    nextInt <- intSeq

    -- See the effect of the closure by calling nextInt a few times.
    n1 <- nextInt
    putStrLn $ show n1
    n2 <- nextInt
    putStrLn $ show n2
    n3 <- nextInt
    putStrLn $ show n3

    -- To confirm that the state is unique to that particular function,
    -- create and test a new one.
    newInts <- intSeq
    n4 <- newInts
    putStrLn $ show n4

In this Idris code, we define a function intSeq that returns another IO action. The returned action closes over a mutable reference i to form a closure.

The intSeq function creates a new IORef (a mutable reference in Idris) initialized to 0. It then returns an IO action that, when executed, increments the value in the IORef and returns the new value.

In the main function, we call intSeq and assign the result to nextInt. This nextInt action captures its own i value, which will be updated each time we call it.

We then demonstrate the effect of the closure by calling nextInt multiple times and printing the results. Each call increments and returns the next integer in the sequence.

Finally, to confirm that the state is unique to each closure, we create a new sequence newInts and call it once, showing that it starts from 1 again.

To run this program, you would typically save it in a file with a .idr extension, then use the Idris compiler to compile and run it:

$ idris -o closures closures.idr
$ ./closures
1
2
3
1

This example demonstrates how Idris can use closures to maintain state across function calls, similar to other functional programming languages.