Timers in Idris

Our first example demonstrates how to use timers in Idris. Timers allow us to execute code at some point in the future or repeatedly at some interval. We’ll focus on timers in this example.

import Data.IORef
import System.Concurrency

main : IO ()
main = do
    -- Timers represent a single event in the future. Here,
    -- we create a timer that will wait for 2 seconds.
    timer1 <- fork $ do
        sleep 2000  -- Sleep for 2 seconds (2000 milliseconds)
        putStrLn "Timer 1 fired"

    -- We wait for the timer to complete
    wait timer1
    
    -- If you just wanted to wait, you could have used
    -- `sleep`. One reason a timer may be useful is
    -- that you can cancel it before it fires.
    -- Here's an example of that.
    cancelFlag <- newIORef False
    
    timer2 <- fork $ do
        sleep 1000  -- Sleep for 1 second
        cancelled <- readIORef cancelFlag
        if not cancelled
            then putStrLn "Timer 2 fired"
            else pure ()

    -- Simulate stopping the timer
    writeIORef cancelFlag True
    putStrLn "Timer 2 stopped"

    -- Give timer2 enough time to fire, if it ever
    -- was going to, to show it is in fact stopped.
    sleep 2000  -- Sleep for 2 seconds

In this Idris example, we’re using the System.Concurrency module to simulate timers. We use fork to start asynchronous computations and sleep to introduce delays.

For the first timer, we simply fork a computation that sleeps for 2 seconds and then prints a message. We use wait to block until this computation completes.

For the second timer, we demonstrate how to “cancel” a timer. We use an IORef to hold a cancellation flag. The timer checks this flag before executing its action. We set the flag to simulate stopping the timer.

To run this program, save it as timers.idr and use the Idris compiler:

$ idris -o timers timers.idr
$ ./timers
Timer 2 stopped
Timer 1 fired

The first timer will fire ~2 seconds after we start the program, but the second timer’s action is prevented from executing due to our “cancellation” mechanism.

Note that Idris doesn’t have built-in timer functionality like Go, so we’ve simulated it using concurrency primitives. In a real-world scenario, you might want to use a more sophisticated timing library if available.