Multiple Return Values in Idris

Idris has support for multiple return values, which can be useful for returning both result and error values from a function.

import Data.Vect

-- The (Int, Int) in this function signature shows that
-- the function returns 2 Ints.
vals : () -> (Int, Int)
vals () = (3, 7)

main : IO ()
main = do
    -- Here we use the 2 different return values from the
    -- call with pattern matching.
    let (a, b) = vals ()
    putStrLn $ show a
    putStrLn $ show b

    -- If you only want a subset of the returned values,
    -- use the wildcard pattern _.
    let (_, c) = vals ()
    putStrLn $ show c

To run the program, save it as multiple_return_values.idr and use the Idris interpreter:

$ idris multiple_return_values.idr -o multiple_return_values
$ ./multiple_return_values
3
7
7

In Idris, functions that return multiple values actually return a single tuple. The syntax (a, b) = vals () is pattern matching on this tuple. The wildcard pattern _ is used to ignore a value in the pattern match.

Idris has strong static typing, so the return type of the function must be explicitly declared. The () in the function type vals : () -> (Int, Int) represents an empty tuple, which is used when a function doesn’t take any meaningful arguments.

Unlike some other languages, Idris doesn’t have a built-in print function for multiple values, so we need to print each value separately using putStrLn $ show x.

Accepting a variable number of arguments is also possible in Idris, typically using list or vector types. We’ll look at this in a future example.