Anonymous Functions

module Tutorial.Functions1.Lambdas

import Tutorial.Functions1.FunctionsWithMultipleArguments

Sometimes we'd like to pass a small custom function to a higher-order function, but without the hassle writing a top level definition. For instance, in the following example, function someTest is very specific and probably not very useful in general, but we'd still like to pass it to higher-order function testSquare:

someTest : Integer -> Bool
someTest n = n >= 3 || n <= 10

Here's, how to pass it to testSquare:

Tutorial.Functions1> testSquare someTest 100
True

Instead of defining and using someTest, we can use an anonymous function:

Tutorial.Functions1> testSquare (\n => n >= 3 || n <= 10) 100
True

For clarity, lets use an anonymous function to reproduce the above definition:

someTest' : Integer -> Bool
someTest' = \n => n >= 3 || n <= 10

Anonymous functions are sometimes also called lambdas (from lambda calculus), and the backslash is chosen since it resembles the Greek letter lambda.

The \n => syntax introduces a new anonymous function of one argument called n, the implementation of which is given on the right hand side of the function arrow. Like other top level functions, lambdas can have more than one arguments, separated by commas: \x,y => x * x + y. When we pass lambdas as arguments to higher-order functions, they typically need to be wrapped in parentheses or separated by the dollar operator ($) (see the next section about this).

Note that, in a lambda, arguments are not annotated with types, so Idris has to be able to infer them from the current context.