Custom Errors in Idris

import System.Error

-- A custom error type usually has the suffix "Error".
data ArgError : Type where
  MkArgError : Int -> String -> ArgError

-- Adding this `show` implementation makes `ArgError` printable.
implementation Show ArgError where
  show (MkArgError arg message) = show arg ++ " - " ++ message

f : Int -> Either ArgError Int
f arg = 
  if arg == 42
    then Left (MkArgError arg "can't work with it")  -- Return our custom error.
    else Right (arg + 3)

main : IO ()
main = do
  -- `isLeft` checks if the result is an error (Left).
  -- `fromLeft` extracts the error value if it exists.
  let result = f 42
  case result of
    Left err => do
      putStrLn $ show $ fromLeft err
    Right _ => 
      putStrLn "err doesn't match ArgError"

This example demonstrates how to create and use custom errors in Idris. Let’s break it down:

1. We define a custom error type ArgError using Idris’s algebraic data types. This is similar to defining a struct in other languages.

2. We implement the Show interface for ArgError, which is equivalent to implementing the Error() method in Go. This allows us to convert our error to a string.

3. The f function returns an Either ArgError Int. In Idris, Either is commonly used to represent computations that might fail, where Left represents an error and Right represents a success.

4. In the main function, we use pattern matching to handle the result of f 42. If it’s a Left (error), we print the error. Otherwise, we print a message indicating no error occurred.

To run this program, you would typically save it in a file with a .idr extension and use the Idris compiler:

$ idris -o custom-errors custom-errors.idr
$ ./custom-errors
42 - can't work with it

This example showcases Idris’s strong type system and pattern matching capabilities, which provide a robust way to handle errors and ensure type safety at compile time.