Tickers in Idris

Tickers are for when you want to do something repeatedly at regular intervals. Here’s an example of a ticker that ticks periodically until we stop it.

import Data.IORef
import System.Concurrency
import System.Clock

main : IO ()
main = do
    ticks <- newIORef 0
    done <- newIORef False
    
    -- Create a ticker that ticks every 500 milliseconds
    ticker <- fork $ do
        loop $ do
            sleep $ seconds 0.5
            isDone <- readIORef done
            if isDone
                then pure ()
                else do
                    t <- clockTime Realtime
                    putStrLn $ "Tick at " ++ show t
                    modifyIORef ticks (+1)

    -- Run the ticker for 1600 milliseconds
    sleep $ seconds 1.6
    
    -- Stop the ticker
    writeIORef done True
    sleep $ seconds 0.1  -- Give some time for the ticker to stop
    
    putStrLn "Ticker stopped"
    
    -- Print the number of ticks
    totalTicks <- readIORef ticks
    putStrLn $ "Total ticks: " ++ show totalTicks

    where
        loop : IO () -> IO ()
        loop action = do
            action
            loop action

In this Idris program, we simulate a ticker using a separate thread and IORef for communication. The ticker runs every 500 milliseconds, printing the current time at each tick.

We use fork to start a new thread for the ticker. The ticker runs in a loop, checking the done IORef at each iteration to see if it should stop.

The main thread sleeps for 1600 milliseconds, then sets the done IORef to True to stop the ticker. We use an IORef to count the number of ticks that occurred.

When we run this program, the ticker should tick about 3 times before we stop it.

$ idris -o tickers tickers.idr
$ ./tickers
Tick at MkClockTime 1623456789 123456789
Tick at MkClockTime 1623456789 623456789
Tick at MkClockTime 1623456790 123456789
Ticker stopped
Total ticks: 3

Note that the exact output may vary depending on system performance and timing. The important part is that we see about 3 ticks before the ticker is stopped.