# Functions

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 : (x_{1}: A_{1}) -> ... -> (x_{n}: A_{n}) -> B f p_{1}... p_{n}= d ... f q_{1}... q_{n}= 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
`(x`

and _{1} : A_{1}) -> ... -> (x_{n} : A_{n}) -> B`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.