Panic in Idris

In Idris, we don’t have a direct equivalent to Go’s panic. Instead, we can use exceptions or the Error type to handle unexpected situations. Here’s an example that demonstrates similar behavior:

import System.File
import System.Exception

main : IO ()
main = do
  -- We'll use exceptions throughout this site to check for
  -- unexpected errors. This is the only program on the
  -- site designed to throw an exception.
  throw (UserError "a problem")

  -- A common use of exceptions is to abort if a function
  -- returns an error value that we don't know how to
  -- (or want to) handle. Here's an example of
  -- throwing an exception if we get an unexpected error when creating a new file.
  Right file <- openFile "/tmp/file" WriteTruncate
    | Left err => throw (FileError err)
  
  closeFile file

Running this program will cause it to throw an exception, print an error message, and exit with a non-zero status.

When the first exception in main is thrown, the program exits without reaching the rest of the code. If you’d like to see the program try to create a temp file, comment out the first throw line.

$ idris panic.idr -o panic
$ ./panic
UserError "a problem"

Note that unlike some languages which use exceptions for handling of many errors, in Idris it is idiomatic to use the Either type or other error-indicating return values wherever possible. The throw mechanism is typically reserved for truly exceptional situations.

In Idris, we have a more powerful type system that allows us to express and prevent many errors at compile-time, reducing the need for runtime exceptions. However, for situations where runtime errors are unavoidable, the exception mechanism provides a way to handle unexpected situations.