Exit in Idris

Here’s an idiomatic Idris example demonstrating the concept of exiting a program:

module Main

import System
import System.File

main : IO ()
main = do
  -- This will not be executed due to the early exit
  let _ = putStrLn "This won't be printed!"
  
  -- Exit the program with status code 3
  exitWith (ExitFailure 3)
  
  -- This line will never be reached
  putStrLn "This also won't be printed!"

This Idris program demonstrates how to exit a program immediately with a specific status code. Let’s break down the code and explain its components:

1. We import the necessary modules: System for the exitWith function and System.File for the ExitFailure constructor.

2. The main function is defined as an IO () action, which is the entry point of our Idris program.

3. We use let _ = putStrLn "This won't be printed!" to demonstrate that this line will not be executed due to the early exit. The _ is used to ignore the result of putStrLn.

4. The exitWith function is called with ExitFailure 3 as its argument. This immediately terminates the program with an exit status of 3.

5. The last putStrLn statement will never be reached due to the early exit.

To compile and run this Idris program:

1. Save the code in a file named Exit.idr.
2. Compile the program using the Idris compiler:

$ idris -o exit Exit.idr

This will create an executable named exit.

3. Run the program:

$ ./exit
$ echo $?
3

You’ll notice that nothing is printed to the console, and the exit status is 3.

In Idris, unlike some other languages, we don’t return an integer from the main function to indicate the exit status. Instead, we use the exitWith function to explicitly set the exit status.

The ExitFailure constructor is used to represent non-zero exit codes, while ExitSuccess represents a zero exit code. This approach provides type safety and clarity when working with exit codes.

This example demonstrates how Idris handles program termination and exit codes, which is particularly useful for command-line applications or scripts where the exit status is important for error handling and process control.