Functions in Idris

Functions are central in Idris. We’ll learn about functions with a few different examples.

module Main

import System.IO

-- Here's a function that takes two Integers and returns
-- their sum as an Integer.
plus : Integer -> Integer -> Integer
plus a b = a + b

-- When you have multiple consecutive parameters of
-- the same type, you can use the same type declaration
-- for all of them.
plusPlus : Integer -> Integer -> Integer -> Integer
plusPlus a b c = a + b + c

main : IO ()
main = do
    -- Call a function just as you'd expect, with
    -- name args.
    let res = plus 1 2
    putStrLn $ "1+2 = " ++ show res

    let res = plusPlus 1 2 3
    putStrLn $ "1+2+3 = " ++ show res

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

$ idris functions.idr -o functions
$ ./functions
1+2 = 3
1+2+3 = 6

In Idris, functions are first-class citizens and are central to the language. Here are some key points about functions in Idris:

1. Function declarations typically include type signatures. For example, plus : Integer -> Integer -> Integer declares a function that takes two Integers and returns an Integer.

2. Idris uses currying by default, which means that a function that takes multiple arguments is actually a series of functions that each take one argument.

3. Unlike some languages, Idris doesn’t require explicit return statements. The last expression in a function body is automatically returned.

4. When you have multiple parameters of the same type, you can declare them together as shown in the plusPlus function.

5. Function application in Idris is simply writing the function name followed by its arguments, separated by spaces.

6. The main function in Idris has the type IO (), indicating that it performs I/O operations and doesn’t return a meaningful value.

There are several other features of Idris functions, including dependent types and totality checking, which make Idris a powerful language for writing provably correct programs.