Channel Synchronization in Idris

Our example demonstrates channel synchronization in Idris. Although Idris doesn’t have built-in channels or goroutines like some other languages, we can simulate similar behavior using Idris’s effects system and lightweight processes.

import System
import System.Concurrency

-- This is the function we'll run in a separate process. The
-- 'done' channel will be used to notify another process
-- that this function's work is done.
worker : Channel Bool -> IO ()
worker done = do
  putStr "working..."
  sleep 1
  putStrLn "done"
  -- Send a value to notify that we're done.
  channelPut done True

main : IO ()
main = do
  -- Create a channel for synchronization
  done <- makeChannel

  -- Start a worker process, giving it the channel to
  -- notify on.
  fork (worker done)

  -- Block until we receive a notification from the
  -- worker on the channel.
  _ <- channelGet done
  pure ()

To run this program:

$ idris -o channel-sync channel-sync.idr
$ ./channel-sync
working...done

In this Idris version, we use the System.Concurrency module to create channels and lightweight processes. The worker function simulates work by sleeping for a second, then sends a True value on the done channel to signal completion.

In the main function, we create a channel, fork a new process to run the worker, and then wait for the worker to finish by attempting to receive from the channel.

If you removed the _ <- channelGet done line from this program, the program would exit before the worker even started, similar to the original example.

Note that Idris’s concurrency model is different from some other languages, and this example is a simplified simulation of channel synchronization. In real-world Idris programs, you might use more idiomatic approaches to concurrency and synchronization.