# Functions

See the official user manual for the most up-to-date version of the information on this page.

Function types are written (x : A) -> B, or in the case of non-dependent functions simply A -> B. For instance, the type of the addition function for natural numbers is

Nat -> Nat -> Nat

and the type of the addition function for vectors is:

(A : Set) -> (n : Nat) -> (u : Vec A n) -> (v : Vec A n) -> Vec A n

where Set is the type of sets and Vec A n is the type of vectors with n elements of type A. Arrows between consecutive hypotheses of the form (x : A) may also be omitted, and (x : A)(y : A) may be shortened to (x y : A):

(A : Set)(n : Nat)(u v : Vec A n) -> Vec A n

Functions are constructed by lambda abstractions, which can be either typed or untyped. For instance, both expressions below have type (A : Set) -> A -> A (the second expression checks against other types as well):

\ (A : Set)(x : A) -> x
\ A x -> x

Applications are written as f a b c where f is a function and a, b and c are arguments.

## Function declarations

The general form for defining a function is

f : (x1 : A1) -> ... -> (xn : An) -> B
f p1 ... pn = d
...
f q1 ... qn = e

where f is a new identifier, A is a type, B is a type under the assumption that the variable x has the type A, p_i and q_i are patterns and d and e are expressions.

The declaration above gives the identifier f type (x1 : A1) -> ... -> (xn : An) -> B and f is defined by the defining equations. Patterns are matched from top to bottom, i.e., the first pattern that matches the actual parameters is the one that is used.

## Abstraction

An object in the type (x : A) -> B is always equal to

\x -> b

where b : B under the assumption that x : A.

Typed abstraction can also be used:

\(x : A) -> b

is another notation for the abstraction above if the type of the variable x is A.

## Application

The application of a function f : (x : A) -> B to an argument a : A is written f a and the type of this is B[x := a]

## Notational conventions

The following notational conventions can be used

• function types
(x : A)(y : B) -> C    is the same as (x : A) -> (y : B) -> C
(x y : A) -> C         is the same as (x : A)(y : A) -> C
forall (x : A) -> C    is the same as (x : A) -> C
forall x -> C          is the same as (x : _) -> C
forall x y -> C        is the same as forall x -> forall y -> C

You can also use the Unicode symbol (type "\all" in the Emacs Agda mode) instead of forall.

• functional abstraction
\x y -> e  is the same as \x -> (\y -> e)
• functional application
f a b  is the same as (f a) b

## Pattern matching lambdas.

Anonymous pattern matching functions can be defined using the syntax

\ { p11 .. p1n -> e1 ; ... ; pm1 .. pmn -> em }

(where, as usual, \ and -> can be replaced by λ and →). Internally this is translated into a function definition of the following form:

.extlam p11 .. p1n = e1
...
.extlam pm1 .. pmn = em

This means that anonymous pattern matching functions are generative. For instance, refl will not be accepted as an inhabitant of the type

(λ { true → true ; false → false }) ≡
(λ { true → true ; false → false }),

because this is equivalent to extlam1 ≡ extlam2 for some distinct fresh names extlam1 and extlam2.

Currently the 'where' and 'with' constructions are not allowed in (the top-level clauses of) anonymous pattern matching functions.

Examples:

and : Bool → Bool → Bool
and = λ { true x → x ; false _ → false }

xor : Bool → Bool → Bool
xor = λ { true  true  → false
; false false → false
; _     _     → true
}

fst : {A : Set} {B : A → Set} → Σ A B → A
fst = λ { (a , b) → a }

snd : {A : Set} {B : A → Set} (p : Σ A B) → B (fst p)
snd = λ { (a , b) → b }

Unlike the usual layout rules, the { ... } block of a pattern matching lambda cannot be replaced by indentation.