Errors in Idris

In Idris, error handling is typically done using the Either type or custom algebraic data types. Here’s an example that demonstrates error handling similar to the Go code:

import Data.Either

-- Define custom error types
data TeaError = OutOfTea | PowerFailure

-- Function that may return an error
f : Int -> Either String Int
f arg = 
  if arg == 42
    then Left "can't work with 42"
    else Right (arg + 3)

-- Function that uses custom error types
makeTea : Int -> Either TeaError ()
makeTea arg = 
  case arg of
    2 -> Left OutOfTea
    4 -> Left PowerFailure
    _ -> Right ()

-- Main function
main : IO ()
main = do
  -- Example using f
  let results = map f [7, 42]
  putStrLn "Results from f:"
  traverse_ (\case
    Left err -> putStrLn $ "f failed: " ++ err
    Right val -> putStrLn $ "f worked: " ++ show val
  ) results

  -- Example using makeTea
  putStrLn "\nResults from makeTea:"
  traverse_ (\i -> do
    case makeTea i of
      Left OutOfTea -> putStrLn "We should buy new tea!"
      Left PowerFailure -> putStrLn "Now it is dark."
      Right () -> putStrLn "Tea is ready!"
  ) [0..4]

In this Idris version:

1. We use Either String Int to represent a result that can be either an error (Left) or a success (Right), similar to Go’s (int, error) return type.

2. Custom error types are defined using algebraic data types (TeaError).

3. The f function returns Either String Int, where Left represents an error and Right represents a success.

4. The makeTea function uses the custom TeaError type for more specific error handling.

5. In the main function, we use pattern matching to handle the different cases of Either.

6. We use traverse_ to iterate over lists and perform actions, which is similar to the for loops in the Go example.

7. Error checking is done using pattern matching on the Either type, which is idiomatic in Idris.

While Idris doesn’t have a direct equivalent to Go’s errors.Is, the use of algebraic data types for errors allows for precise error matching using pattern matching.

To run this program, save it as Errors.idr and use the Idris compiler:

$ idris Errors.idr -o errors
$ ./errors
Results from f:
f worked: 10
f failed: can't work with 42

Results from makeTea:
Tea is ready!
Tea is ready!
We should buy new tea!
Tea is ready!
Now it is dark.

This example demonstrates how Idris handles errors using algebraic data types and pattern matching, providing a type-safe approach to error handling.