Function declarations

A function declaration consists of a type signature and a group of function clauses.

In the following example, we define a function multiplyByTwo.

  import Stdlib.Data.Nat open using {Nat; *};

  multiplyByTwo : Nat -> Nat;
  multiplyByTwo n := 2 * n;

The first line multiplyByTwo : Nat -> Nat; is the type signature and the second line multiplyByTwo n := 2 * n; is a function clause.

Pattern matching

A function may have more than one function clause. When a function is called, it will pattern match on the input, and the first clause that matches the arguments is used.

The following function has two clauses:

  import Stdlib.Data.Bool open;

  neg : Bool -> Bool;
  neg true := false;
  neg false := true;

When neg is called with true, the first clause is used and the function returns false. Similarly, when neg is called with false, the second clause is used and the function returns true.

Mutually recursive functions

Function declarations can depend on each other recursively. In the following example, we define a function that checks if a number is even by calling a function that checks if a number is odd.

  import Stdlib.Data.Nat open;
  import Stdlib.Data.Bool open;

  import Stdlib.Prelude open;

  odd : Nat -> Bool;

  even : Nat -> Bool;

  odd zero := false;
  odd (suc n) := even n;

  even zero := true;
  even (suc n) := odd n;

Anonymous functions

Anonymous functions, or lambdas, are introduced with the syntax:

\{| pat1 .. patN_1 := clause1
  | ..
  | pat1 .. patN_M := clauseM }

The first pipe | is optional. Instead of \ one can also use the Unicode alternative – λ.

An anonymous function just lists all clauses of a function without naming it. Any function declaration can be converted to use anonymous functions:

  import Stdlib.Prelude open;

  odd : Nat -> Bool;

  even : Nat -> Bool;

  odd :=
    \ {
      | zero := false
      | (suc n) := even n
    };

  even :=
    \ {
      | zero := true
      | (suc n) := odd n
    };

Short definitions

A function definition can be written in one line, with the body immediately following the signature:

  import Stdlib.Data.Nat open;

  multiplyByTwo : Nat -> Nat := \ {n := 2 * n};

Comments