# 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 : (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.